Source estimate for the actual flow-pulled gradient in the first d_m term.

theorem AVenhance.Infra.Section4.DmPulledGradient.dm_gradMatrix_entry_eq_fderiv {X : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} (hX : DifferentiableAt ℝ X x) (i j : Fin 2) : gradMatrix X x i j = (fderiv ℝ X x) (Homogenization.basisVec i) j

theorem AVenhance.Infra.Section4.hatXiML_active_time_window {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (t : ℝ) (hactive : I.hatXiML m l t ≠ 0) : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m

Every active large cutoff lies in its time window.