Algebraic decomposition of the per-index corrector diffusion matrix.

theorem AVenhance.Infra.Section5.shear_corrector_flux_matrix_expansion (κ q : ℝ) (H C : Matrix (Fin 2) (Fin 2) ℝ) : (κ • 1 + q • sigmaMat) * (1 + H * C) = κ • 1 + (q • sigmaMat + κ • C) + κ • ((H - 1) * C) + q • sigmaMat * (H * C)

Expand the diffusion matrix times the twisted corrector gradient into the base corrector flux, inverse-flow gradient defect, and shear cross term.

theorem AVenhance.Infra.Section5.shear_cross_flux_vecDiv_eq_zero {ψ f : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (hψ : DifferentiableAt ℝ ψ x) (hf : ContDiffAt ℝ 2 f x) (horth : Homogenization.vecDot (spaceGrad ψ x) (sigmaMat.mulVec (spaceGrad f x)) = 0) : vecDiv (fun (y : Homogenization.Vec 2) => (ψ y • sigmaMat).mulVec (spaceGrad f y)) x = 0

The shear cross flux has zero divergence whenever its two scalar potentials obey the skew-gradient orthogonality used by the corrector.

theorem AVenhance.Infra.Section5.frozen_corrector_diffusion_matrix_expansion {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (κ : ℝ) : correctorFlux I hΦ m κ k t x = κ • 1 + ((I.zetaProd m k t * psi β I.Λ m k (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x)) • sigmaMat + κ • gradMatrix (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y) (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x)) + κ • ((gradMatrix (I.xFlowInv hΦ m (lIdx β I.Λ m k) t) x - 1) * gradMatrix (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y) (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x)) + (I.zetaProd m k t * psi β I.Λ m k (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x)) • sigmaMat * (gradMatrix (I.xFlowInv hΦ m (lIdx β I.Λ m k) t) x * gradMatrix (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y) (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x))

The k-th diffusion-corrector matrix splits into its base corrector flux, inverse-flow gradient defect, and shear cross term.