High-contrast homogenization: Provider.Quenched.SmallContrastDescentStageArithmetic

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

The round arithmetic of the adaptive-depth descent

The descent at level-adapted lag proceeds in stages; this module collects the four arithmetic facts those stages live on.

• geometric_le_of_logb — the generic threshold: a geometric term C·3^{−rate·L} sits below a positive target once L exceeds the explicit logarithm. Instantiated twice downstream: the second error term S_Π·3^{−2(ν−γ)·L} at the level-adapted lag, and the drop-channel memory A·δ₀·ra^T at the stage length.
• the lag telescoping: when each stage at least doubles the level's logarithm, the SUM of the round lags is at most twice the final one. The total threshold is therefore linear in log₃ Π + log(1/λ_final), with no loglog accumulation: the round count enters only through the per-round constant factor.
• the first error term's absolute part: S·3^{2(γ·L − k)} ≤ S·3^{−2(1−γ)k} for any lag L ≤ k, hence below target for k past the explicit burn-in.
• the prefactor identity — the compounded per-stage constant C^J rewritten as 3^{J·log₃C}, the form hpref absorbs (the stage count J is logarithmic in the total scale, so this is the polylog factor).

theorem HCPolySupport.HighContrast.Quenched.geometric_le_of_logb {C target rate : ℝ} (hC : 0 < C) (htarget : 0 < target) (hrate : 0 < rate) {L : ℝ} (hL : Real.logb 3 (C / target) / rate ≤ L) : C * 3 ^ (-(rate * L)) ≤ target

A geometric term sits below a positive target past the explicit logarithmic threshold.