High-contrast homogenization: Provider.Quenched.SmallContrastAdaptiveDescent

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

The adaptive-depth descent: rounds of the floor cadence at doubling lag

the stated condition mechanism as an iteration: the family clause is consumed one step at a time, each step a proved cadence_profile_descent_floor (the corresponding clause) instance on the shifted sequence, with

• the round's quadratic anchored at the FIXED round lag L, so the anchor value is the previous level schedule level by antitonicity (F (r+k−L) ≤ F r), and the ∀ m slot of the corresponding clause is discharged by weakening;
• the pre-round drop history entering as the geometric echo A·ra^k·DS(r) ≤ A·ra^T·δ₀ (the shift recurrence iterationDropSum_shift), absorbed into the round's constant error;
• the level-adapted source bound src (r+k) (r+k−L) ≤ sE — the round's own M_λ charge.

The level schedule induction (the descent induction theorem) then propagates levels across rounds: any level schedule whose arithmetic is consistent (each next level covers the round's floor, each next start covers the round's firing region) yields F n ≤ lam j for n ≥ r j. The explicit level schedule and the geometric conversion are

theorem HCPolySupport.HighContrast.Quenched.iterationDropSum_shift (ra : ℝ) (F : ℕ → ℝ) (r k : ℕ) : iterationDropSum ra F (r + k) = ra ^ k * iterationDropSum ra F r + iterationDropSum ra (fun (j : ℕ) => F (r + j)) k

The drop history of a shifted sequence: the pre-history enters as one geometric echo.

theorem HCPolySupport.HighContrast.Quenched.adaptive_descent_stage {A alpha lam d0 sE : ℝ} {F : ℕ → ℝ} {src : ℕ → ℕ → ℝ} {ns r L T cA : ℕ} (hA : 1 ≤ A) (halpha : 0 < alpha) (hlam0 : 0 ≤ lam) (hsmall : 9 * A * lam ≤ 1) (hcA : 24 * A ≤ 3 ^ (alpha * ↑cA)) (hFnn : ∀ (n : ℕ), 0 ≤ F n) (hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p) (hFd0 : F 0 ≤ d0) (hd0 : 0 ≤ d0) (hsE : 0 ≤ sE) (hnsr : ns ≤ r) (hentry : F r ≤ lam) (hfam : ∀ (n m : ℕ), ns ≤ m → m ≤ n → F n ≤ A * iterationDropSum (3 ^ (-alpha)) F n + A * F m ^ 2 + src n m) (hsrcL : ∀ (k : ℕ), L ≤ k → src (r + k) (r + k - L) ≤ sE) (i k : ℕ) : max L T + i * (cA + 1) ≤ k → F (r + k) ≤ lam * (2 * A / (2 * A + 1)) ^ i + 8 * A * (A * (3 ^ (-alpha)) ^ T * d0 + A * lam ^ 2 + sE)

One round of the adaptive descent. From entry level lam at the round start r, the family clause at the fixed round lag L, the memory margin T, and the level-adapted source charge sE, the proved floor cadence grinds the level along the round's windows.

theorem HCPolySupport.HighContrast.Quenched.adaptive_descent_ledger {A alpha d0 : ℝ} {F : ℕ → ℝ} {src : ℕ → ℕ → ℝ} {ns cA : ℕ} {lam sE : ℕ → ℝ} {r L T ii : ℕ → ℕ} (hA : 1 ≤ A) (halpha : 0 < alpha) (hd0 : 0 ≤ d0) (hcA : 24 * A ≤ 3 ^ (alpha * ↑cA)) (hFnn : ∀ (n : ℕ), 0 ≤ F n) (hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p) (hFd0 : ∀ (n : ℕ), F n ≤ d0) (hfam : ∀ (n m : ℕ), ns ≤ m → m ≤ n → F n ≤ A * iterationDropSum (3 ^ (-alpha)) F n + A * F m ^ 2 + src n m) (hlam0 : ∀ (j : ℕ), 0 ≤ lam j) (hlamsmall : ∀ (j : ℕ), 9 * A * lam j ≤ 1) (hbase : d0 ≤ lam 0) (hr0 : ns ≤ r 0) (hsrcL : ∀ (j k : ℕ), L j ≤ k → src (r j + k) (r j + k - L j) ≤ sE j) (hsE0 : ∀ (j : ℕ), 0 ≤ sE j) (hstep : ∀ (j : ℕ), lam j * (2 * A / (2 * A + 1)) ^ ii j + 8 * A * (A * (3 ^ (-alpha)) ^ T j * d0 + A * lam j ^ 2 + sE j) ≤ lam (j + 1)) (hspace : ∀ (j : ℕ), r j + (max (L j) (T j) + ii j * (cA + 1)) ≤ r (j + 1)) (j n : ℕ) : r j ≤ n → F n ≤ lam j

The level schedule induction. An arithmetically consistent level schedule of levels, starts, lags, memories, and window counts propagates: the level lam j holds from the start r j on.