High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PushforwardFamilyClauses

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

the stationary corrector family clause at the pushforward marker

The identity-gauge producer reduces the clause to RootNormalizedSupply, which is a change of comparison matrix: it asks the certificate for an identity-gauge weak-error row, while the root's certificate supplies an abar-gauge one, and no lemma transports between the two.

This module executes the architectural repair. The physical corrector is defined as the affine pushforward of the normalized-gauge one, so the certificate-side demand becomes the normalized-gauge datum the converter already produces.

clause of the hole	discharged by
marker	the definitional record of the pushforward pair
slope linearity	rootJointCarrier_add/_smul through pushforwardGradient_linear_ae
integer covariance	pushforwardCarrier_gradient_translate_ae
weak-gradient pair on univ	hasWeakGradientOn_univ_pushforward
corrector equation on univ	pushforward_isWeakSolutionOn

The integer-covariance clause is the delicate one: in the normalized gauge an integer translation of the physical sample is a translation by the real vector L⁻¹ z, and the Liouville input at a real translation is exactly what RealTranslateLiouville supplies.

Slope linearity

theorem HCPolySupport.HighContrast.Root.pushforwardPhysicalGradPhi_linear (d : ℕ) [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (c : ℝ) (e e' : Vec d) (a : CoeffSpace d) : pushforwardPhysicalGradPhi d abar hS (c • e + e') a =ᵐ[MeasureTheory.volume] fun (x : Vec d) => c • pushforwardPhysicalGradPhi d abar hS e a x + pushforwardPhysicalGradPhi d abar hS e' a x

The pushforward gradient family is slope-linear on every sample.

Integer covariance

theorem HCPolySupport.HighContrast.Root.pushforwardPhysicalGradPhi_stationary (d : ℕ) [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (z : Fin d → ℤ) (e : Vec d) (a : CoeffSpace d) : pushforwardPhysicalGradPhi d abar hS e (translateCoeff z a) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => pushforwardPhysicalGradPhi d abar hS e a (x + Source.AKL.intTranslation z)

Integer covariance of the pushforward gradient family. An integer translation of the physical sample is, in the normalized gauge, a translation by the real vector L⁻¹ z; the identification at that real translation is pushforwardCarrier_gradient_translate_ae.

The marker and the hole

def HCPolySupport.HighContrast.Root.RootPushCorrectorFamily (d : ℕ) [NeZero d] (abar : Mat d) (Phi : Vec d → CoeffSpace d → Vec d → ℝ) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d) : Prop

The pushforward construction marker. The definitional record of the one pushforward pair attached to abar. No certificate, order, rate, law, sample or scale occurs.

Equations

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

def HCPolySupport.HighContrast.Root.RootPushCorrectorFamilyPredicate (d : ℕ) [NeZero d] : Mat d → (Vec d → CoeffSpace d → Vec d → ℝ) → (Vec d → CoeffSpace d → Vec d → Vec d) → Prop

The root's corrector-family predicate, re-pointed at the pushforward marker.

Equations

• HCPolySupport.HighContrast.Root.RootPushCorrectorFamilyPredicate d = HCPolySupport.HighContrast.Root.RootPushCorrectorFamily d

def HCPolySupport.HighContrast.Root.RootNormalizedSupply (d : ℕ) [NeZero d] (GoodScale : Mat d → CoeffSpace d → ℝ → Prop) : Prop

The certificate-side supply the pushforward producer needs. It is the normalized-gauge datum — what exists_shiftedNormalizedReferencePowerTail_of_hasAllLaterPhysicalBlockRow produces from the root's abar-comparison block row, and not the identity-gauge row the identity-gauge producer asks for.

Equations

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

theorem HCPolySupport.HighContrast.Root.correctorFamilyHole_of_normalizedSupply (d : ℕ) [NeZero d] (GoodScale : Mat d → CoeffSpace d → ℝ → Prop) (hsupply : RootNormalizedSupply d GoodScale) (abar : Mat d) : Matrix.PosDef (symmPart abar) → ∃ (Phi : Vec d → CoeffSpace d → Vec d → ℝ) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d), RootPushCorrectorFamilyPredicate d abar Phi gradPhi ∧ (∀ (c : ℝ) (e e' : Vec d) (a : CoeffSpace d), gradPhi (c • e + e') a =ᵐ[MeasureTheory.volume] fun (x : Vec d) => c • gradPhi e a x + gradPhi e' a x) ∧ (∀ (z : Fin d → ℤ) (e : Vec d) (a : CoeffSpace d), gradPhi e (translateCoeff z a) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => gradPhi e a (x + Source.AKL.intTranslation z)) ∧ ∀ (a : CoeffSpace d) (x : ℝ), GoodScale abar a x → ∀ (e : Vec d), HasWeakGradientOn Set.univ (Phi e a) (gradPhi e a) ∧ IsWeakSolutionOn (fun (y : Vec d) => ↑↑a y) Set.univ fun (y : Vec d) => e + gradPhi e a y

the stationary corrector family clause of the root assembly, at the pushforward marker. Every clause is discharged; the only certificate-side input is the normalized-gauge datum, quantified after the marker and the family have been chosen, so no scale datum precedes the construction.