Summation of the actual first-material velocity recursion.

theorem AVenhance.Infra.Section4.amnr_negative_power_sum {β p : ℝ} (I : Ingredients β) (hp : p ≤ -(1 / 7)) (m : ℕ) : ∑ j ∈ Finset.range (m + 1), epsilon β I.Λ j ^ p ≤ 2 * epsilon β I.Λ m ^ p

Minimal separation controls every negative-power scalar amplitude sum. The constant does not depend on the number of scales or on Λ.

theorem AVenhance.Infra.Section4.amnr_abs_recursion_sum (v u : ℕ → ℝ) {K : ℝ} (hK : 0 ≤ K) (hu : ∀ (j : ℕ), 0 ≤ u j) (hzero : v 0 = 0) (hstep : ∀ (j : ℕ), |v (j + 1) - v j| ≤ K * u (j + 1)) (m : ℕ) : |v m| ≤ K * ∑ j ∈ Finset.range (m + 1), u j

Absolute summation of an actual scalar recursion, retaining its base term.