Left-Jacobian form: spatial smoothness of the pulled gap fluxes y ↦ Σ_l ξ̂_l F_lᵀ M F_l ∇T (constant matrix M), which carry the base flux (M = JHat - K) and the first summand of sourceErrorD (M = JHat - 𝒥).

theorem AVenhance.Infra.Section5.LeftJacobian.contDiff_flowGrad_entry {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (i j : Fin 2) : ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => I.flowGrad hΦ m l t y i j

theorem AVenhance.Infra.Section5.LeftJacobian.contDiff_pulledGapFlux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (M : Matrix (Fin 2) (Fin 2) ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hT : ContDiff ℝ (↑⊤) (T t)) : ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => ∑' (l : ℤ), I.hatXiML m l t • (I.flowGrad hΦ m l t y).transpose.mulVec (M.mulVec ((I.flowGrad hΦ m l t y).mulVec (spaceGrad (T t) y)))

y ↦ Σ_l ξ̂_l F_lᵀ M F_l ∇T is spatially C^∞ for a constant matrix M.