Positive velocity orders in actual squared material-error energies.

theorem AVenhance.Infra.Section4.iterate_sum_positive_orders (n : ℕ) (f : ℕ → ℝ) : (∑ j ∈ Finset.range (n + 1), if 1 ≤ j then f j else 0) = ∑ k ∈ Finset.range n, f (k + 1)

Exact positive-order range shift.

theorem AVenhance.Infra.Section4.iterate_positive_factorial_profile_sum_le (n a : ℕ) {r L : ℝ} (hL : 0 < L) (hg : 2 * (r / L) ^ 2 ≤ 1 / 2) : (∑ j ∈ Finset.range (n + 1), if 1 ≤ j then ↑(n.choose j) ^ 2 * 2 ^ j * (↑j.factorial * r ^ j) ^ 2 * (↑(n - j + a).factorial * L ^ (n - j)) ^ 2 else 0) ≤ 4 * (r / L) ^ 2 * (↑(n + a).factorial * L ^ n) ^ 2

Every actual positive velocity order contributes a squared radius gain, after exact binomial-factorial cancellation.