: the literal-name residual identity (36) from the material and diffusion expansions.

This is the corrected-form analogue of frozen_residual_identity_of_expansions: the hnorm step is replaced by the identity Σ_q ξ_q (κ I + F_qᵀ P) : ∇G_q - Σ_q ξ_q C_q : ∇G_q = normie3Sel, and the averaged transport contraction is replaced by the divergence of the coarse transport flux V_tr (transportFluxPlus), which is evaluated through the Piola column lemma.

theorem AVenhance.Infra.Section5.LeftJacobian.Assembly.vecDot_comm' (u v : Homogenization.Vec 2) : Homogenization.vecDot u v = Homogenization.vecDot v u

theorem AVenhance.Infra.Section5.LeftJacobian.Assembly.asm_frob_sub_left (A B C : Matrix (Fin 2) (Fin 2) ℝ) : frob (A - B) C = frob A C - frob B C

frob is additive-subtractive in its first slot.

theorem AVenhance.Infra.Section5.LeftJacobian.Assembly.asm_piola_mulVec_differentiableAt {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t : ℝ) (P : Matrix (Fin 2) (Fin 2) ℝ) (κm : ℝ) (V : Homogenization.Vec 2 → Homogenization.Vec 2) (x : Homogenization.Vec 2) (hV : DifferentiableAt ℝ V x) : DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => (κm • 1 + (flowGradK I hΦ m k t y).transpose * P).mulVec (V y)) x

The field y ↦ (κ I + F_k(y)ᵀ P) V(y) is differentiable at x when V is.

theorem AVenhance.Infra.Section5.LeftJacobian.Assembly.asm_transportFluxPlus_differentiableAt {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hT : ContDiff ℝ 1 (T t)) (x : Homogenization.Vec 2) (hG : ∀ q ∈ ⋯.toFinset, DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => G I hΦ m T (lIdx β I.Λ m ↑q) t y) x) (hr46 : DifferentiableAt ℝ (r46Flux I hΦ m κm T t) x) : DifferentiableAt ℝ (transportFluxPlus I hΦ m κm T t) x

V_tr is differentiable at x under the regularity hypotheses of the divergence formula.

theorem AVenhance.Infra.Section5.LeftJacobian.Assembly.asm_vecDiv_transportFluxPlus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hT : ContDiff ℝ 1 (T t)) (x : Homogenization.Vec 2) (hG : ∀ q ∈ ⋯.toFinset, DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => G I hΦ m T (lIdx β I.Λ m ↑q) t y) x) (hr46 : DifferentiableAt ℝ (r46Flux I hΦ m κm T t) x) : vecDiv (transportFluxPlus I hΦ m κm T t) x = ∑ q ∈ ⋯.toFinset, I.xiMK m (↑q) t * frob (κm • 1 + (flowGradK I hΦ m (↑q) t x).transpose * (I.flux κm m t - κm • 1)) (gradG I hΦ m T (lIdx β I.Λ m ↑q) t x) + R46 I hΦ m κm T t x

The divergence of the coarse transport flux V_tr at x: the finite Piola sum of ξ_q (κ I + F_qᵀ P) : ∇G_q plus the transition remainder R46.

