High-contrast homogenization:

Provider.PolynomialHomogenization.RootInterface.GoodScaleInstantiation

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

The root certificate, instantiated

GoodScale is instantiated at the row-retaining printed-order certificate: the printed-order rate-bearing certificate at the common affine scale, carrying alongside it the physical block row that produced it. That row is exactly what the Dirichlet provider consumes and what no producer supplied.

With this instantiation the root's hhomogenized hypothesis is proved, not assumed — at the enlarged scale forced by the common affine multiplier, whose law-free amplitude and eccentricity power are the Lcert, pCert the restated interface exports.

The certificate rate is min (kappa / 2) ((1 + g) / 4): the printed conversion halves the quenched row rate, and the frozen order window s₀ ∈ Ico ((1+g)/4) (1/2) caps the Dirichlet exponent at (1+g)/4. Both the certificate and the row are downward closed in the rate, so the minimum is available.

def HCPolySupport.HighContrast.RootInterface.RootGoodScale (d : ℕ) [NeZero d] (g kappaRate : ℝ) (abar : Mat d) (a : CoeffSpace d) (x : ℝ) : Prop

The root certificate. The printed-order rate-bearing certificate at the common affine scale, with the producing physical block row retained, and with the row's own amplitude window delta ∈ Ioo 0 1 exposed — the Dirichlet provider reads √delta ≤ 1 off it, and the row-retaining structure carries only 0 ≤ delta.

Equations

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

noncomputable def HCPolySupport.HighContrast.RootInterface.rootCertificateRate (g kappa : ℝ) : ℝ

The certificate rate the root exports: the halved quenched row rate, capped at the frozen order window's left endpoint.

Equations

• HCPolySupport.HighContrast.RootInterface.rootCertificateRate g kappa = min (kappa / 2) ((1 + g) / 4)

theorem HCPolySupport.HighContrast.RootInterface.rootCertificateRate_pos {g kappa : ℝ} (hg : g ∈ Set.Ico 0 1) (hkappa : 0 < kappa) : 0 < rootCertificateRate g kappa

theorem HCPolySupport.HighContrast.RootInterface.rootCertificateRate_le {g kappa : ℝ} : rootCertificateRate g kappa ≤ (1 + g) / 4