High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.ExactRootGaugeTerminalPieces

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

Small pieces the large-scale C¹ slope approximation terminal assembly needs

Three facts, each one step:

• the joint local limit at slope 0 has vanishing gradient representative (finiteAffineCorrectionJointLocalLimit_smul at c = 0), which is what makes the degenerate case of the terminal — the one where the whole radius range sits in the near-terminal band — closable with eRef := 0 and no triangle inequality at all;
• a triadic cube contained in the exact-root pullback ball has exact-root image inside the ellipsoid, so the terminal cube solution applies;
• the affine-coefficient field of the certificate's reference family is a.e. the identity-gauge family's, cube by cube — the bridge every energy comparison in the two branch estimates consumes.

theorem HCPolySupport.HighContrast.CorrectorComposition.jointLimit_zero_grad_ae {d : ℕ} [NeZero d] {aId : Book.Ch02.TriadicCoeffFamily d} (hCauchy : FiniteAffineCorrectionLocalCauchy aId) (Phi : Vec d → NormalizedLocalH1Carrier d) (hPhi : IsFiniteAffineCorrectionJointLocalEquation aId Phi) : (Phi 0).globalGradientRepresentative =ᵐ[MeasureTheory.volume] fun (x : Vec d) => 0

The corrector at slope 0 is trivial.

theorem HCPolySupport.HighContrast.CorrectorComposition.matImage_subset_ellipsoid_of_subset_closedNormBall {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {R : ℝ} {S : Set (Vec d)} (h : S ⊆ closedNormBall d R) : matImage (Selection.normalizedRoot (symmPart abar)) S ⊆ ellipsoid abar R

The terminal cube solution's geometric premise.

theorem HCPolySupport.HighContrast.CorrectorComposition.exactRootCoeff_ae_identityGauge {d : ℕ} [NeZero d] (geom : RoundedGenerationAnalyticGeometry d) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {a : CoeffSpace d} (hI : Matrix.PosDef (symmPart 1)) (aIdentity : Book.Ch03.CoeffFamily d) (hIdentity : ∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace 1 hI (exactGaugeCoeffSpace a abar hS))) (Q : TriadicCube d) : affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS) =ᵐ[MeasureTheory.volume] (aIdentity.coeffOn Q).toCoeffField

The coefficient bridge. The exact-root affine coefficient is a.e. the identity-gauge family's coefficient on every triadic cube.