High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.DirichletHoleConsumption

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

The restated negative-Sobolev Dirichlet error clause, transcribed, and its

acceptance check

An earlier form of the clause took GoodScale : Mat d → CoeffSpace d → ℝ → Prop, ∃ κ, length x * eccentricityFoldFactor abar pEcc). The root-interface module's the current form replaces it: GoodScale threads g and the rate, κ is a ∀-binder capped at (1 + g)/4, and the enlarged length carries a per-g factor Lg ≥ 1 beside the fold.

DirichletHole below is that slot, transcribed from RootInterface.RootAssemblyV2.polynomial_homogenization_of_quenched_scale_v2 The consumption theorem below is the fail-closed check that the transcription is the slot: it feeds a DirichletHole into the root theorem's seventh binder, so any deviation — a renamed binder, a moved premise, a different rate factor — is an elaboration error, not a silent mismatch.

This module does not inhabit the hole. It fixes its statement in this module so later supplies can be measured against it.

def HCPolySupport.HighContrast.RowSupply.DirichletHole (d : ℕ) (GoodScale : ℝ → ℝ → Mat d → CoeffSpace d → ℝ → Prop) : Prop

The restated internal Dirichlet clause, transcribed from the root assembly.

Equations

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