High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.FrozenWitnessPriceAtWitnessRoute

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

The frozen-witness energy price, with the transported row supplied

that module supplied the price at an eccentricity-shaped Cwit, taking the λ-route's observation-error bound (hErr) and the sign 0 ≤ j as binders. The route refuted the sign; this module replaces both:

• hErr is now produced, by the λ-route composition of HCPoly.Provider.PolynomialHomogenization.Root.Dirichlet.WitnessLambdaRouteComposition (21a);
• the 3 ^ (−r j) factor is paid by the law-free geometric factor of HCPoly.Provider.PolynomialHomogenization.Root.Dirichlet.WitnessCubeTwoSidedGeometry (21c′), through that module.

The resulting price has no analytic binder from the row: every hypothesis is either on the domain surface, an output of the response-window tail, an identification of the observation family, or one of the energy's own transport binders.

The one constraint this exposes. The composition fixes the observation order to responseWindowOrder g, because that reference tail is at that order; the frozen clause's boundary energy is at s₀ ∈ Ico ((1+g)/4) (1/2), and responseWindowOrder g = (3+5g)/16 < (1+g)/4 for every g < 1. The price produced here is therefore at the response-window order. Transporting it to the printed s₀ is a separate obligation and is not performed here.

The witness generation is below the outer bracket

theorem HCPolySupport.HighContrast.RowSupply.cubeScale_le_two_mul_Rad {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} {rho Rad : ℝ} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) (hsandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) rho Rad) : 3 ^ j ≤ 2 * Rad

The witness cube side is at most twice the outer sandwich radius.

theorem HCPolySupport.HighContrast.RowSupply.witnessGeneration_le_bracket {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} {rho Rad : ℝ} {J : ℕ} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) (hsandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) rho Rad) (hJ : 2 * Rad ≤ 3 ^ ↑J) : j ≤ ↑J

With the anchored provider's outer bracket 2 Rad ≤ 3 ^ J, the witness generation is below J.

The Cwit the witness route supports

noncomputable def HCPolySupport.HighContrast.RowSupply.witnessRouteCwit (d : ℕ) (Claw Cgeo g kappaRate J : ℝ) (abar : Mat d) : ℝ

The witness route's Cwit: the λ-route filling constant, the law-free geometric factor, the frame fold, and a fixed power of the witness eccentricity.

Equations

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

theorem HCPolySupport.HighContrast.RowSupply.witnessRouteCwit_nonneg (d : ℕ) {Claw Cgeo : ℝ} (hClaw : 0 ≤ Claw) (hCgeo : 0 ≤ Cgeo) (g kappaRate J : ℝ) (abar : Mat d) : 0 ≤ witnessRouteCwit d Claw Cgeo g kappaRate J abar

The price, with row 21 supplied