Absorb the exact first-stream multiplicity into analytic weights.

theorem AVenhance.Infra.Section4.iterate_first_stream_factorial_le (n i : ℕ) (hn : 1 ≤ n) : n * (n - 1 + 2 * i).factorial ^ 2 ≤ (n + 2 * i).factorial ^ 2

The n first-jet terms cost no derivative-order constant after the preceding factorial energy is compared to the current factorial energy.

theorem AVenhance.Infra.Section4.iterate_first_stream_analytic_weight_le (n i : ℕ) (hn : 1 ≤ n) {L : ℝ} (hL : 0 < L) : ↑n * (↑(n - 1 + 2 * i).factorial * L ^ (n - 1)) ^ 2 ≤ (↑(n + 2 * i).factorial * L ^ n) ^ 2 / L ^ 2

The first coefficient derivative supplies exactly one squared analytic radius gain after summing all n positions.