High-contrast homogenization: Provider.Quenched.SmallContrastAdaptedTilt

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

The adapted-to-Euclidean tilt comparison

This file formalizes the first display of Lemma 2.15 of HC, equation (2.127),

𝐀hom(y + cus_n) ≤ 𝐀hom(cu_k) + C Π^{1/2}(1-γ)^{-1}(1 + K²3^{-k})^γ 3^{-(n-k)}𝐄,

in the construction's carriers, and combines it with the Euclidean envelope of SmallContrastHomogenizedComparison to produce the adapted-cube form of HC (4.18).

The construction is the base-scale refinement of the Whitney bridge Window.adapted_scaled_of_standard. That bridge fills the adapted cell of scale r with Euclidean cells starting at scale r itself, and pays boundaryConst = C_d 𝔢_q ζ_g on every row, including the top one — which is exactly the Π-dependence that has to be isolated. Here the maximal filling is started at a lower base scale k ≤ r. Then

• the top row consists of Euclidean cells of scale k; its weights sum to at most one, and — this is the step the printed proof performs and the construction never did — its annealed value is 𝐀hom(cu_k) by stationarity (Quenched.annealedBlock_standardCell_eq_centeredCube), not a Dagger envelope. No geometric constant is paid on it at all;
• every lower row k - u, u ≥ 1, is a boundary row: its relative volume is at most C_d 𝔢_q 3^{(k-u)-r}, so the whole tail is charged boundaryConst · 3^{-(1-g)(r-k)} · 3^{gG}, which is a decaying function of the gap r - k.

Consequently all of the adapted geometry — 𝔢_q and the grid enlargement G, i.e. all of Π — appears only inside a quantity that the gap r - k can be chosen to make smaller than any prescribed dimensional tolerance, and the gap enters only through log₃. This is the printed design principle and the (1-γ)^{-1} + 2 log Π part of the printed threshold n₁: the (1-g) in the exponent is the source of the printed (1-γ)^{-1} factor.

The burn scale

theorem HCPolySupport.HighContrast.Quenched.exists_burnScale {d : ℕ} {g : ℝ} (hg : g ∈ Set.Ico 0 1) {S : CoeffSpace d → ℝ} {sK t : ℤ} (hDelta : 0 ≤ t - 1 - sK) (a : CoeffSpace d) : ∃ (m : ℤ), t ≤ m ∧ S a ≤ 3 ^ m ∧ 3 ^ (g * (↑m - ↑t)) ≤ 1 + {b : CoeffSpace d | 3 ^ t < S b}.indicator (normalizedSourceScale S sK) a

The burn scale of a sample. At every sample there is a scale m ≥ t at which the source has burned and whose Dagger discount relative to t is at most 1 + 1_bad·nss: the good event uses m = t and pays nothing, and the bad event uses the source's own scale and pays the normalized source scale. This is the Markov step the construction's entry envelope performs inline, isolated.

The boundary-row series

The tilt defect

noncomputable def HCPolySupport.HighContrast.Quenched.tiltDefect {d : ℕ} (Cd g : ℝ) (m : Mat d) (G : ℕ) (k r : ℤ) : ℝ

The boundary defect of the tilt comparison: the construction's rendering of the printed error CΠ^{1/2}(1-γ)^{-1}(1 + K²3^{-k})^γ3^{-(n-k)} of HC (2.127). All the adapted geometry sits in the prefactor boundaryConst · 3^{gG}, and the gap r - k discounts it geometrically at rate 1 - g.

Equations

• HCPolySupport.HighContrast.Quenched.tiltDefect Cd g m G k r = 2 * HCPolySupport.HighContrast.boundaryConst Cd g m * 3 ^ (-(1 - g) * (↑r - ↑k) + g * ↑G)

theorem HCPolySupport.HighContrast.Quenched.tiltDefect_nonneg {d : ℕ} [Nonempty (Fin d)] {Cd g : ℝ} (hCd : 1 ≤ Cd) (hg : g ∈ Set.Ico 0 1) {m : Mat d} (hm : Matrix.PosDef m) (G : ℕ) (k r : ℤ) : 0 ≤ tiltDefect Cd g m G k r

The bad-event first moment

theorem HCPolySupport.HighContrast.Quenched.integral_indicator_normalizedSourceScale_le {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) (t : ℤ) : ∫ (a : CoeffSpace d), {b : CoeffSpace d | 3 ^ t < S b}.indicator (normalizedSourceScale S sK) a ∂P ≤ euclideanEntryDefect K sK t

The first moment of the bad-event indicator of the normalized source scale, by Markov at the second moment: this is the Markov step of the entry envelope, isolated for reuse.

The tilt comparison

