High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.WitnessPriceAtPrintOrder

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

The λ-route price at the printed order s₀

The orders have to be reconciled: the response-window tail produces the reference tail at responseWindowOrder g = (3+5g)/16, so the λ-route composition delivers the observation error at that order, while the frozen clause's boundary energy is at s₀ ∈ Ico ((1+g)/4) (1/2) — and (3+5g)/16 < (1+g)/4 for every g < 1.

The gap closes with one upstream lemma, and nothing is restated. The multiscale error is decreasing in the fractional order (Book.Ch03.ABK26.homogenizationErrorOnCube_infinity_two_le_of_lt, loss exactly one), and the comparison runs in the favourable direction: the composition is performed at the smaller order responseWindowOrder g and its conclusion is read at the larger order s₀. The fold arithmetic — frameFoldConstant, witnessErrorEccentricityExponent — is therefore used unchanged at responseWindowOrder g and needs no restatement.

Cwit is unchanged: it is still lambdaRouteClaw d (responseWindowOrder g) λ abar · ((ρ/(3√d))^(−responseWindowOrder g) · frameFoldConstant) · ecc^q, so the whole s₀-dependence of the price sits in the energy's own gaugeWitnessEnergyPriceW C d s₀ Cwit abar, exactly where the interface modules needs it.

The two scalar facts about the two orders

theorem HCPolySupport.HighContrast.RowSupply.responseWindowOrder_pos {g : ℝ} (hg : g ∈ Set.Ico 0 1) : 0 < responseWindowOrder g

The response-window order is positive on the printed g-window.

theorem HCPolySupport.HighContrast.RowSupply.responseWindowOrder_lt_printOrder {g s₀ : ℝ} (hg : g ∈ Set.Ico 0 1) (hs₀ : s₀ ∈ Set.Ico ((1 + g) / 4) (1 / 2)) : responseWindowOrder g < s₀

The response-window order is strictly below the whole printed s₀ window. (3+5g)/16 < (4+4g)/16 = (1+g)/4 ≤ s₀ for every g < 1.

The order lift of the λ-route conclusion

theorem HCPolySupport.HighContrast.RowSupply.exists_witnessLambdaRouteError_at_printOrder {d : ℕ} [NeZero d] {g kappa deltaScaled lambda s₀ : ℝ} (hg : g ∈ Set.Ico 0 1) (hs₀ : s₀ ∈ Set.Ico ((1 + g) / 4) (1 / 2)) (hlambda : lambda ∈ Set.Icc 1 3) (a : CoeffSpace d) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (t : ℤ) {j : ℤ} {z : Vec d} {U : Set (Vec d)} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) (hUsub : U ⊆ ellipsoid abar 1) (aRef : Book.Ch03.CoeffFamily d) (haRef : ∀ (R : TriadicCube d), (aRef.coeffOn R).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ((normalizedCenteredCoeff a abar hS).coeffOn (Response.adaptedDomain ⋯ t)).toCoeffField) (L : ℕ) (n : ℤ) (hLn : ↑L ≤ n) (hTail : ScalarIdentityPowerTail aRef (responseWindowOrder g) (√deltaScaled) kappa (3 ^ ↑L)) (aObs : Book.Ch03.CoeffFamily d) (hObs : (aObs.coeffOn (originCube d j)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (originCube d j))] fun (x : Vec d) => affineCoefficient (matSqrt (symmPart abar)) ⋯ (fun (y : Vec d) => scaledCoeff lambda a y - skewPart abar) (x + matVecMul (matSqrt (symmPart abar))⁻¹ z)) : ∃ (M : ℤ), M = max (max n j) 1 ∧ n ≤ M ∧ j ≤ M ∧ 1 ≤ M ∧ Book.Ch02.HomogenizationErrorOnCube (originCube d j) s₀ Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) aObs 1 ≤ lambdaRouteClaw d (responseWindowOrder g) lambda abar * (3 ^ ((responseWindowOrder g - kappa) * ↑M - responseWindowOrder g * ↑j + kappa * ↑L) * √deltaScaled)

21e. The λ-route's observation-error bound, produced at the response-window order, holds unchanged at every printed order s₀.

The frozen-witness price at the printed order

theorem HCPolySupport.HighContrast.RowSupply.exists_frozenWitnessEnergyPrice_at_printOrder (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 < C ∧ ∀ (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (U : Set (Vec d)) (j : ℤ) (z : Vec d) (g kappaRate deltaScaled lambda rho Rad s₀ : ℝ) (G L J : ℕ) (a : CoeffSpace d) (t : ℤ) (aRef 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), g ∈ Set.Ico 0 1 → s₀ ∈ Set.Ico ((1 + g) / 4) (1 / 2) → 0 < kappaRate → 0 ≤ Certificate.printRowOrder g → 0 < 1 - 3 ^ (-(2 * responseWindowOrder g - Certificate.printRowOrder g)) → 0 < Certificate.shiftedTailAbsorptionPrefactor d (responseWindowOrder g) (Certificate.printRowOrder g) G → L = Certificate.formulaicNormalizedReferenceTailShift d (responseWindowOrder g) (Certificate.printRowOrder g) (2 * kappaRate) G → 3 ^ ↑G ≤ 1 + 3 * (witnessEccentricity (symmPart abar) * √↑d) → 2 * Rad ≤ 3 ^ ↑J → √deltaScaled ≤ 1 → lambda ∈ Set.Icc 1 3 → U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j) → U ⊆ ellipsoid abar 1 → ellipsoid abar (1 / (3 * √↑d)) ⊆ U → HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) rho Rad → (∀ (R : TriadicCube d), (aRef.coeffOn R).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ((normalizedCenteredCoeff a abar hS).coeffOn (Response.adaptedDomain ⋯ t)).toCoeffField) → ScalarIdentityPowerTail aRef (responseWindowOrder g) (√deltaScaled) kappaRate (3 ^ ↑L) → ((aFam.coeffOn (originCube d j)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (originCube d j))] fun (x : Vec d) => affineCoefficient (matSqrt (symmPart abar)) ⋯ (fun (y : Vec d) => scaledCoeff lambda a y - skewPart abar) (x + 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) → (∀ (x : Vec d), FTrans (matVecMul (matSqrt (symmPart abar))⁻¹ x) = matVecMul (matSqrt (symmPart abar)) (g0grad x)) → 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 (x : Vec d) => matVecMul (matSqrt (symmPart abar)) (g0grad x))

The frozen-witness energy price at the printed order s₀. Identical to HCPoly.Provider.PolynomialHomogenization.Root.Dirichlet.FrozenWitnessPriceAtWitnessRoute except that the energy order is the frozen clause's s₀, not the response-window order; Cwit is unchanged.