High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.RootCertificateAndFoldAbsorption

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

(iii) the certificate surface, and the Lg/pEcc double absorptions

(iii). RootInterface.RootGoodScale.provider_surface hands the Dirichlet provider everything the certificate side of the module asks for. Two of its eight conclusions are the ones no other module supplies: the positive-definiteness of symmPart abar, and the retained row's amplitude window delta ∈ Ioo 0 1 — from which √δ ≤ 1, the hypothesis the module needs to drop the certificate amplitude out of the flux constant. The Dirichlet-surface packaging supplies exactly those.

The double absorptions. The module proves the frozen conclusion at the capstone's own length x * eccentricityFoldFactor abar p₀ and at whatever constant the caller passes. The clause wants it at x * (Lg * eccentricityFoldFactor abar pEcc) with C₀ law-free. The two moves that get there are already separately — that module absorptions a law-free residual Krest into the length factor at the rate κ, and that module absorptions an eccentricity power into the fold exponent — and constant_and_eccentricity_absorbed performs them in one step, with

Lg   := perGLengthFactor Krest κ ,      pEcc := p₀ + p / κ .

That is the dispatch's "pEcc := the sum of the rate-leg and energy-leg exponents": p₀ is the rate leg (foldedFrameEccentricityExponent g κ), and p / κ is the energy leg together with the output factor's (d+1)/2, divided by κ because the rate factor takes the κ-th power.

(iii) The certificate surface

The double absorptions

theorem HCPolySupport.HighContrast.RowSupply.constant_and_eccentricity_absorbed {d : ℕ} (abar : Mat d) {Claw Krest p p0 kappa epsilon x : ℝ} (hClaw : 0 ≤ Claw) (hkappa : 0 < kappa) (hp : 0 ≤ p) (hp0 : 0 ≤ p0) (heps : 0 ≤ epsilon) (hx : 0 ≤ x) : Claw * max 1 (witnessEccentricity (symmPart abar)) ^ p * Krest * (epsilon * (x * eccentricityFoldFactor abar p0)) ^ kappa ≤ Claw * (epsilon * (x * (perGLengthFactor Krest kappa * eccentricityFoldFactor abar (p0 + p / kappa)))) ^ kappa

The Lg/pEcc double absorptions. A law-free residual constant and an eccentricity power standing beside the law-free head are absorbed, the first into the per-g length factor and the second into the fold exponent, leaving the head alone in front of the clause's rate factor.