High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.ConstantAbsorptionIntoLength

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

The C₀ absorptions: absorbing the per-g constants into the length

bound carries the constant Cscheduled produced by the flux scheduled rate at the witness, which is

Cscheduled = 2 · outputFactor · Cdual · Cbesov d · √Kflux · √hardyConstant

(HCPoly.Provider.PolynomialHomogenization.Root.RowSupply.UniformFluxScheduledRateExtraction, with Cbesov d = fractionalDualToBesovConstant d and D = Cbesov d ^ 2). The restated hole, on the other hand, needs a single C₀ with ∀ s₀ ρ Rad, 0 < C₀ s₀ ρ Rad, fixed before g and before the domain.

The factors split into five classes:

• (a) law-free and admissible in C₀ s₀ ρ Rad: 2, Cdual (dimension only, by the Cdual module's F1 absorptions), Cbesov d, and √hardyConstant, whose selector exists_ruledHardySelection fixes it from (d, ρ, Rad, s) alone — exactly C₀'s permitted dependence;
• (b) the rate factor (ε · x · …) ^ κ, already the hole's own;
• (c) boundaryEnergy ^ (1/2), already the hole's own right-hand factor;
• (d) law-free but g-dependent: everything in Kframe beyond (a) — the orders r, b = responseWindowOrder g, the rate kappaRate, Rad, cnorm, the certificate amplitude √h.delta, the bracket J, and frameFoldConstant/foldedResponseFillingConstant;
• (e) the eccentricity: √Kenergy from the frozen-witness price at the eccentricity constant Cwit.

outputFactor is in none of them: it cancels against the physical-frame transport.

This module supplies the absorption itself. Classes (d) and (e) are a single nonnegative real Krest; the lemma below moves it into the length as a factor perGLengthFactor Krest kappa, which is exactly the per-g law-free length factor the root-interface modules is adding. The 0 ≤ versus 0 < defect is repaired in the same step by C₀ + 1.

noncomputable def HCPolySupport.HighContrast.RowSupply.perGLengthFactor (Krest kappa : ℝ) : ℝ

The per-g length factor that absorbs a nonnegative constant at the rate kappa: the kappa-th root of the constant, truncated at one.

Equations

• HCPolySupport.HighContrast.RowSupply.perGLengthFactor Krest kappa = max 1 Krest ^ kappa⁻¹

theorem HCPolySupport.HighContrast.RowSupply.one_le_perGLengthFactor (Krest : ℝ) {kappa : ℝ} (hkappa : 0 < kappa) : 1 ≤ perGLengthFactor Krest kappa

theorem HCPolySupport.HighContrast.RowSupply.perGLengthFactor_nonneg (Krest : ℝ) {kappa : ℝ} (hkappa : 0 < kappa) : 0 ≤ perGLengthFactor Krest kappa

theorem HCPolySupport.HighContrast.RowSupply.perGLengthFactor_rpow (Krest : ℝ) {kappa : ℝ} (hkappa : 0 < kappa) : perGLengthFactor Krest kappa ^ kappa = max 1 Krest

The defining property: raised to the rate, the length factor is the truncated constant it absorbs.

theorem HCPolySupport.HighContrast.RowSupply.constant_absorbed_into_length {C0 Krest epsilon x fold kappa : ℝ} (hC0 : 0 ≤ C0) (hkappa : 0 < kappa) (heps : 0 ≤ epsilon) (hx : 0 ≤ x) (hfold : 0 ≤ fold) : C0 * Krest * (epsilon * (x * fold)) ^ kappa ≤ C0 * (epsilon * (x * perGLengthFactor Krest kappa * fold)) ^ kappa

The absorption. A per-g constant multiplying the rate factor is moved into the length, leaving the law-free constant alone in front.