High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.CorrectorComposition.ReconciledSmallnessCertificate
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The reconciled-smallness certificate: the assembly at the reconciled #
corrector smallness #
The restated assembly RootInterface.polynomial_homogenization_of_quenched_scale_v2
takes GoodScale as a parameter bound before g. The the ceiling-exporting smallness
interface ceiling
therefore cannot be a constant chosen after g — but it can be cStar g for a
function cStar : ℝ → ℝ bound before GoodScale. That is what
reconciledRootGoodScale is.
hhomogenized is then proved at this certificate, character for character
in the assembly's binder shape, checked by the partial application below,
which supplies hquenched and hhomogenized and leaves exactly the six
clauses.
The reconciled root certificate. The c-parameterised printed-order
certificate, read at the reconciled g-indexed corrector smallness.
Equations
- One or more equations did not get rendered due to their size.