High-contrast homogenization: Provider.Quenched.SmallContrastBurnInPolynomial

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

The burn-in is polynomial in the telescope's base

The hentry clause of the isotropic-variance core body reads

(3 : ℝ) ^ (2 * N₀) ≤ base ^ Centry

with base = 2 + aspectRatio Ebase * Kbase and Centry chosen before the law.'s entry_exponent_of_burnIn reduces it to a law-free exponent for 3 ^ N₀ itself, and the burn-in N₀ the endpoint uses is the bootstrap's N1 = sK + 1 + gap (HCPoly.Provider.Quenched.SmallContrastBurnInUniform).

This file closes's table. Its two one-line entries are

• witnessEccentricity_one — the identity witness has eccentricity one, so boundaryConst Cd g 1 is (d, g)-only and bootstrapAdapterFactor Cd g K E 1 loses its grid factor entirely;
• rpow_le_self_of_one_le — (1 + K ^ 2) ^ g ≤ 1 + K ^ 2 for g ≤ 1, which is what removes the source gauge's fractional power.

With them, every factor of 3 ^ N1 = 3 ^ sK * 3 * 3 ^ gap is under a power of the base: 3 ^ sK by exists_source_scale_minimal and growthBar_le_base, 3 ^ gap by exists_gap_three_pow_le_minimal and the polynomial bound on bootstrapAdapterFactor assembled here. The law-free constants that remain — CB, Cd, zetaG g, 1 + 6 * sigma, sigma⁻¹, 3 ^ kZero d — ride into the exponent through exists_rpow_ge_uniform, which is admissible precisely because they are fixed before Ebase and Kbase.

sigma is the endpoint's cSc step 6) and CB, Cd depend on d and g alone, so cburn — and therefore Cdelay — is chosen at the binder's own quantifier order.

1. The two one-line entries of

theorem HCPolySupport.HighContrast.Quenched.witnessEccentricity_one {d : ℕ} [Nonempty (Fin d)] : witnessEccentricity 1 = 1

The identity witness has eccentricity one. witnessEccentricity is the square root of |m| |m⁻¹|, and both factors are one at the identity.

theorem HCPolySupport.HighContrast.Quenched.rpow_le_self_of_one_le {y c : ℝ} (hy : 1 ≤ y) (hc : c ≤ 1) : y ^ c ≤ y

A subunit power of a quantity at least one is below the quantity. At y := 1 + K ^ 2 and c := g this is (1 + K ^ 2) ^ g ≤ 1 + K ^ 2.

2. The bootstrap adapter factor at the identity witness

theorem HCPolySupport.HighContrast.Quenched.boundaryConst_one {d : ℕ} [Nonempty (Fin d)] (Cd g : ℝ) : boundaryConst Cd g 1 = Cd * zetaG g

The boundary constant at the identity witness is (d, g)-only.

theorem HCPolySupport.HighContrast.Quenched.bootstrapAdapterFactor_one_le {d : ℕ} [Nonempty (Fin d)] {Cd g K sigma : ℝ} {E : BlockMat d} (hg1 : g ≤ 1) (hCd : 0 ≤ Cd) (hzeta : 0 ≤ zetaG g) (hsigma : 0 ≤ sigma) (hkap0 : 0 ≤ kappaRef E) (hkap : kappaRef E ≤ 1 + 6 * sigma) : bootstrapAdapterFactor Cd g K E 1 ≤ (1 + K ^ 2) * ((1 + 6 * sigma) * (3 * growthBar K * (Cd * zetaG g)))

The bootstrap adapter factor, polynomial in the growth bar. At the identity witness the grid eccentricity is one, the source gauge's fractional power collapses, and what remains is the reference ratio times the first source moment times the (d, g)-only boundary constant.

3. The three factors combine

theorem HCPolySupport.HighContrast.Quenched.three_zpow_burnIn_le_rpow {base c1 c2 : ℝ} {sK gap : ℤ} (hbase : 3 ≤ base) (hsK : 3 ^ sK ≤ base.rpow c1) (hgap : 3 ^ gap ≤ base.rpow c2) : 3 ^ (sK + 1 + gap) ≤ base.rpow (c1 + c2 + 1)

3 ^ (sK + 1 + gap) from its two factors. The + 1 of the burn-in costs one power of the base, because the base is at least three.

4. The law-free burn-in exponent