theorem AVenhance.Infra.Section5.LeftJacobian.variantA_residual_identity_sel_of_expansions {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) (S : Finset { k : ℤ // Odd k }) (hS : S = ⋯.toFinset) (hpartition : ∑ q ∈ S, I.xiMK m (↑q) t = 1) (hgradDivSplit : gradDiv (fun (s : ℝ) (y : Homogenization.Vec 2) => (I.Kmat κ m s + I.sMat hΦ m κ s y).mulVec (spaceGrad (T s) y) + e s y) t x = gradDiv (fun (s : ℝ) (y : Homogenization.Vec 2) => (I.Kmat κ m s + I.sMat hΦ m κ s y).mulVec (spaceGrad (T s) y)) t x + gradDiv e t x) (hmaterial : deriv (fun (s : ℝ) => I.ansatz hΦ m κ T s x) t + Homogenization.vecDot (streamVel (Φ (m - 1)) t x) (spaceGrad (I.ansatz hΦ m κ T t) x) = cutoff1 I hΦ m κ T t x + ∑ q ∈ S, I.xiMK m (↑q) t * Homogenization.vecDot (fun (j : Fin 2) => deriv (fun (s : ℝ) => I.chiMK κ m (↑q) s (I.xFlowInv hΦ m (lIdx β I.Λ m ↑q) t x) j) t) (G I hΦ m T (lIdx β I.Λ m ↑q) t x) + ∑ q ∈ S, I.xiMK m (↑q) t * Homogenization.vecDot (I.chiTilde hΦ m κ (↑q) t x) ((I.flowGrad hΦ m (lIdx β I.Λ m ↑q) t x).mulVec (gradDiv (fun (s : ℝ) (y : Homogenization.Vec 2) => (I.Kmat κ m s + I.sMat hΦ m κ s y).mulVec (spaceGrad (T s) y) + e s y) t x)) + vecDiv (fun (y : Homogenization.Vec 2) => transportFluxPlus I hΦ m κ T t y + d t y + e t y) x) (hdiffusion : vecDiv (fun (y : Homogenization.Vec 2) => (diffusionMatrix I hΦ m κ t y).mulVec (spaceGrad (I.ansatz hΦ m κ T t) y)) x = ∑ q ∈ S, I.xiMK m (↑q) t * Homogenization.vecDot (matDiv (correctorDefectMatrix I hΦ m (↑q) t κ) x) (G I hΦ m T (lIdx β I.Λ m ↑q) t x) + ∑ q ∈ S, I.xiMK m (↑q) t * Homogenization.vecDot (matDiv (correctorPushforwardMatrix I hΦ m (↑q) t κ) x) (G I hΦ m T (lIdx β I.Λ m ↑q) t x) + ∑ q ∈ S, I.xiMK m (↑q) t * frob (correctorFlux I hΦ m κ (↑q) t x) (gradG I hΦ m T (lIdx β I.Λ m ↑q) t x) + ∑ q ∈ S, I.xiMK m (↑q) t * Homogenization.vecDot (fun (j : Fin 2) => deriv (fun (s : ℝ) => I.chiMK κ m (↑q) s (I.xFlowInv hΦ m (lIdx β I.Λ m ↑q) t x) j) t) (G I hΦ m T (lIdx β I.Λ m ↑q) t x) - twistie3 I hΦ m κ T t x - normie1 I hΦ m κ T t x - normie2 I hΦ m κ T t x) (hT : ContDiff ℝ 1 (T t)) (hG : ∀ q ∈ ⋯.toFinset, DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => G I hΦ m T (lIdx β I.Λ m ↑q) t y) x) (hr46 : DifferentiableAt ℝ (r46Flux I hΦ m κ T t) x) (hde : DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => d t y + e t y) x) (hAnsatz : ContDiffAt ℝ 2 (I.ansatz hΦ m κ T t) x) : residualIdentitySel I hΦ m κ T d e (streamVel (Φ m)) t x

corrected-form literal residual identity (36) from the two expansions.

Hypotheses, all of the shape of frozen_residual_identity_of_expansions except as noted:

• hS, hpartition: S is the finite support of the odd transition weights at time t, and those weights sum to one on it.
• hgradDivSplit: the coefficient I.sMat splits gradDiv against e (a differentiability fact, identical to the one; no sMatPlus is needed here).
• hmaterial: the source material expansion, with the averaged-flux term replaced by the divergence of V_tr + d + e (transportFluxPlus).
• hdiffusion: the selected diffusion expansion, identical to the one.
• hT: T t is C¹ (so G_l = F_l ∇T and V_tr has its selected form).
• hG: each G_q, q ∈ S, is differentiable at x.
• hr46: the transition flux r46Flux is differentiable at x.
• hde: d t + e t is differentiable at x.
• hAnsatz: the ansatz is C² at x (for the operator divergence split).