: the literal split (36) implies the repaired split (38).

For 1 ≤ m and a spatially smooth T t, the literal-name nine terms (twistie3, twistie4, twistie5, normie3Sel) differ from the revised nine terms (twistie3⁺, twistie4⁺, twistie5⁺, normie3⁺) exactly by the molecular divergence 𝓜:

• twistie4⁺ = twistie4 - Σ_k ξ_k D_k : ∇G_k and twistie5⁺ = twistie5 - Σ_k ξ_k E_k : ∇G_k (product rule on div (A_k G_k), over the finite odd support);
• twistie3 = twistie3⁺ + 𝓜 (ψTilde = p_k on supp ξ_k, and κ (∇T - G_k) = -κ (F_k - I) ∇T);
• normie3Sel = normie3⁺ - Σ_k ξ_k (D_k + E_k) : ∇G_k (normie3Sel_eq).

The only analytic hypothesis is ContDiff ℝ ∞ (T t); all flow, corrector and cutoff regularity is discharged from the smoothness lemmas.

Differentiable calculus helpers

theorem AVenhance.Infra.Section5.LeftJacobian.differentiableAt_mulVec_of_entries {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {V : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} (hA : ∀ (i j : Fin 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => A y i j) x) (hV : DifferentiableAt ℝ V x) : DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => (A y).mulVec (V y)) x

theorem AVenhance.Infra.Section5.LeftJacobian.vecDiv_sub_of_differentiableAt {V W : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} (hV : DifferentiableAt ℝ V x) (hW : DifferentiableAt ℝ W x) : vecDiv (fun (y : Homogenization.Vec 2) => V y - W y) x = vecDiv V x - vecDiv W x

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

theorem AVenhance.Infra.Section5.LeftJacobian.tsum_xi_mul_eq_sum {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (t : ℝ) (f : { k : ℤ // Odd k } → ℝ) : ∑' (q : { k : ℤ // Odd k }), I.xiMK m (↑q) t * f q = ∑ q ∈ ⋯.toFinset, I.xiMK m (↑q) t * f q

∑' over odd modes with a cutoff factor is the finite sum over the odd support.

theorem AVenhance.Infra.Section5.LeftJacobian.vecDiv_selected_matrix_vec {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (t : ℝ) (A : ℤ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (Gf : ℤ → Homogenization.Vec 2 → Homogenization.Vec 2) (x : Homogenization.Vec 2) (hA : ∀ (k : ℤ) (i j : Fin 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => A k y i j) x) (hG : ∀ (k : ℤ), DifferentiableAt ℝ (Gf k) x) : vecDiv (fun (y : Homogenization.Vec 2) => ∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t • (A (↑k) y).mulVec (Gf (↑k) y)) x = ∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t * Homogenization.vecDot (matDiv (A ↑k) x) (Gf (↑k) x) + ∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t * frob (A (↑k) x) (gradMatrix (Gf ↑k) x)

Product rule for the divergence of Σ_k ξ_k A_k G_k over the odd cutoff support.

twistie4⁺ and twistie5⁺

theorem AVenhance.Infra.Section5.LeftJacobian.twistie4Plus_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) (hT : ContDiff ℝ (↑⊤) (T t)) : twistie4Plus I hΦ m κm T t x = twistie4ND 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)

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

twistie3 = twistie3⁺ + 𝓜

theorem AVenhance.Infra.Section5.LeftJacobian.twistie3_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) (hT : ContDiff ℝ (↑⊤) (T t)) : twistie3 I hΦ m κm T t x = twistie3Plus I hΦ m κm T t x + molecular I hΦ m κm T t x

The regrouping (36) ⇒ (38)

theorem AVenhance.Infra.Section5.LeftJacobian.nineTermsSel_eq_nineTermsPlus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) (hT : ContDiff ℝ (↑⊤) (T t)) : nineTermsSel I hΦ m κm T d e t x = nineTermsPlus I hΦ m κm T d e t x + molecular I hΦ m κm T t x

The literal-name nine terms (36) equal the repaired nine terms (38) plus the molecular divergence 𝓜. The only hypotheses are 1 ≤ m and spatial smoothness of T t.

theorem AVenhance.Infra.Section5.LeftJacobian.residualIdentityPlus_of_sel {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) (hT : ContDiff ℝ (↑⊤) (T t)) : residualIdentitySel I hΦ m κm T d e b t x → residualIdentityPlus I hΦ m κm T d e b t x

Literal-name residual identity (36) implies the repaired identity (38).

The named-slot identity

With the slot definitions of Terms.lean (twistie4 = twistie4⁺, twistie5 = twistie5⁺, normie3 = normie3⁺, definitionally) and twistie3 = twistie3⁺ + 𝓜, the nine terms are the repaired nine terms plus 𝓜.

theorem AVenhance.Infra.Section5.LeftJacobian.nineTerms_eq_nineTermsPlus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) (hT : ContDiff ℝ (↑⊤) (T t)) : nineTerms I hΦ m κm T d e t x = nineTermsPlus I hΦ m κm T d e t x + molecular I hΦ m κm T t x

nineTerms = nineTermsPlus + 𝓜 (the ten slot names carry the repaired split (38)).

theorem AVenhance.Infra.Section5.LeftJacobian.residualIdentity_iff_plus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) (hT : ContDiff ℝ (↑⊤) (T t)) : residualIdentity I hΦ m κm T d e b t x ↔ residualIdentityPlus I hΦ m κm T d e b t x

The repaired identity (38) is the named-slot residualIdentity.