Inputs of the first-summand d_m estimate: the stream-regularity flow-Jacobian bound on active cutoff windows in the elementwise supremum norm, and the L² bound of the terminal temperature gradient from the profile.

theorem AVenhance.Infra.Section4.dm_flowGrad_norm_le_two_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (z : ℝ × Homogenization.Vec 2) (l : ℤ) : I.hatXiML m l z.1 ≠ 0 → ‖I.flowGrad hΦ m l z.1 z.2‖ ≤ 2

The stream-regularity estimates bound the pullback Jacobian, in the elementwise supremum norm, by two on every active cutoff window.

theorem AVenhance.Infra.Section4.dm_Tgrad_eLpNorm_le_of_Tprofile (T : ℝ → Homogenization.Vec 2 → ℝ) (hGradCont : Continuous fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (T z.1) z.2) {κprev N : ℝ} (hκprev : 0 < κprev) (hTprofile : √κprev * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (T t)) ≤ N) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (T z.1) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (N / √κprev)

The L²(timeCube) norm of the terminal temperature gradient is controlled by the profile: ‖∇T‖_{L²} ≤ N / √κ_prev.