The squared geometric kernel from stream coefficient orders at least two.

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

Remove orders zero and one without changing any remaining term.

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

Every high stream jet supplies two radius gains before the remaining geometric kernel. The lower scalar energy remains squared in this term.