Factorial-weighted closure of the source amplitudes in l.Tm.minus.thetam. The analytic input is the exact per-increment l.V bound; this file closes only its finite scalar sum.

theorem AVenhance.Infra.Section4.iterateAmplitude_two_shift_le_geometric {η : ℝ} (hη : 0 ≤ η) (hηsmall : η ≤ 1 / 4) (k : ℕ) : iterateAmplitude η (k + 2) ≤ η * (1 / 2) ^ k

For the positive increments, the source amplitude after the first two levels is dominated by a geometric tail when η ≤ 1/4.

theorem AVenhance.Infra.Section4.iterateAmplitude_positive_sum_le_three {η : ℝ} (hη : 0 ≤ η) (hηsmall : η ≤ 1 / 4) (N : ℕ) : ∑ i ∈ Finset.range N, iterateAmplitude η (i + 1) ≤ 3 * η

The finite sum of all positive-increment source amplitudes costs at most 3η: the first increment contributes η, the second-through-last increments have a geometric majorant of mass at most 2η.

theorem AVenhance.Infra.Section4.iterate_Tm_minus_theta_factorial_sum_bound {η ρ C₀ : ℝ} {N : ℕ} (hη : 0 ≤ η) (hηsmall : η ≤ 1 / 4) (hscale : η ≤ C₀ * ρ) (hC₀ρ : 0 ≤ C₀ * ρ) : ∑ i ∈ Finset.range N, ↑(2 * (i + 1)).factorial * iterateAmplitude η (i + 1) ≤ ↑(2 * N).factorial * (4 * C₀ * ρ)

The source l.V amplitude estimates sum to the error scale in l.Tm.minus.thetam. This is the numerical closure with the source's 4 C₀^3 slack; application to the actual L² norms uses Minkowski separately.