High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.PrintOrderLocalCauchy

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

theorem HCPolySupport.HighContrast.successorInner_energy_eq_direct_restriction {d : ℕ} [NeZero d] (a : Book.Ch03.CoeffFamily d) (m r : ℤ) (e : Vec d) (hr : r ≤ m - 1 - 2) : finiteCenteredCubeSolutionEnergy a (m - 1 - 2) (successorInnerRestriction a m e) r = Book.Ch03.h1EnergyNormOnCube (originCube d r) a (finiteCubeSolutionRestriction a ⋯ (finiteAffineSuccessorDifference a m e)).toH1

theorem HCPolySupport.HighContrast.identityGaugeFiniteCorrectionLocalCauchy (d : ℕ) [NeZero d] (g : ℝ) (geom : RoundedGenerationAnalyticGeometry d) (hg : g ∈ Set.Ico 0 1) (hdual : PrintOrderRoundedReferenceDualRegularityAtGeneration d g geom.generation) (aGauge : CoeffSpace d) (hI : Matrix.PosDef (symmPart 1)) (aIdentity : Book.Ch03.CoeffFamily d) (hIdentity : ∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace 1 hI aGauge)) (delta : ℝ) (n : ℤ) (hdelta : delta ∈ Set.Ioc 0 (identitySuccessorSmallness d g geom hg hdual)) (hgood : ScalarIdentityGoodTail aIdentity (printCertificateOrder g) delta n) : FiniteAffineCorrectionLocalCauchy aIdentity

At the printed order, the exact identity-gauge successor estimate makes the literal finite-corrector sequence locally Cauchy.