Uniform bounds for the single-mode corrector ingredients.

theorem AVenhance.Infra.Section3.CorrectorBounds.indIcc_le_one (a b t : ℝ) : indIcc a b t ≤ 1

theorem AVenhance.Infra.Section3.zetaMK_mem_Icc {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) (t : ℝ) : I.zetaMK m k t ∈ Set.Icc 0 1

Each small-scale time cutoff lies in [0,1].

theorem AVenhance.Infra.Section3.hatZetaML_mem_Icc {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (t : ℝ) : I.hatZetaML m l t ∈ Set.Icc 0 1

For positive scales, each translated large-scale time cutoff lies in [0,1].

theorem AVenhance.Infra.Section3.zetaProd_mem_Icc {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (t : ℝ) : I.zetaProd m k t ∈ Set.Icc 0 1

The Section 3 forcing coefficient is between zero and one.

theorem AVenhance.Infra.Section3.corrTime_nonneg_le_inv {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (k : ℤ) (t : ℝ) : 0 ≤ I.corrTime κ m k t ∧ I.corrTime κ m k t ≤ (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2)⁻¹

The memory integral is nonnegative and bounded by the exponential relaxation scale.

theorem AVenhance.Infra.Section3.CorrectorBounds.abs_mul_cos_le (c z : ℝ) : |c * Real.cos z| ≤ |c|

theorem AVenhance.Infra.Section3.uShear_component_abs_le {β : ℝ} {Λ m : ℕ} (k : ℤ) (x : Homogenization.Vec 2) (j : Fin 2) : |uShear β Λ m k x j| ≤ |2 * Real.pi * a β Λ m * epsilon β Λ m|

Every component of the shear is bounded by its amplitude.

theorem AVenhance.Infra.Section3.chiMK_component_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) : |I.chiMK κ m k t x j| ≤ (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2)⁻¹ * |2 * Real.pi * a β I.Λ m * epsilon β I.Λ m|

The explicit corrector has a global bound when κ > 0.