Actual integrated forcing with dissipation absorbed uniformly in order.

theorem AVenhance.Infra.Section4.iterate_truncated_allocated_word_flux_bound {A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} {s : ℝ} (hs1 : s ≤ 1) (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (hcoef : ∀ p ∈ iterateSpatialSplits w, ContinuousOn (fun (z : AmnrSpace) => iterateMatrixWord (A z.1) p.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) {κ : ℝ} (hκ : 0 < κ) (D E : ℕ → ℝ) (hD : ∀ (t : ℝ) (x : Homogenization.Vec 2), ∀ p ∈ iterateSpatialSplits w, ∀ (j k : Fin 2), |iterateMatrixWord (A t) p.1 x j k| ≤ D p.1.length) (hE : ∀ p ∈ iterateSpatialSplits w, (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (v t))) ≤ E p.2.length) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u z.1)) z.2) (iterateWordFlux (A z.1) (v z.1) w z.2)| ≤ (κ / 8 * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (u t))) + 16 / κ * ∑ j ∈ Finset.range (w.length + 1), ↑(w.length.choose j) ^ 2 * 2 ^ j * D j ^ 2 * E (w.length - j)

The actual all-order flux pairing has a uniform dissipation allocation and an explicit binomial-square sum of preceding gradient energies.