Named terms in the Section 5.1 residual identity.

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

The flow-pulled gradient G_l = ∇(T ∘ X_l) ∘ X_l⁻¹.

Equations

• AVenhance.Infra.Section5.G I hΦ m T l t x = AVenhance.spaceGrad (fun (y : Homogenization.Vec 2) => T t (I.xFlow hΦ m l t y)) (I.xFlowInv hΦ m l t x)

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

The spatial derivative matrix of G_l, with coordinate derivatives in rows.

Equations

• AVenhance.Infra.Section5.gradG I hΦ m T l t x = Matrix.of fun (i j : Fin 2) => AVenhance.spaceGrad (fun (y : Homogenization.Vec 2) => AVenhance.Infra.Section5.G I hΦ m T l t y j) x i

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

The scalar coefficient ψTilde_m obtained by pulling each ψ_{m,k} back along the l_k inverse flow.

Equations

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

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

The diffusion matrix in the ansatz equation.

Equations

• AVenhance.Infra.Section5.diffusionMatrix I hΦ m κm t x = κm • 1 + AVenhance.Infra.Section5.psiTilde I hΦ m t x • AVenhance.sigmaMat

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

The twisted corrector-gradient matrix ∇ΧTilde_{m,k}.

Equations

• AVenhance.Infra.Section5.gradChiTilde I hΦ m κm k t x = AVenhance.gradMatrix (I.chiTilde hΦ m κm k t) x

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

The l_k flow-gradient matrix ∇X_{m-1,l_k} ∘ X⁻¹_{m-1,l_k}.

Equations

• AVenhance.Infra.Section5.flowGradK I hΦ m k t x = I.flowGrad hΦ m (AVenhance.lIdx β I.Λ m k) t x

noncomputable def AVenhance.Infra.Section5.gradDiv (V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The spatial gradient of the divergence of a vector field.

Equations

• AVenhance.Infra.Section5.gradDiv V t x = AVenhance.spaceGrad (fun (y : Homogenization.Vec 2) => AVenhance.vecDiv (V t) y) x

noncomputable def AVenhance.Infra.Section5.matDiv (A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

Column-wise divergence of a matrix field: the flux coordinate is differentiated and the column/corrector index is returned. This is the convention in the per-corrector flux equation.

Equations

• AVenhance.Infra.Section5.matDiv A x j = ∑ i : Fin 2, AVenhance.spaceGrad (fun (y : Homogenization.Vec 2) => A y i j) x i

def AVenhance.Infra.Section5.frob (A B : Matrix (Fin 2) (Fin 2) ℝ) : ℝ

Frobenius contraction, matching the : convention in Section 5.1.

Equations

• AVenhance.Infra.Section5.frob A B = ∑ i : Fin 2, ∑ j : Fin 2, A i j * B i j

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

The centered flow average used in the correction.

Equations

• AVenhance.Infra.Section5.Gbar I hΦ m T t x = ∑' (l : ℤ), I.hatXiML m l t • AVenhance.Infra.Section5.G I hΦ m T l t x

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

The flux matrix attached to the k-th corrector in its cutoff window.

Equations

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

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

cutoff1, the time-cutoff derivative term.

Equations

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

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

twistie1, the transport of T_{m-1} through the l_k flow.

Equations

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

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

twistie3 in the Σ_k ξ_{m,k} form for the line-2 ansatz. The source's printed l-average is the line-1 hybrid; with the line 2, the gradient defect is ∇T - G_{l_k}. Under this slot keeps its body: it is the repaired twistie3⁺ = -div Σ_k ξ_k p_k σ (∇T - G_k) plus the molecular divergence 𝓜 = div(κ Σ_k ξ_k (F_k - I)∇T) of the corrected formulation (37) (LeftJacobian.twistie3_eq), so the ten slot names are unchanged.

Equations

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

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

twistie4ND, the non-divergence inverse-flow corrector-gradient error -Σ_k ξ_k G_k · Div D_k. In the corrected form, twistie4 = twistie4ND - Σ_k ξ_k D_k : ∇G_k (LeftJacobian.twistie4Plus_eq).

Equations

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

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

twistie5ND, the non-divergence push-forward Jacobian error -Σ_k ξ_k G_k · Div E_k (since twistie5 = twistie5ND - Σ_k ξ_k E_k : ∇G_k). The gradMatrix convention stores coordinate derivatives in rows, so the Piola push-forward acts by the transpose on vector fields. This is the corrected orientation of the source's I - ∇X factor (see PushforwardOrientation).

Equations

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

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

twistie4 (the corrected formulation §7, twistie4⁺): -div Σ_k ξ_k D_k G_k with the inverse-flow corrector defect D_k = κ (∇Y_{l_k} - I)(∇χ_k ∘ Y_{l_k}).

Equations

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

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

twistie5 (the corrected formulation §7, twistie5⁺): -div Σ_k ξ_k E_k G_k with the push-forward Jacobian error E_k = (I - F_kᵀ)(p_k σ + κ ∇χ_k ∘ Y_{l_k}) (transpose orientation: see PushforwardOrientation).

Equations

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

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

The rank-two product ΧTilde_k ∇G_{l_k}, contracted as a vector before applying the diffusion matrix.

Equations

• AVenhance.Infra.Section5.chiGradG I hΦ m κm T k t x i = ∑ j : Fin 2, I.chiTilde hΦ m κm k t x j * AVenhance.Infra.Section5.gradG I hΦ m T (AVenhance.lIdx β I.Λ m k) t x i j

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

normie1, the corrector times the Hessian term.

Equations

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

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

normie2, the diffusion of the H_m corrector.

Equations

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

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

tiny, the residual generated by the two forcing fields.

Equations

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

noncomputable def AVenhance.Infra.Section5.selCoeff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The selected cell coefficient p_k = ζ̂_{l_k} ζ_k ψ_k ∘ Y_{l_k} (the corrected formulation §7).

Equations

• AVenhance.Infra.Section5.selCoeff I hΦ m k t x = I.hatZetaML m (AVenhance.lIdx β I.Λ m k) t * I.zetaMK m k t * AVenhance.psi β I.Λ m k (I.xFlowInv hΦ m (AVenhance.lIdx β I.Λ m k) t x)

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

The unpulled cell flux C⁰_k = (κ I + p_k σ)(I + B_k), B_k = (∇χ_k) ∘ Y_{l_k} (the corrected formulation §7): the cell flux integrand evaluated at Y_{l_k}.

Equations

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

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

normie3 (the corrected formulation §7, normie3⁺): Σ_k ξ_k F_kᵀ (𝒥 - C⁰_k) : ∇G_k. Its fast factor 𝒥 - C⁰_k has exact zero cell mean (LeftJacobian.cellFluxCell_fastFactor_mean_zero). This corrects (𝒥 - C_k) : ∇G_k, whose slow part misses the left Jacobian.

Equations

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

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

The transition-window remainder in divergence form.

Equations

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

noncomputable def AVenhance.Infra.Section5.nineTerms {β : ℝ} (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) : ℝ

Sum of the nine residual terms, using the line-2 ansatz.

Equations

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

def AVenhance.Infra.Section5.residualIdentity {β : ℝ} (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 Section 5.1 target proposition with the named residual terms. The source-specific theorem establishing it is kept separate from this statement.

Equations

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