Corrected scalar closure of l.V, retaining the corrected C/C0 remainder. These are scalar induction helpers; the actual PDE recurrence is a separate required input and is not claimed to have been derived in this module.

theorem AVenhance.Infra.Section4.iterateAmplitude_pos {η : ℝ} (hη : 0 < η) (i : ℕ) : 0 < iterateAmplitude η i

All printed amplitude coefficients are positive for positive eta.

theorem AVenhance.Infra.Section4.iterateAmplitude_scaled_previous_ratio {C₀ q : ℝ} (hC : 0 < C₀) (hq : 0 < q) (hsmall : C₀ * q ≤ 1) {i : ℕ} (hi : 1 ≤ i) : q * iterateAmplitude (C₀ * q) (i - 1) / iterateAmplitude (C₀ * q) i ≤ C₀⁻¹

The squared previous-amplitude estimate also gives the linear ratio needed for the half-geometric term, including the first increment.

theorem AVenhance.Infra.Section4.iterate_corrected_material_remainder_bound {C C₀ q : ℝ} (hC : 0 ≤ C) (hC₀ : 0 < C₀) (hq : 0 < q) (hsmall : C₀ * q ≤ 1) {i : ℕ} (hi : 2 ≤ i) : C * (q ^ 2 * iterateAmplitudeSq (C₀ * q) (i - 1) / iterateAmplitudeSq (C₀ * q) i) + C * (q * iterateAmplitudeSq (C₀ * q) (i - 1) / iterateAmplitudeSq (C₀ * q) i) + C * (q ^ 2 * iterateAmplitudeSq (C₀ * q) (i - 2) / iterateAmplitudeSq (C₀ * q) i) ≤ C / C₀ + 2 * C / C₀ ^ 2

The three retained material remainders at i >= 2 have the corrected C/C0 + 2C/C0^2 budget. In particular, the C/C0 term is not discarded.

theorem AVenhance.Infra.Section4.iterate_source_linear_ratio_le {C₀ ρ F : ℝ} (hC₀ : 0 < C₀) (hρ : 0 < ρ) (hF : C₀ ≤ F) (hsmall : C₀ * (ρ * F ^ 2) ≤ 1) {i : ℕ} (hi : 1 ≤ i) : ρ * iterateAmplitude (C₀ * (ρ * F ^ 2)) (i - 1) / iterateAmplitude (C₀ * (ρ * F ^ 2)) i ≤ 1 / C₀ ^ 3

The actual source amplitude ratio controls the linear convolution coefficient by C0^-3, since F >= C0.