High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.DirichletHoleInhabitant

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

The inhabitant of the restated Dirichlet clause

Every row of's table is now a producer, and this module assembles them. The law-free constant is

C₀ s₀ ρ Rad := max 0 (frozenHeadC0Factor C d s₀ ρ Rad (1/(3√d)) Cdual
                        (Chardy s₀ ρ Rad).toReal) + 1

— strictly positive by construction, and a function of (s₀, ρ, Rad) alone; C is the energy's d-level constant, Cdual the d-level duality constant, and Chardy is (s₀, ρ, Rad)-level Hardy constant. The per-g data are

Lg   := perGLengthFactor (frozenHeadLgFactor d g κ) κ ,
pEcc := foldedFrameEccentricityExponent g κ + (d + 1 + q) / κ ,
       q := witnessErrorEccentricityExponent g κ .

The row-by-row supply, against the hole's own binders:

binder from the modules named above	producer
hgood, hS, √δ ≤ 1	RootInterface.RootGoodScale.provider_surface
hscale : x ≤ ε⁻¹	RootInterface.scale_le_of_foldedScale_le
system, hU, hUnonempty, hRad, hUhatMeas, hUhat0	—
hGauge	—
u, huGrad	—
uHat, hHat, huHat, hhHat	—
aObs, hObs	—
aCell, wCell, hfamily	that module (via row 4′)
hEnergy	—
hBoundaryTop	—
hHardy	—
hFdefect	—
hDual	the duality constant
hhead	that module, from the modules named above+the KenergyBound premise
the hole's shape	that module + that module (double absorptions)

theorem HCPolySupport.HighContrast.RowSupply.dirichletHole_inhabited (d : ℕ) [NeZero d] : DirichletHole d (RootInterface.RootGoodScale d)

The restated internal Dirichlet clause is inhabited.