High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.WitnessRouteEnergyCollapse

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

The witness-route Kenergy, collapsed at a law-free amplitude listed five factors of the

scheduled-rate head. Four were in hand; the fifth — Kenergy ≤ law-free × E^{d+2s₀+2q} — was blocked because collapse applies to the shape gaugeWitnessEnergyPriceW C d s₀ (A · E^q) abar and that shape was produced by nothing, last row). The module now produces exactly that shape, with A = lambdaRouteClaw · (witnessGeometricFactor · frameFoldConstant).

This module supplies the two pieces of glue that module did not carry:

• witnessRouteCwit_eq_amplitude_mul_pow — the associativity that exhibits witnessRouteCwit in shape, with q = witnessErrorEccentricityExponent g κ;
• collapsedEnergyLawFree_mono — monotonicity of the collapsed law-free constant in its amplitude, so that any law-free upper bound for A may be substituted after the collapse.

The combination is witnessRouteEnergyPrice_le_collapsed: the price at the witness-route Cwit is below collapsedEnergyLawFree C d s₀ Alaw times a fixed power of the witness eccentricity, for any Alaw dominating the amplitude. The only thing left in the fifth factor is the explicit law-free Alaw, whose three factors are each already (EnergyPrice.observationFillingCoefficient_le_of_residualWindow for the λ-route constant, the witnessGeometricFactor_le_uniform premise for the geometric factor, and the max_one_rpow_three_bracket_le premise for the bracket factor of frameFoldConstant).

theorem HCPolySupport.HighContrast.RowSupply.witnessRouteCwit_eq_amplitude_mul_pow (d : ℕ) (Claw Cgeo g kappaRate J : ℝ) (abar : Mat d) : witnessRouteCwit d Claw Cgeo g kappaRate J abar = Claw * (Cgeo * frameFoldConstant d g kappaRate J) * max 1 (witnessEccentricity (symmPart abar)) ^ witnessErrorEccentricityExponent g kappaRate

The witness-route Cwit in collapse shape.

theorem HCPolySupport.HighContrast.RowSupply.witnessErrorEccentricityExponent_nonneg {g kappaRate : ℝ} (hkappa : 0 < kappaRate) (hrho : 0 ≤ Certificate.printRowOrder g) : 0 ≤ witnessErrorEccentricityExponent g kappaRate

The witness-error eccentricity exponent is nonnegative on the printed window.

theorem HCPolySupport.HighContrast.RowSupply.collapsedEnergyLawFree_mono {d : ℕ} (C : ℝ) {s A B : ℝ} (hs : 0 < s) (hA : 0 ≤ A) (hAB : A ≤ B) : collapsedEnergyLawFree C d s A ≤ collapsedEnergyLawFree C d s B

The collapsed law-free constant is monotone in its amplitude.

theorem HCPolySupport.HighContrast.RowSupply.witnessRouteEnergyPrice_le_collapsed {d : ℕ} (C : ℝ) {g kappaRate s₀ Claw Cgeo J Alaw : ℝ} {abar : Mat d} (hs : 0 < s₀) (hkappa : 0 < kappaRate) (hrho : 0 ≤ Certificate.printRowOrder g) (hsd : 0 ≤ ↑d + 2 * s₀) (hA0 : 0 ≤ Claw * (Cgeo * frameFoldConstant d g kappaRate J)) (hAle : Claw * (Cgeo * frameFoldConstant d g kappaRate J) ≤ Alaw) : EnergyPrice.gaugeWitnessEnergyPriceW C d s₀ (witnessRouteCwit d Claw Cgeo g kappaRate J abar) abar ≤ collapsedEnergyLawFree C d s₀ Alaw * max 1 (witnessEccentricity (symmPart abar)) ^ (↑d + 2 * s₀ + 2 * witnessErrorEccentricityExponent g kappaRate)

The fifth factor, in hand. The witness-route energy price collapses to a law-free constant times a fixed power of the witness eccentricity, at any law-free amplitude dominating the route's own.