Exact binomial-square remainder after allocating dissipation.

theorem AVenhance.Infra.Section4.iterate_weighted_remainder_group_bound {κ : ℝ} (hκ : 0 < κ) (w : List (Fin 2)) (D E : ℕ → ℝ) (G : List (Fin 2) → ℝ) (hG : ∀ p ∈ iterateSpatialSplits w, G p.2 ≤ E p.2.length) : (List.map (fun (p : List (Fin 2) × List (Fin 2)) => D p.1.length ^ 2 / iterateYoungWeight κ w.length p.1.length * G p.2) (iterateSpatialSplits w)).sum ≤ 16 / κ * ∑ j ∈ Finset.range (w.length + 1), ↑(w.length.choose j) ^ 2 * 2 ^ j * D j ^ 2 * E (w.length - j)

A preceding gradient-energy bound at each scalar order groups the actual Leibniz remainder with squared, rather than exponential, multiplicities.