High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.EpsilonFrameWitnessPrice

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

The frozen-witness energy price at the hole's own microscopic parameter split module twenty-four

hypotheses into a "the certificate destructurings" of five certificate destructurings and a "the analytic inputs" of four analytic identifications. This module closes the certificate destructurings entirely, and closes the one load-bearing analytic input (the λ-versus-ε mismatch), by composing

• RowRetainingPrintOrderGoodScale.exists_formulaicScaledResponseWindowTail — which delivers, in one call from the row-retaining certificate and the hole's own hx/hepsilon/hscale, the whole λ-route package: N, G, lambda = epsilon * 3 ^ N with lambda ∈ Icc 1 3, aScaled = Quenched.physical_scale_coeff N a, the amplitude deltaScaled, the enclosure bracket 3 ^ G ≤ 1 + 3 (ecc √d), the formulaic shift L = formulaicNormalizedReferenceTailShift d b ρ (2κ) G, the normalized reference aRef and its ScalarIdentityPowerTail at the response-window order;
• the sqrt_deltaScaled_le_one premise — the amplitude window √deltaScaled ≤ 1;
• the one_sub_rpow_neg_gap_pos_responseWindow premise and the two printed-order margins — the three scalar premises;
• the witnessObservation_lambdaScaled_of_epsilon premise — the ε/λ frame identity.

The certificate-destructuring table points at PrintOrderQuantitativeNormalizedReferenceCertificate itself. That is the wrong producer: the raw certificate carries the tail at printCertificateOrder g for the unscaled a, whereas that module consumes it at responseWindowOrder g for the scaled aScaled, with the formulaic shift. that module is the producer that does both conversions, and it is available.

Only the analytic inputs remain, and this theorem exhibits them exactly: v, hBesov, hL2, hb, hu, hF, hFrame are the only hypotheses below that are not the hole's own binders or a producer's output.

theorem HCPolySupport.HighContrast.RowSupply.exists_frozenWitnessEnergyPrice_at_epsilon (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 : ℕ) (aFam : Book.Ch03.CoeffFamily d) (v : Book.Ch03.DirichletForcedCubeSolution (originCube d j) aFam 0) (aHat : CoeffField d) (uHat : H1Function (matImage (matSqrt (symmPart abar))⁻¹ U)) (g0grad FTrans : Vec d → Vec d), 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 → ((aFam.coeffOn (originCube d j)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (originCube d j))] fun (y : Vec d) => affineCoefficient (matSqrt (symmPart abar)) ⋯ (fun (w : Vec d) => scaledCoeff epsilon a w - skewPart abar) (y + matVecMul (matSqrt (symmPart abar))⁻¹ z)) → Book.Ch03.ForceBesovRegularity (originCube d j) s₀ (Book.Ch03.dirichletBoundaryGradientField v) → MemVectorL2 (openCubeSet (originCube d j)) (Book.Ch03.dirichletBoundaryGradientField v) → (∀ (y : Vec d), aHat (y + matVecMul (matSqrt (symmPart abar))⁻¹ z) = (aFam.coeffOn (originCube d j)).toCoeffField y) → (∀ (y : Vec d), uHat.grad (y + matVecMul (matSqrt (symmPart abar))⁻¹ z) = v.toH1.grad y) → (∀ (y : Vec d), FTrans (y + matVecMul (matSqrt (symmPart abar))⁻¹ z) = Book.Ch03.dirichletBoundaryGradientField v y) → (∀ (w : Vec d), FTrans (matVecMul (matSqrt (symmPart abar))⁻¹ w) = matVecMul (matSqrt (symmPart abar)) (g0grad w)) → ∃ lambda ∈ Set.Icc 1 3, GaugePhysicalEnergyPriceAtWitness (matImage (matSqrt (symmPart abar))⁻¹ U) aHat 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)) (g0grad w))

The frozen-witness energy price, stated at the hole's scaledCoeff ε a. Every Group-A hypothesis from the modules named above is discharged inside; the seven Group-B items (v, hBesov, hL2, hb, hu, hF, hFrame) remain as binders, and the λ-route's microscopic parameter survives only inside lambdaRouteClaw, bounded by the exported lambda ∈ Icc 1 3.