flow and cutoff specializations of the corrector diffusion rule.

theorem AVenhance.Infra.Section5.frozen_corrector_diffusion_column_divergence_flow {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (κ : ℝ) (j : Fin 2) {LB LD LE : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hB : HasFDerivAt (frozenCorrectorFlux I κ m k j t) LB (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x)) (hD : HasFDerivAt (correctorDefectColumn I hΦ m k t κ j) LD x) (hE : HasFDerivAt (correctorShearCrossColumn I hΦ m k t κ j) LE x) (hdiv : ∀ (r : ℝ) (y : Homogenization.Vec 2), Flow.spatialDivergence (streamVel (Φ (m - 1))) r y = 0) : matDiv (correctorFlux I hΦ m κ k t) 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

The per-index corrector diffusion identity with the cofactor Piola hypothesis discharged from the C² inverse-flow slice. The remaining differentiability premises are precisely those of the three flux pieces in the product rule.

theorem AVenhance.Infra.Section5.diffusionMatrix_selected_corrector_column_divergence {β : ℝ} (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) {LB LD LE : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hB : HasFDerivAt (frozenCorrectorFlux I κ m k j t) LB (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x)) (hD : HasFDerivAt (correctorDefectColumn I hΦ m k t κ j) LD x) (hE : HasFDerivAt (correctorShearCrossColumn I hΦ m k t κ j) LE x) (hdiv : ∀ (r : ℝ) (y : Homogenization.Vec 2), Flow.spatialDivergence (streamVel (Φ (m - 1))) r y = 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

The source's selected diffusion column agrees with the per-index corrector flux column on the support of its odd cutoff, so the corrected divergence expansion applies directly to the full twisted diffusion matrix.