Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.CorrectorDecay.TargetedGaugeSpine

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.CorrectorDecay.TargetedGaugeSpine

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

source
theorem HCPolySupport.HighContrast.exists_targetedIdentityGaugeJointLimit (d : ℕ) [NeZero d] (g : ℝ) (hg : g ∈ Set.Ico 0 1) :
have c := canonicalCorrectorSmallness d g hg; ∀ (kappa : ℝ) (abar : Mat d) (a : CoeffSpace d) (x : ℝ), PrintOrderQuantitativeNormalizedReferenceCertificate abar g (correctorTargetAmplitude c kappa) kappa x a → ∃ (hS : Matrix.PosDef (symmPart abar)) (hI : Matrix.PosDef (symmPart 1)) (aIdentity : Book.Ch03.CoeffFamily d), (∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑((canonicalIdentityGeometry d g hg).centeredCoeffSpace 1 hI (exactGaugeCoeffSpace a abar hS))) ∧ ScalarIdentityPowerTail aIdentity (printCertificateOrder g) (correctorTargetAmplitude c kappa) kappa x ∧ ∃ (Phi : Vec d → NormalizedLocalH1Carrier d), IsFiniteAffineCorrectionJointLocalEquation aIdentity Phi

A target-amplitude certificate constructs the canonical identity-gauge joint corrector at its own (pre-affine) effective scale. This is the exact variant needed to retain the affine multiplier for the later physical negative-one transport.