theorem HCPolySupport.HighContrast.Quenched.adaptedMean_quadratic_le_add_tiltDefect {d : ℕ} [NeZero d] (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (hstat : IsStationaryLaw P) {l : ℤ} (hl : ↑(kZero d) ≤ l) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {nu : Mat d} (hnu : Matrix.PosDef nu) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) {k r : ℤ} {G : ℕ} (hk0 : 0 ≤ k) (hDelta : 0 ≤ r + ↑G - 1 - sK) (hentry : sourceMomentTwo K ≤ 3 ^ (r + ↑G - sK)) (hsub : adaptedCell (roundedGrid l nu) r ⊆ centeredCube d (r + ↑G)) (hint : HasFiniteAdaptedMean P (roundedGrid l nu) r) (X : BlockVec d) : blockVecDot X (blockMatVecMul (adaptedMean P (roundedGrid l nu) r) X) ≤ blockVecDot X (blockMatVecMul (annealedBlock P (centeredCube d k)) X) + tiltDefect Cd g nu G k r * blockVecDot X (blockMatVecMul E X)

The adapted-to-Euclidean tilt comparison (Lemma 2.15 of HC, equation (2.127)). For 0 ≤ k ≤ r the annealed adapted cell of scale r is dominated by the annealed Euclidean cube of scale k plus a boundary defect which carries all of the adapted geometry but decays geometrically in the gap r - k.

The top row of the maximal filling is charged by stationarity — its annealed value is exactly 𝐀hom(cu_k) — and only the rows strictly below the base scale are charged by the Dagger, at total relative volume C_d𝔢_q3^{-(r-k)}.

The threshold and the adapted near-identity comparison

noncomputable def HCPolySupport.HighContrast.Quenched.tiltGap {d : ℕ} (Cd g cEnt : ℝ) (m : Mat d) (G : ℕ) : ℤ

The adapted part of the printed entry threshold n₁: the scale gap r - k that discounts the boundary defect below the tolerance. It is (1-g)^{-1}·log₃(2·boundaryConst·3^{gG}/cEnt), i.e. exactly the printed (1-γ)^{-1} + 2 log Π + A(d) terms — the aspect ratio enters here, inside a logarithm, and nowhere else.

Equations

• HCPolySupport.HighContrast.Quenched.tiltGap Cd g cEnt m G = max 1 ⌈Real.logb 3 (2 * HCPolySupport.HighContrast.boundaryConst Cd g m * 3 ^ (g * ↑G) / cEnt) / (1 - g)⌉

theorem HCPolySupport.HighContrast.Quenched.tiltDefect_le {d : ℕ} [Nonempty (Fin d)] {Cd g cEnt : ℝ} (hCd : 1 ≤ Cd) (hg : g ∈ Set.Ico 0 1) {nu : Mat d} (hnu : Matrix.PosDef nu) (hcEnt : 0 < cEnt) {G : ℕ} {k r : ℤ} (hgap : tiltGap Cd g cEnt nu G ≤ r - k) : tiltDefect Cd g nu G k r ≤ cEnt

Past the gap the tilt defect is at most the prescribed tolerance.

theorem HCPolySupport.HighContrast.Quenched.adaptedMean_near_reference {d : ℕ} [NeZero d] (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (hstat : IsStationaryLaw P) {l : ℤ} (hl : ↑(kZero d) ≤ l) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {nu : Mat d} (hnu : Matrix.PosDef nu) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) {k r : ℤ} {G : ℕ} (hk0 : 0 ≤ k) {sigma cEnt : ℝ} (hsigma : refContrast E - 1 ≤ sigma) (hsigma0 : 0 ≤ sigma) (hcEnt : 0 < cEnt) (hkthr : euclideanEntryThreshold K (cEnt / 2) sK ≤ k) (hgap : tiltGap Cd g (cEnt / 2) nu G ≤ r - k) (hDelta : 0 ≤ r + ↑G - 1 - sK) (hentry : sourceMomentTwo K ≤ 3 ^ (r + ↑G - sK)) (hsub : adaptedCell (roundedGrid l nu) r ⊆ centeredCube d (r + ↑G)) (hint : HasFiniteAdaptedMean P (roundedGrid l nu) r) : BlockMatLoewnerLE (blockScale (1 - nearIdentityDefect cEnt sigma) E) (adaptedMean P (roundedGrid l nu) r) ∧ BlockMatLoewnerLE (adaptedMean P (roundedGrid l nu) r) (blockScale (1 + nearIdentityDefect cEnt sigma) E)

The construction form of HC (4.18) on adapted cubes. Once the base scale k is past the source-moment threshold and the gap r - k is past the geometric threshold, the annealed adapted block of scale r is a near identity in the reference normalization, at a defect that depends only on the prescribed tolerance and on the reference contrast excess.

Both thresholds are logarithmic in the data — log₃ M₂(K) and (1-g)^{-1}log₃(boundaryConst·3^{gG}) — and the conclusion's constant carries neither the eccentricity of the adapted geometry nor the grid enlargement G, hence neither carries the reference aspect ratio Π. This is the routing the printed proof performs and the construction's Π-carrying entry envelope does not.