Candidate objects for the corrected formulation, sharing existing definitions where equal.

These names reuse the corrected Section 4 and Section 5 objects of the corrected formulation §2, §7 and §9. sMatPlus and amnrBasePlus become the sMat and the zero branch of Amnr (rfl); the theorems of Section5/LeftJacobian take the equalities I.sMat = sMatPlus and I.Amnr · 0 = amnrBasePlus as hypotheses, which are then discharged by rfl. Every other object below keeps its meaning.

noncomputable def AVenhance.Infra.Section5.LeftJacobian.sMatPlus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm t : ℝ) (x : Homogenization.Vec 2) : Matrix (Fin 2) (Fin 2) ℝ

Candidate corrected-form coarse coefficient, the corrected formulation (4) and §9.1: s⁺ = K Σ_l ξ̂_l (F_l - I) + Σ_l ξ̂_l (F_lᵀ - I)(K - κ I) F_l.

Equations

• AVenhance.Infra.Section5.LeftJacobian.sMatPlus I hΦ m κm t x = I.sMat hΦ m κm t x

noncomputable def AVenhance.Infra.Section5.LeftJacobian.coarseFluxPlus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm t : ℝ) (x : Homogenization.Vec 2) : Matrix (Fin 2) (Fin 2) ℝ

The Piola form of the coarse coefficient, 𝓚⁺ = Σ_l ξ̂_l [κ F_l + F_lᵀ (K - κ) F_l] (the corrected formulation (4)).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section5.LeftJacobian.amnrBasePlus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (n : ℕ) (Tm1 : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) (i j k : Fin 2) : ℝ

Candidate corrected-form base tensor A⁺_{n,0}^{ijk} = -L_n Σ_l ξ̂_l (F_l)_{ji} (F_l ∇T)_k (the corrected formulation (7), §9.2; index form flowGrad … j i).

Equations

• AVenhance.Infra.Section5.LeftJacobian.amnrBasePlus I hΦ m κm n Tm1 t x i j k = I.Amnr hΦ m κm n Tm1 0 t x i j k

noncomputable def AVenhance.Infra.Section5.LeftJacobian.sourceErrorDPlus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The corrected-form forcing error d⁺, the corrected formulation (9) and the §9.4 body.

Equations

• AVenhance.Infra.Section5.LeftJacobian.sourceErrorDPlus I hΦ m κm T t x = AVenhance.Infra.Section5.sourceErrorD I hΦ m κm T t x

noncomputable def AVenhance.Infra.Section5.LeftJacobian.transportFluxPlus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The coarse transport flux V_tr = Σ_l ξ̂_l [κ F_l + F_lᵀ P F_l] ∇T, P = 𝒥 - κ (the corrected formulation (34)).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section5.LeftJacobian.twistie3Plus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (_κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

twistie3⁺ = -div Σ_k ξ_k p_k σ (∇T - G_k).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section5.LeftJacobian.twistie4Plus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

twistie4⁺ = -div Σ_k ξ_k D_k G_k, D_k = κ (Q_k - I) B_k.

Equations

• AVenhance.Infra.Section5.LeftJacobian.twistie4Plus I hΦ m κm T t x = AVenhance.Infra.Section5.twistie4 I hΦ m κm T t x

noncomputable def AVenhance.Infra.Section5.LeftJacobian.twistie5Plus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

twistie5⁺ = -div Σ_k ξ_k E_k G_k, E_k = (I - F_kᵀ)(p_k σ + κ B_k).

Equations

• AVenhance.Infra.Section5.LeftJacobian.twistie5Plus I hΦ m κm T t x = AVenhance.Infra.Section5.twistie5 I hΦ m κm T t x

noncomputable def AVenhance.Infra.Section5.LeftJacobian.normie3Plus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

normie3⁺ = Σ_k ξ_k F_kᵀ (𝒥 - C⁰_k) : ∇G_k. Its fast factor 𝒥 - C⁰_k has exact zero cell mean (the corrected formulation §7).

Equations

• AVenhance.Infra.Section5.LeftJacobian.normie3Plus I hΦ m κm T t x = AVenhance.Infra.Section5.normie3 I hΦ m κm T t x

noncomputable def AVenhance.Infra.Section5.LeftJacobian.normie3Sel {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The literal-name normie3 of the corrected formulation (36) and §9.4: N_sel⁺ = Σ_k ξ_k (κ I + F_kᵀ P - C_k) : ∇G_k.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section5.LeftJacobian.molecular {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The molecular divergence 𝓜 = div(κ Σ_k ξ_k (F_k - I) ∇T), the corrected formulation (37).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section5.LeftJacobian.nineTermsSel {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The nine terms in the literal-name split (36): the names, with normie3 replaced by normie3Sel (§9.4).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Section5.LeftJacobian.nineTermsPlus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The nine revised terms of the corrected formulation §7 table, in the slot order (cutoff1, twistie1, twistie3, twistie4, twistie5, normie1, normie2, tiny, normie3).

Equations

• One or more equations did not get rendered due to their size.

def AVenhance.Infra.Section5.LeftJacobian.residualIdentitySel {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) : Prop

The literal-name corrected-form residual identity (36).

Equations

• One or more equations did not get rendered due to their size.

def AVenhance.Infra.Section5.LeftJacobian.residualIdentityPlus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) : Prop

The repaired corrected-form residual identity (38): nine revised terms, R46 and 𝓜.

Equations

• One or more equations did not get rendered due to their size.

Identifications

The candidates are the Section 4 and Section 5 objects, definitionally.

theorem AVenhance.Infra.Section5.LeftJacobian.sMat_eq_sMatPlus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm t : ℝ) (x : Homogenization.Vec 2) : I.sMat hΦ m κm t x = sMatPlus I hΦ m κm t x

theorem AVenhance.Infra.Section5.LeftJacobian.Amnr_zero_eq_amnrBasePlus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (n : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) (i j k : Fin 2) : I.Amnr hΦ m κm n T 0 t x i j k = amnrBasePlus I hΦ m κm n T t x i j k

theorem AVenhance.Infra.Section5.LeftJacobian.twistie4Plus_eq_twistie4 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : twistie4Plus I hΦ m κm T t x = twistie4 I hΦ m κm T t x

theorem AVenhance.Infra.Section5.LeftJacobian.twistie5Plus_eq_twistie5 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : twistie5Plus I hΦ m κm T t x = twistie5 I hΦ m κm T t x

theorem AVenhance.Infra.Section5.LeftJacobian.normie3Plus_eq_normie3 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : normie3Plus I hΦ m κm T t x = normie3 I hΦ m κm T t x