High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PushforwardEngineInput

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The engine's Liouville input at a real translation

Clause (1) of the stationary corrector family clause — integer stationarity of the pushforward family — is one application of the translated-gradient identification engine at the real translation matVecMul (gaugeRoot abar)⁻¹ (Source.AKL.intTranslation z). The engine's free translation binder accepts it; what has to be produced is its Liouville input at the translated sample.

This module reduces that input to a single named statement: that the Liouville class transports along a translation by an arbitrary real vector. Everything gauge-theoretic is discharged here by the real-vector conjugation.

The 0 < theta binder is necessary. Quantifying theta over all of ℝ makes the statement false: take b any elliptic field, v = 0, Dv = 0, theta = -1 and c = 1. The hypothesis holds — the growth row reads r ^ 0 * ‖0‖ → 0 — while the conclusion requires r ^ 0 * ‖-1‖ = 1 → 0. The same failure occurs for every theta ≤ -1. The defect is exactly the additive recentring: the growth row is scale-invariant at theta = -1, so a nonzero constant is not absorbed. The 0 < theta binder below repairs it, is what the printed Liouville class carries (ϑ ∈ (0,1)), and is supplied by the consumer at rootCorrectorGrowth = 1/2; engine_liouville_input_of_realTranslate carries the same binder.

def HCPolySupport.HighContrast.Root.RealTranslateLiouville (d : ℕ) : Prop

P4, as a named residue. The Liouville class transports along a translation by an arbitrary real vector, the coefficient field translating with it and an additive constant absorbing the affine part. The available statements — memLiouvilleClass_affineAdd_of_cubeGrowth and memLiouvilleClass_realTranslate_subConst — give the integer case bundled with a growth row; this is the bare translation.

The 0 < theta binder is necessary: without it the statement is false for the additive recentring at every theta ≤ -1.

Equations

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

theorem HCPolySupport.HighContrast.Root.isAELocallyUniformlyElliptic_gaugeCoeff_translate {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (z : Fin d → ℤ) : IsAELocallyUniformlyElliptic fun (y : Vec d) => gaugeCoeff a abar hS (y + matVecMul (gaugeRoot abar)⁻¹ (Source.AKL.intTranslation z))

The translated normalized-gauge coefficient is locally uniformly elliptic.

theorem HCPolySupport.HighContrast.Root.engine_liouville_input_of_realTranslate {d : ℕ} [NeZero d] (hT : RealTranslateLiouville d) (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (G : NormalizedLocalH1Carrier d) (e : Vec d) {theta : ℝ} (htheta : 0 < theta) (hLiou : MemLiouvilleClass (gaugeCoeff a abar hS) theta (fun (y : Vec d) => vecDot (matVecMul (gaugeRoot abar) e) y + G.globalValueRepresentative y) fun (y : Vec d) => matVecMul (gaugeRoot abar) e + G.globalGradientRepresentative y) (z : Fin d → ℤ) : MemLiouvilleClass (gaugeCoeff (translateCoeff z a) abar hS) theta (fun (y : Vec d) => vecDot (matVecMul (gaugeRoot abar) e) y + G.globalValueRepresentative (y + matVecMul (gaugeRoot abar)⁻¹ (Source.AKL.intTranslation z))) fun (y : Vec d) => matVecMul (gaugeRoot abar) e + G.globalGradientRepresentative (y + matVecMul (gaugeRoot abar)⁻¹ (Source.AKL.intTranslation z))

Clause (1)'s engine input, from the single residue. On the translated sample the normalized-gauge Liouville membership needed by the translated-gradient identification engine follows from the untranslated one, with no hypothesis beyond RealTranslateLiouville.