High-contrast homogenization: Provider.Quenched.SmallContrastHomogenizedComparison

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

The reference-normalized near-identity comparison

This file formalizes the printed comparison HC (4.18),

for every m ≥ 2n₁, |𝐄^{-1/2}𝐀hom(cus_m)𝐄^{-1/2} - I_{2d}| ≤ c(d),

in the construction's Loewner dialect, where the printed absolute-value statement reads blockScale (1 - c) 𝐄 ≤ 𝐀hom ≤ blockScale (1 + c) 𝐄.

The printed derivation has two halves and this file supplies both, in the generality in which they are actually printed.

• The algebraic half is Lemma 2.7 of HC (equation (2.89), the printed argument): a one-sided bound gives a two-sided bound for free when the reference contrast is small. The printed proof reads the chain 𝐄_* ≤ 𝐀_*(U) ≤ 𝐀(U) ≤ 𝐄₁ and then quotes the upper half of HC (2.82). That upper half is machine-refuted as printed (the corrected statement, the upper comparison obstruction), so the valid route uses the reference ratio bound κ_𝐄 ≤ 1 + 6(Θ - 1) of Initialization.kappaRef_le_one_add_six_mul_refContrast_sub_one, which is the established replacement for the false display. Given A ≤ (1 + ε)𝐄, the sharp involution reverses the order and is homogeneous of degree minus one, the annealed block dominates its own sharp, and 𝐄 ≤ κ_𝐄𝐄^♯; the four facts compose to ((1 + ε)κ_𝐄)^{-1}𝐄 ≤ A. No Π enters.

• The analytic half is the Euclidean-cube envelope HC (2.98), the printed argument, whose upper part is 𝐀hom(cu_n) ≤ (1 + 3^{3-n}K_{Ψ_S}²)𝐄. Here it is proved directly from e.coarse.ellipticity at coincident scales — where the Dagger's discount is exactly 1, with no boundary transfer and therefore no boundaryConst — plus the Markov step on the source scale that the construction already uses elsewhere. The resulting defect is M₂(K)·3^{-(n - s_K)}, so the scale threshold it forces is n ≳ s_K + log₃ M₂(K) ≈ 4 log₃ K_bar_S: exactly the 4 log K_{Ψ_S} term of the printed n₁ (the printed argument).

Both halves are free of the reference aspect ratio Π: the whole point of the printed route is that Π enters only through the scale threshold, which is the design principle stated at the printed argument and the slot the frozen hcore binder reserves for it.

The algebraic half: two-sided bounds from one-sided bounds

theorem HCPolySupport.HighContrast.Quenched.blockScale_inv_le_of_le_blockScale {d : ℕ} [NeZero d] {E A : BlockMat d} (hEsymm : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hEsharp : BlockMatLoewnerLE (blockSharp E) E) (hAsymm : IsSymmetricBlockMat A) (hApd : Book.Ch02.BlockPosDef A) (hAself : BlockMatLoewnerLE (blockSharp A) A) {c : ℝ} (hc : 0 < c) (hupper : BlockMatLoewnerLE A (blockScale c E)) : BlockMatLoewnerLE (blockScale (c * kappaRef E)⁻¹ E) A

Lemma 2.7 of HC, lower half (equation (2.89)). A positive block that dominates its own sharp and is dominated by c𝐄 is bounded below by (cκ_𝐄)^{-1}𝐄. The printed proof reads the chain 𝐄_* ≤ 𝐀_*(U) ≤ 𝐀(U) ≤ 𝐄₁ and quotes HC (2.82); the route here composes the order reversal of the sharp involution, its degree -1 homogeneity, the self-domination A^♯ ≤ A, and the intrinsic bound 𝐄 ≤ κ_𝐄𝐄^♯.

def HCPolySupport.HighContrast.Quenched.nearIdentityDefect (eps sigma : ℝ) : ℝ

The near-identity defect assembled from the entry defect ε of the one-sided envelope and the reference contrast excess σ: the printed c(d) of HC (4.18), which the print obtains by choosing A(d) large and σ_0(d) small.

