High-contrast homogenization: Provider.Quenched.SmallContrastDelayExponentUniform

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

The delay exponents, chosen before the law

the corresponding argument check. The frozen hcore binder (the cited theorem) reads

∃ cSc, 0 < cSc ∧ ∀ g ∈ Ico 0 1, ∃ alpha Cdelay, … ∀ cStar gBase Pbase Ebase Ψbase Kbase Sbase, …

so Cdelay — not only alpha — is chosen before the law. The endpoint takes Cdelay := fusedDelay Centry Cpref A g (the corresponding argument), and its two producers are

entry_exponent_le_rpow : 3 ^ (2 * N₀) ≤ base ^ ((2 * N₀ : ℕ) : ℝ)     -- Centry := 2 N₀
exists_rpow_ge         : ∃ C, 0 ≤ C ∧ x ≤ base ^ C                    -- Cpref  := logb base x

Neither is admissible at that quantifier order, and this file says exactly why and supplies the replacements:

• the real-power entry exponent returns 2 N₀, and N₀ is the burn-in — a law-dependent natural number. The printed route is that Π rides in the base 2 + aspectRatio Ebase * Kbase with a law-free exponent, i.e. one needs 3 ^ N₀ ≤ base ^ cburn at a law-free cburn first; entry_exponent_of_burnIn then squares it.
• the base-dependent real-power bound returns logb base x, which depends on the base, hence on the law. exists_rpow_ge_uniform gives one exponent good for every base ≥ 3 at once, by measuring the logarithm at the fixed base 3 and using 3 ≤ base monotonically.

The capstone states the settlement in the binder's own quantifier order: ∃ Centry Cpref, ∀ base, ∀ N₀, …. With it, Cdelay is law-free as soon as A is — so the Cdelay side needs no carrier wave, only the burn-in's own polynomial bound (the corresponding argument, and three_mul_max_one_le_rpow below is the step every such bound ends with).

1. The base-uniform exponent

theorem HCPolySupport.HighContrast.Quenched.exists_rpow_ge_uniform (x : ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (base : ℝ), 3 ≤ base → x ≤ base.rpow C

One exponent for every base at once. The replacement for the base-dependent bound, whose exponent logb base x depends on the base and so may not be chosen before the law.

2. The entry exponent from a law-free burn-in exponent

theorem HCPolySupport.HighContrast.Quenched.entry_exponent_of_burnIn {base cburn : ℝ} {N₀ : ℕ} (hbase : 3 ≤ base) (hburn : 3 ^ N₀ ≤ base.rpow cburn) : 3 ^ (2 * N₀) ≤ base.rpow (2 * cburn)

hentry at a law-free exponent. The real-power entry exponent returns 2 * N₀, which is law-dependent; once the burn-in itself is polynomial in the base at a law-free exponent cburn, the entry clause holds at 2 * cburn.

theorem HCPolySupport.HighContrast.Quenched.entry_exponent_of_integer_split_cap {base C cC c Centry : ℝ} {split : ℤ} {N₀ : ℕ} (hbase : 3 ≤ base) (hN₀ : ↑N₀ = split) (hsplit : 3 ^ split ≤ C * base.rpow c) (hC : C ≤ base.rpow cC) (hCentry : Centry = 2 * cC + 2 * c) : 3 ^ (2 * N₀) ≤ base.rpow Centry

An integer-index split cap supplies the cadence endpoint's natural, squared entry cap after its coefficient is absorbed into the base.

3. The step every polynomial burn-in bound ends with

theorem HCPolySupport.HighContrast.Quenched.three_mul_max_one_le_rpow {base c x : ℝ} (hbase : 3 ≤ base) (hc : 0 ≤ c) (hx : x ≤ base.rpow c) : 3 * max 1 x ≤ base.rpow (c + 1)

3 · max 1 x stays polynomial. three_pow_ceil_logb_le bounds a ceiling-of-logarithm delay by 3 * max 1 x; if x is itself below a law-free power of the base, the delay is below the next one.

4. The source gauge rides in the base

theorem HCPolySupport.HighContrast.Quenched.growthBar_le_base {d : ℕ} {E : BlockMat d} {K : ℝ} (haspect : 1 ≤ aspectRatio E) (hK : 0 ≤ K) : growthBar K ≤ 2 + aspectRatio E * K

growthBar is below the telescope's own base. The source gauge needs no separate polynomial bound: the base already contains it.

5. The settlement, in the binder's quantifier order

6. The corrected-cadence prefactor interface

theorem HCPolySupport.HighContrast.Quenched.corrected_cadence_prefactor_of_uniform_cap {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {lAl : ℤ} {E : BlockMat d} {N₀ ns cA : ℕ} {A alpha b0 bA b2 S0 S1 S2 d0 base C cC c Cpref : ℝ} (hbase : 3 ≤ base) (hraw : 9 / 2 * ((1 + hatExcess P (roundedGrid lAl (canonicalMetric E)) N₀ 0) * 3 ^ (linRate A alpha b0 bA b2 cA S0 * ↑(linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 0))) * (Real.rpow 3 (linRate A alpha b0 bA b2 cA S0 / 2) + 1) ≤ C * base.rpow c) (hC : C ≤ base.rpow cC) (hCpref : Cpref = cC + c) : 9 / 2 * ((1 + hatExcess P (roundedGrid lAl (canonicalMetric E)) N₀ 0) * 3 ^ (linRate A alpha b0 bA b2 cA S0 * ↑(linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 0))) * (Real.rpow 3 (linRate A alpha b0 bA b2 cA S0 / 2) + 1) ≤ base.rpow Cpref

A coefficient/base cap for the corrected cadence prefactor, with the coefficient absorbed into the endpoint's base exponent. The left side and conclusion are the hpref input of hcore_body_of_corrected_design; the raw cap remains with the threshold arithmetic that produces it.