: the exact cell-flux identity (33) and the normie3 split.

For every odd (indeed every) k, with Q = ∇Y_{l_k}, F = F_{l_k}, B = (∇χ_k) ∘ Y_{l_k}, p = selCoeff, the determinant-one/Piola identity σ Q = Fᵀ σ gives C_k = Fᵀ C⁰_k + κ (I - Fᵀ) + D_k + E_k (the corrected formulation (33)). Consequently the literal-name normie3Sel equals the centered normie3Plus minus the two defect contractions. All statements are unconditional: smoothness of χ_k and of the inverse flow is supplied by FrozenFlowRegularity and Section3.chiMK_component_contDiff_two.

theorem AVenhance.Infra.Section5.LeftJacobian.sigmaMat_mul_eq_rowCofactor_mul (Q : Matrix (Fin 2) (Fin 2) ℝ) : sigmaMat * Q = rowCofactor Q * sigmaMat

σ Q = cof(Q) σ for every 2 × 2 matrix: the algebraic core of σ Q = Fᵀ σ.

theorem AVenhance.Infra.Section5.LeftJacobian.cellFlux_algebra (κ p : ℝ) (Ft Q B : Matrix (Fin 2) (Fin 2) ℝ) (hσ : sigmaMat * Q = Ft * sigmaMat) : (κ • 1 + p • sigmaMat) * (1 + Q * B) = Ft * ((κ • 1 + p • sigmaMat) * (1 + B)) + κ • (1 - Ft) + κ • ((Q - 1) * B) + (1 - Ft) * (p • sigmaMat + κ • B)

Pure matrix algebra behind (33): from σ Q = Fᵀ σ.

theorem AVenhance.Infra.Section5.LeftJacobian.sigmaMat_mul_gradMatrix_xFlowInv {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : sigmaMat * gradMatrix (I.xFlowInv hΦ m l t) x = (I.flowGrad hΦ m l t x).transpose * sigmaMat

The inverse flow's row-Jacobian satisfies σ ∇Y = Fᵀ σ (det one).

theorem AVenhance.Infra.Section5.LeftJacobian.chiMK_differentiable {β : ℝ} (I : Ingredients β) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) (z : Homogenization.Vec 2) : DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y) z

Each corrector χ_k(t, ·) is differentiable (indeed C²).

theorem AVenhance.Infra.Section5.LeftJacobian.correctorFlux_eq_cellFlux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : correctorFlux I hΦ m κm k t x = (flowGradK I hΦ m k t x).transpose * cellFlux I hΦ m κm k t x + κm • (1 - (flowGradK I hΦ m k t x).transpose) + correctorDefectMatrix I hΦ m k t κm x + correctorPushforwardMatrix I hΦ m k t κm x

Exact identity (33): C_k = F_kᵀ C⁰_k + κ (I - F_kᵀ) + D_k + E_k.

The normie3 split

theorem AVenhance.Infra.Section5.LeftJacobian.frob_sub_left (A B G : Matrix (Fin 2) (Fin 2) ℝ) : frob (A - B) G = frob A G - frob B G

theorem AVenhance.Infra.Section5.LeftJacobian.frob_add_left (A B G : Matrix (Fin 2) (Fin 2) ℝ) : frob (A + B) G = frob A G + frob B G

theorem AVenhance.Infra.Section5.LeftJacobian.normie3_matrix_split {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : κm • 1 + (flowGradK I hΦ m k t x).transpose * (I.flux κm m t - κm • 1) - correctorFlux I hΦ m κm k t x = (flowGradK I hΦ m k t x).transpose * (I.flux κm m t - cellFlux I hΦ m κm k t x) - correctorDefectMatrix I hΦ m k t κm x - correctorPushforwardMatrix I hΦ m k t κm x

The matrix split: κ I + Fᵀ(𝒥 - κ I) - C_k = Fᵀ(𝒥 - C⁰_k) - D_k - E_k.

theorem AVenhance.Infra.Section5.LeftJacobian.normie3Sel_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : normie3Sel I hΦ m κm T t x = normie3Plus I hΦ m κm T t x - ∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t * (frob (correctorDefectMatrix I hΦ m (↑k) t κm x) (gradG I hΦ m T (lIdx β I.Λ m ↑k) t x) + frob (correctorPushforwardMatrix I hΦ m (↑k) t κm x) (gradG I hΦ m T (lIdx β I.Λ m ↑k) t x))

The literal-name normie3 equals the centered normie3⁺ minus the two defect contractions Σ_k ξ_k (D_k + E_k) : ∇G_k.