The selected corrector diffusion expansion with all flow-divergence inputs derived from the stream sequence.

theorem AVenhance.Infra.Section5.diffusionMatrix_selected_corrector_column_divergence_source {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (κ : ℝ) (j : Fin 2) (hk : Odd k) (hxi : I.xiMK m k t ≠ 0) : matDiv (fun (y : Homogenization.Vec 2) => diffusionMatrix I hΦ m κ t y * (1 + gradChiTilde I hΦ m κ k t y)) x j = deriv (fun (s : ℝ) => I.chiMK κ m k s (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x) j) t + matDiv (correctorDefectMatrix I hΦ m k t κ) x j + matDiv (correctorPushforwardMatrix I hΦ m k t κ) x j

At a nonzero odd cutoff, the source diffusion column expands into the corrector time derivative and its inverse-flow and Piola error divergences. The classical divergence-free property is derived from IsStreamSeq.