High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.ExplicitFrozenFrameDirichletBound

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

(δ), part three: the frozen Dirichlet conclusion body at an explicit C₀

The module composes the physical-frame transport from the modules named above with the gauge-side terminal bound from the modules named above, at outputFactor := √(hsAffineFactor (matSqrt (symmPart abar))⁻¹ s ‖matSqrt (symmPart abar)‖). The composition is unchanged here; only the terminal bound is swapped for module that module's, which carries C₀ as a parameter.

The result is the conclusion body of the frozen Dirichlet conjunct, at the folded homogenization length and at a constant the caller chooses — which is what the restated Dirichlet clause's binder order requires. The Hardy-top premise is not a hypothesis.

theorem HCPolySupport.HighContrast.RowSupply.RowRetainingPrintOrderGoodScale.explicit_foldedFrozenFrameDirichletBound_of_energy {d : ℕ} [NeZero d] {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)) (hg : g ∈ Set.Ico 0 1) (hkappa : 0 < kappaRate) (hx : 1 ≤ x) (hepsilon : 0 < epsilon) (hscale : x ≤ epsilon⁻¹) (hd : 1 ≤ d) {Uphys Uhat : Set (Vec d)} (hUhat : Uhat = matImage (matSqrt (symmPart abar))⁻¹ Uphys) (hUhatMeas : MeasurableSet Uhat) (hUhat0 : MeasureTheory.volume Uhat ≠ 0) {rho Rad s : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem Uhat rho Rad) (hU : IsOpenBoundedConvexDomain Uhat) (hUnonempty : Uhat.Nonempty) (hRad : 0 < Rad) (hs : 0 < s) (hsHalf : s < 1 / 2) (hsRange : s ∈ Set.Ico ((1 + g) / 4) (1 / 2)) (hrateOrder : kappaRate ≤ s) (hGauge : Uhat ⊆ {z : Vec d | vecNormSq z ≤ specBound (symmPart abar)⁻¹}) (u h : H1Function Uphys) (uHat hHat : H1Function Uhat) (huHat : uHat.grad = fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (u.grad (matVecMul (matSqrt (symmPart abar)) y))) (hhHat : hHat.grad = fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (h.grad (matVecMul (matSqrt (symmPart abar)) y))) {aHat : CoeffField d} (haHat : aHat = affineCoefficient (matSqrt (symmPart abar)) ⋯ fun (z : Vec d) => scaledCoeff epsilon a z - skewPart abar) (aObs aCell : system.CellIndex → Book.Ch03.CoeffFamily d) (hObs : ∀ (i : system.CellIndex), ((aObs i).coeffOn (ruledObservationCube system i)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (ruledObservationCube system i))] fun (y : Vec d) => affineCoefficient (matSqrt (symmPart abar)) ⋯ (fun (z : Vec d) => scaledCoeff epsilon a z - skewPart abar) (y + ruledObservationCenter system i)) (wCell : (i : system.CellIndex) → Book.Ch03.ForcedCubeSolution (whitneyCellCube system i) (aCell i) 0) (hfamily : RuledCellPhysicalForcedFamily system aHat uHat aCell wCell) {Kenergy : ℝ} {boundaryEnergy hardyConstant : ENNReal} (hEnergy : GaugePhysicalEnergyPriceAtWitness Uhat aHat uHat Kenergy boundaryEnergy) (hBoundaryTop : boundaryEnergy ≠ ⊤) (hHardy : ∀ (G : Vec d → Vec d), MeasureTheory.Integrable G (MeasureTheory.volume.restrict Uhat) → PrintFaithfulPositiveTestRow system s G hardyConstant) (hFdefect : MemVectorL2 Uhat fun (y : Vec d) => matVecMul (aHat y - 1) (uHat.grad y)) {cnorm : ℝ} (hcnorm : 0 < cnorm) (hInner : ellipsoid abar cnorm ⊆ Uphys) (hSandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ Uphys) rho Rad) {Cdual : ℝ} (hDual : PrintFaithfulDomainFluxDefectDuality Uhat s aHat uHat hHat Cdual) {C₀ : ℝ → ℝ → ℝ → ℝ} (hC₀ : 0 ≤ C₀ s rho Rad) (hhead : ∀ (J : ℕ), 2 * Rad ≤ 3 ^ ↑J → 3 ^ ↑J ≤ 1 + 3 * (2 * Rad) → scheduledRateHead d (√(hsAffineFactor (matSqrt (symmPart abar))⁻¹ s ‖matSqrt (symmPart abar)‖)) Cdual ((Real.rpow 3 (responseWindowOrder g) * foldedAnchoredFrameConstant d g kappaRate s (coarseFluxResponseConstant d) Rad cnorm hgood.delta ↑J) ^ 2 * Kenergy) hardyConstant ≤ ENNReal.ofReal (C₀ s rho Rad)) (uGrad : Vec d → Vec d) (huGrad : u.grad = uGrad) : ((negSobolevNorm Uphys s fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (uGrad y - h.grad y)) + negSobolevNorm Uphys s fun (y : Vec d) => matVecMul (matSqrt (symmPart abar))⁻¹ (matVecMul (scaledCoeff epsilon a y - skewPart abar) (uGrad y) - matVecMul (symmPart abar) (h.grad y))) ≤ ENNReal.ofReal (C₀ s rho Rad * (epsilon * (x * eccentricityFoldFactor abar (foldedFrameEccentricityExponent g kappaRate))) ^ kappaRate) * boundaryEnergy ^ (1 / 2)

(δ), part three. The frozen Dirichlet conclusion at the folded length, with the constant an explicit parameter.