High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.FrozenWitnessEnergyPriceAssembly

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

The frozen-witness energy price, with the analytic inputs discharged

Modules that module–that module closed, one by one, every item listed as open in hypothesis surface. This module composes them: the energy price is produced from the clause's own binders alone, together with two definitional constraints on the gauge carriers (haHat, huHat) — which are binders, not new hypotheses.

The chain, in order:

step	producer
the physical realization u of (uFun, uGrad)	—
the gauge weak solution at aHat (row 4′)	—
the cube pullbacks gObs (of g₀) and uObs (of u)	—
hBesov, hL2 for gObs.grad	—
the observation family, hb and hObs at scaledCoeff ε a	—
the zero-trace difference	—
the Dirichlet forced cube solution v	—
the ε/λ reconciliation, the certificate destructurings, and the price	—

FTrans is the canonical transported datum w ↦ S (g₀.grad (S w)), and g0grad := g₀.grad; the two FTrans premises are gradient identity and the frozenWitnessFrameTransport premise.

theorem HCPolySupport.HighContrast.RowSupply.exists_frozenWitnessEnergyPrice_atHoleBinders (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 < C ∧ ∀ (g c kappaRate : ℝ) (abar : Mat d) (a : CoeffSpace d) (x epsilon : ℝ) (hgood : RowRetainingPrintOrderGoodScale d g c kappaRate abar a x) (hS : Matrix.PosDef (symmPart abar)) (U : Set (Vec d)) (j : ℤ) (z : Vec d) (rho Rad s₀ : ℝ) (J : ℕ) (g₀ h : H1Function U) (uFun : Vec d → ℝ) (uGrad : Vec d → Vec d) (uHat : H1Function (matImage (matSqrt (symmPart abar))⁻¹ U)), hgood.delta ∈ Set.Ioo 0 1 → g ∈ Set.Ico 0 1 → 0 < kappaRate → 1 ≤ x → 0 < epsilon → x ≤ epsilon⁻¹ → s₀ ∈ Set.Ico ((1 + g) / 4) (1 / 2) → 2 * Rad ≤ 3 ^ ↑J → U = (fun (y : Vec d) => z + matVecMul (matSqrt (symmPart abar)) y) '' openCubeSet (originCube d j) → U ⊆ ellipsoid abar 1 → ellipsoid abar (1 / (3 * √↑d)) ⊆ U → HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) rho Rad → hsNormSq U s₀ g₀.grad ≠ ⊤ → MemAffineH10 U g₀ h → (MemH1a0 (scaledCoeff epsilon a) U (fun (y : Vec d) => uFun y - g₀.toFun y) fun (y : Vec d) => uGrad y - g₀.grad y) → IsWeakSolutionOn (scaledCoeff epsilon a) U uGrad → (uHat.grad = fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (uGrad (matVecMul (matSqrt (symmPart abar)) y))) → ∃ lambda ∈ Set.Icc 1 3, GaugePhysicalEnergyPriceAtWitness (matImage (matSqrt (symmPart abar))⁻¹ U) (affineCoefficient (matSqrt (symmPart abar)) ⋯ fun (w : Vec d) => scaledCoeff epsilon a w - skewPart abar) uHat (EnergyPrice.gaugeWitnessEnergyPriceW C d s₀ (witnessRouteCwit d (lambdaRouteClaw d (responseWindowOrder g) lambda abar) (witnessGeometricFactor d rho (responseWindowOrder g)) g kappaRate (↑J) abar) abar) (hsNormSq U s₀ fun (w : Vec d) => matVecMul (matSqrt (symmPart abar)) (g₀.grad w))

The frozen-witness energy price at the hole's binders. No Group-B hypothesis survives: v, hBesov, hL2, hb, hu, hF, hFrame and the ε-shaped observation identification are all produced inside.