Exact analytic weights in the linear material commutator recurrence.

theorem AVenhance.Infra.Section4.iterate_linear_material_factorial_le (n j i : ℕ) (hj : j ≤ n) : n.choose j * j.factorial * (n - j + 2 * i).factorial * (n + 2 * i - 1).factorial ≤ (n + 2 * i).factorial ^ 2

The current lower-order factorial and preceding Hessian factorial are absorbed by two current factorial weights.

theorem AVenhance.Infra.Section4.iterate_linear_material_analytic_term_le (n j i : ℕ) (hj : j ≤ n) {b L : ℝ} (hb : 0 ≤ b) (hL : 0 < L) : ↑(n.choose j) * (↑j.factorial * b ^ j) * (↑(n - j + 2 * i).factorial * L ^ (n - j)) * (↑(n + 2 * i - 1).factorial * L ^ (n + 1)) ≤ (b / L) ^ j * L * (↑(n + 2 * i).factorial * L ^ n) ^ 2

The remaining radius gain is exactly one geometric factor per velocity jet. No derivative-order constant is introduced.

theorem AVenhance.Infra.Section4.iterate_linear_material_series_le (n i : ℕ) {b L : ℝ} (hb : 0 ≤ b) (hL : 0 < L) (hg : b / L ≤ 1 / 2) (D : ℕ → ℝ) (hD : ∀ (r : ℕ), 0 ≤ D r) : ∑ k ∈ Finset.range n, ↑(n.choose (k + 1)) * (↑(k + 1).factorial * b ^ (k + 1)) * (↑(n - (k + 1) + 2 * i).factorial * L ^ (n - (k + 1))) * (↑(n + 2 * i - 1).factorial * L ^ (n + 1)) * D (n - (k + 1)) ≤ b * (↑(n + 2 * i).factorial * L ^ n) ^ 2 * ∑ k ∈ Finset.range n, (1 / 2) ^ k * D (n - 1 - k)

The positive velocity-jet orders give the geometric linear kernel in the actual norm recurrence. The leading radius factor cancels exactly.