Equations

• HCPolySupport.HighContrast.Quenched.nearIdentityDefect eps sigma = (1 + eps) * (1 + 6 * sigma) - 1

theorem HCPolySupport.HighContrast.Quenched.nearIdentityDefect_nonneg {eps sigma : ℝ} (heps : 0 ≤ eps) (hsigma : 0 ≤ sigma) : 0 ≤ nearIdentityDefect eps sigma

theorem HCPolySupport.HighContrast.Quenched.near_identity_of_le_blockScale {d : ℕ} [NeZero d] {E A : BlockMat d} (hEsymm : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hEsharp : BlockMatLoewnerLE (blockSharp E) E) (hAsymm : IsSymmetricBlockMat A) (hApd : Book.Ch02.BlockPosDef A) (hAself : BlockMatLoewnerLE (blockSharp A) A) {eps cIso : ℝ} (heps : 0 ≤ eps) (hcIso : 0 ≤ cIso) (hupper : BlockMatLoewnerLE A (blockScale (1 + eps) E)) (hprod : (1 + eps) * kappaRef E ≤ 1 + cIso) : BlockMatLoewnerLE (blockScale (1 - cIso) E) A ∧ BlockMatLoewnerLE A (blockScale (1 + cIso) E)

Lemma 2.7 of HC (equation (2.89)): the two-sided near-identity comparison from a one-sided envelope. This is the algebraic engine of HC (4.18).

The analytic half: the Euclidean annealed envelope

noncomputable def HCPolySupport.HighContrast.Quenched.euclideanEntryDefect (K : ℝ) (sK n : ℤ) : ℝ

The entry defect of the Euclidean annealed envelope: the construction's rendering of the printed 3^{3-n}K_{Ψ_S}² of HC (2.98).

Equations

• HCPolySupport.HighContrast.Quenched.euclideanEntryDefect K sK n = HCPolySupport.HighContrast.Quenched.sourceMomentTwo K * 3 ^ (sK - n)

theorem HCPolySupport.HighContrast.Quenched.annealedBlock_centeredCube_le_one_add_entryDefect {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) {n : ℤ} (hDelta : 0 ≤ n - 1 - sK) : BlockMatLoewnerLE (annealedBlock P (centeredCube d n)) (blockScale (1 + euclideanEntryDefect K sK n) E)

The Euclidean annealed envelope (HC (2.98), upper half): 𝐀hom(cu_n) ≤ (1 + M₂(K)3^{-(n-s_K)})𝐄, with prefactor exactly one and a defect that decays geometrically in the scale. No aspect-ratio constant appears: the Dagger is read at coincident scales, so no adapted-cell boundary transfer is performed.

The scale threshold and the assembled comparison

noncomputable def HCPolySupport.HighContrast.Quenched.euclideanEntryThreshold (K cEnt : ℝ) (sK : ℤ) : ℤ

The Euclidean part of the printed entry threshold n₁ (the printed argument): the scale past which the annealed Euclidean envelope has defect at most cEnt. It is s_K + log₃(M₂(K)/cEnt), i.e. the printed 4 log K_{Ψ_S} + A(d) terms; the remaining 2 log Π + (1-γ)^{-1} terms of n₁ belong to the adapted-cube transfer and enter only as a threshold there as well.

Equations

• HCPolySupport.HighContrast.Quenched.euclideanEntryThreshold K cEnt sK = sK + max 1 ⌈Real.logb 3 (HCPolySupport.HighContrast.Quenched.sourceMomentTwo K / cEnt)⌉

theorem HCPolySupport.HighContrast.Quenched.one_le_sourceMomentTwo (K : ℝ) : 1 ≤ sourceMomentTwo K

theorem HCPolySupport.HighContrast.Quenched.euclideanEntryDefect_le {K cEnt : ℝ} (hcEnt : 0 < cEnt) {sK n : ℤ} (hn : euclideanEntryThreshold K cEnt sK ≤ n) : euclideanEntryDefect K sK n ≤ cEnt

Past the threshold the entry defect is at most cEnt.