High-contrast homogenization: Provider.PolynomialHomogenization.RootInterface.ProviderSurface

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

The Dirichlet provider's binder surface, and what it consumes

Two checks on the restated interface.

(1) What RootGoodScale hands the provider. Every row the capstone's hypothesis table marks as required is supplied: the row-retaining certificate itself, the positive-definiteness of symmPart abar (recovered from the certificate, which opens with ∃ hS : (symmPart abar).PosDef), the corrector threshold window c ∈ Ioo 0 1, and the retained row's amplitude window delta ∈ Ioo 0 1 — the last being the one the row-retaining structure itself does not carry (it carries only 0 ≤ delta).

(2) That the capstone's proved bound feeds the interface clause. The clause reads its rate factor at x * (Lg * eccentricityFoldFactor abar pEcc); the capstone proves the bound at x * eccentricityFoldFactor abar p₀. Since the rate factor is increasing in the scale and the constant may be enlarged, any Lg ≥ 1 and any pEcc ≥ p₀ transfer the proved bound to the hole's shape, and the hole's ε-premise is stronger than the capstone's hscale : x ≤ ε⁻¹.

The fold factor is monotone in its exponent

theorem HCPolySupport.HighContrast.RootInterface.eccentricityFoldFactor_mono {d : ℕ} (abar : Mat d) {p q : ℝ} (hp : 0 ≤ p) (hpq : p ≤ q) : RowSupply.eccentricityFoldFactor abar p ≤ RowSupply.eccentricityFoldFactor abar q

(1) The provider's binder surface

theorem HCPolySupport.HighContrast.RootInterface.RootGoodScale.provider_surface {d : ℕ} [NeZero d] {g kappaRate : ℝ} {abar : Mat d} {a : CoeffSpace d} {x : ℝ} (h : RootGoodScale d g kappaRate abar a x) : ∃ (c : ℝ) (hh : RowSupply.RowRetainingPrintOrderGoodScale d g c kappaRate abar a x), c ∈ Set.Ioo 0 1 ∧ hh.delta ∈ Set.Ioo 0 1 ∧ Matrix.PosDef (symmPart abar) ∧ 0 ≤ hh.delta ∧ 1 ≤ hh.activationScale a ∧ hh.sourceScale a ≤ hh.activationScale a ∧ hh.activationScale a ≤ x ∧ Quenched.HasAllLaterPhysicalBlockRow (Certificate.printRowOrder g) (2 * kappaRate) hh.delta (Book.Ch02.constantBlockMatrix abar) hh.sourceScale hh.activationScale a

Everything the Dirichlet provider needs from the certificate.

(2) What the surface consumes

theorem HCPolySupport.HighContrast.RootInterface.scale_le_of_foldedScale_le {d : ℕ} {abar : Mat d} {x Lg pEcc epsilon : ℝ} (hx : 0 ≤ x) (hLg : 1 ≤ Lg) (h : x * (Lg * RowSupply.eccentricityFoldFactor abar pEcc) ≤ epsilon⁻¹) : x ≤ epsilon⁻¹

The clause's ε-premise implies the capstone's.