High-contrast homogenization: Provider.Quenched.SmallContrastCadenceFloor

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

The cadence descent at a constant error floor

The repair: the tree's family recursion carries a positive generation-independent source component in its error slot, so the deltaRec·ra^n clause of row 351 is not the producible shape. That induction, repeated stage-by-stage at a CONSTANT error E₀, closes with the descent terminating at the floor 8A·E₀:

F n ≤ delta·θ^i + 8A·E₀        for every n ≥ ns + i·(c_A+1),

with the same 24A margin and the law-free bookkeeping constants (8A, 16A) — the Q-step closes from 8A + 2/3 ≤ 16A and the collapse branch from (8/3)A + 4 ≤ 8A, both true at A ≥ 1. The descent to the floor takes ⌈log(δ/(8A·E₀))/log(1/θ)⌉ stages — a length proportional to the level's logarithm, which is what makes the outer bootstrap's total threshold linear: instantiating the design at the improved floor gives stage lengths that sum geometrically to the final level's logarithm.

theorem HCPolySupport.HighContrast.Quenched.cadence_profile_descent_floor {A alpha delta E0 : ℝ} {F : ℕ → ℝ} {ns cA : ℕ} (hA : 1 ≤ A) (halpha : 0 < alpha) (hd0 : 0 ≤ delta) (hE0 : 0 ≤ E0) (hsmall : 9 * A * delta ≤ 1) (hcA : 24 * A ≤ 3 ^ (alpha * ↑cA)) (hFnn : ∀ (n : ℕ), 0 ≤ F n) (hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p) (hFinit : F 0 ≤ delta) (hrec : ∀ (n : ℕ), ns ≤ n → ∀ (m : ℕ), ns ≤ m → m ≤ n → F n ≤ A * iterationDropSum (3 ^ (-alpha)) F n + A * F m ^ 2 + E0) (i : ℕ) : iterationDropSum (3 ^ (-alpha)) F (ns + i * (cA + 1)) ≤ 2 * delta * (2 * A / (2 * A + 1)) ^ i + 16 * A * E0 ∧ ∀ (n : ℕ), ns + i * (cA + 1) ≤ n → F n ≤ delta * (2 * A / (2 * A + 1)) ^ i + 8 * A * E0

The cadence descent at a constant floor.