High-contrast homogenization: Provider.Quenched.SmallContrastSplitWitnessCap

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

The burn-split witness is a power of the telescope base

The enlarged-witness cap: at the normalized gauge the minimal growth power is capped (K^{n+2} ≤ 2K³), and the burn-split witness burnSplitThreshold·K^{n+2} — hence its growth bar, and hence every crude-moment logarithm of the enlarged source — is bounded by a pre-law power of the telescope base 2 + Π·K.

theorem HCPolySupport.HighContrast.Quenched.exists_minimal_two_pow {K : ℝ} (hK : 1 < K) : ∃ (n : ℕ), 2 ≤ K ^ n ∧ K ^ (n + 2) ≤ 2 * K ^ 3

The minimal growth power at the normalized gauge.

theorem HCPolySupport.HighContrast.Quenched.crude_le_growth_pow (N : ℕ) {gK : ℝ} (h2 : 2 ≤ gK) : 1 + 2 * ↑N * (1 + Real.log gK) * gK ^ IndependentSums.natTriangular N ≤ (4 * ↑N + 1) * gK ^ (IndependentSums.natTriangular N + 1)

The crude moment constant is a growth-bar power.

theorem HCPolySupport.HighContrast.Quenched.three_zpow_max_le_mul {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 3 ^ max a b ≤ 3 ^ a * 3 ^ b

The nonnegative-max split for ternary powers.

theorem HCPolySupport.HighContrast.Quenched.three_zpow_intCeil_le (y : ℝ) : 3 ^ ⌈y⌉ ≤ 3 * 3 ^ y

The ceiling collapse at a nonnegative exponent.

theorem HCPolySupport.HighContrast.Quenched.three_rpow_mul_logb {x : ℝ} (hx : 0 < x) (c : ℝ) : 3 ^ (c * Real.logb 3 x) = x ^ c

The logb-power collapse: 3^{c·log₃ x} = x^c.

theorem HCPolySupport.HighContrast.Quenched.exists_burnSplit_witness_exponent (d : ℕ) (hd : 2 ≤ d) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {g : ℝ} (hg : g ∈ Set.Ico 0 1) : ∃ (cW : ℝ), 0 ≤ cW ∧ ∀ (K Pi : ℝ), 1 < K → 1 ≤ Pi → ∀ (n : ℕ), K ^ (n + 2) ≤ 2 * K ^ 3 → burnSplitThreshold d K (burnSplitAnchor d 1 K (burnSplitDepth d Cd g Pi)) (burnSplitAnchor d 1 K (burnSplitDepth d Cd g Pi) + ↑(2 * burnSplitDepth d Cd g Pi)) * K * K ^ (n + 1) ≤ (2 + Pi * K).rpow cW

The burn-split witness exponent.