The K_m + s_{m-1} flux (corrected form).

The identity (K_m + s_{m-1})∇T = K_m GDot_m fails for the sMat; instead the coefficient has the Piola form (K + s)∇T = Σ_l ξ̂_l [κ F_l + F_lᵀ (K - κ) F_l] ∇T (Kmat_add_sMat_mulVec_eq_piola, from LeftJacobian.Kmat_add_sMatPlus_mulVec; sMat = sMatPlus by rfl).

theorem AVenhance.Infra.Section5.Kmat_add_sMat_mulVec_eq_piola {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : (I.Kmat κ m t + I.sMat hΦ m κ t x).mulVec (spaceGrad (T t) x) = ∑' (l : ℤ), I.hatXiML m l t • (κ • I.flowGrad hΦ m l t x + (I.flowGrad hΦ m l t x).transpose * (I.Kmat κ m t - κ • 1) * I.flowGrad hΦ m l t x).mulVec (spaceGrad (T t) x)

The Piola form of the coarse flux, the corrected formulation (4).