LeftJacobian the left-Jacobian form: the coarse transport flux V_tr (LeftJacobian-variantA (34)), its decomposition against K + s⁺ and the base flux, and the exact transition dichotomy (LeftJacobian-variantA (35)).

theorem AVenhance.Infra.Section5.LeftJacobian.transport_window_identity (κ : ℝ) (K J C F : Matrix (Fin 2) (Fin 2) ℝ) (g : Homogenization.Vec 2) : (κ • F + F.transpose * (K - κ • 1) * F).mulVec g + F.transpose.mulVec ((J - K).mulVec (F.mulVec g)) = (κ • F + F.transpose * (C - κ • 1) * F).mulVec g + F.transpose.mulVec ((J - C).mulVec (F.mulVec g))

Per-window vector identity: adding the Fᵀ(JHat-K)F g correction to (κF + Fᵀ(K-κ)F) g trades K for 𝒥 (flux) at the price of Fᵀ(JHat - 𝒥)F g.

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

LeftJacobian-variantA (34)–(35), pointwise: (K + s⁺)∇T + Σ_l ξ̂_l Fᵀ(JHat - K)F∇T equals V_tr plus the first summand of d⁺ (sourceErrorDPlus). Composes with Kmat_add_sMatPlus_mulVec and amnrBasePlus_qMNR_sum.

theorem AVenhance.Infra.Section5.LeftJacobian.sourceErrorDPlus_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : sourceErrorDPlus I hΦ m κm T t x = ∑' (l : ℤ), I.hatXiML m l t • (I.flowGrad hΦ m l t x).transpose.mulVec ((I.Jhat κm m t - I.flux κm m t).mulVec ((I.flowGrad hΦ m l t x).mulVec (spaceGrad (T t) x))) + fun (i : Fin 2) => ∑ n ∈ Finset.range (Nstar β), ∑ j : Fin 2, ∑ k : Fin 2, I.Amnr hΦ m κm n T (Jcut β) t x i j k * I.qMNR κm m n (Jcut β) t j k

sourceErrorDPlus is its first (transport-correction) summand plus the terminal A_{Jcut} q_{Jcut} tail.

theorem AVenhance.Infra.Section5.LeftJacobian.sum_xiMK_odd_support {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (t : ℝ) : ∑ q ∈ ⋯.toFinset, I.xiMK m (↑q) t = 1

The odd transition weights sum to one over their finite support.

theorem AVenhance.Infra.Section5.LeftJacobian.Transport.xFlowInv_right_inverse_at' {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : I.xFlow hΦ m l t (I.xFlowInv hΦ m l t x) = x

theorem AVenhance.Infra.Section5.LeftJacobian.G_eq_flowGrad_mulVec_of_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hT : ContDiff ℝ 1 (T t)) (l : ℤ) (y : Homogenization.Vec 2) : G I hΦ m T l t y = (I.flowGrad hΦ m l t y).mulVec (spaceGrad (T t) y)

G_l = F_l ∇T for T t of class C¹.

theorem AVenhance.Infra.Section5.LeftJacobian.piola_form_mulVec (κ : ℝ) (P F : Matrix (Fin 2) (Fin 2) ℝ) (g : Homogenization.Vec 2) : (κ • F + F.transpose * P * F).mulVec g = (κ • 1 + F.transpose * P).mulVec (F.mulVec g)

(κ F + Fᵀ P F) g = (κ I + Fᵀ P)(F g).

theorem AVenhance.Infra.Section5.LeftJacobian.transportFluxPlus_eq_selected {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hT : ContDiff ℝ 1 (T t)) (y : Homogenization.Vec 2) : transportFluxPlus I hΦ m κm T t y = ∑ q ∈ ⋯.toFinset, I.xiMK m (↑q) t • (κm • 1 + (flowGradK I hΦ m (↑q) t y).transpose * (I.flux κm m t - κm • 1)).mulVec (G I hΦ m T (lIdx β I.Λ m ↑q) t y) + r46Flux I hΦ m κm T t y