High-contrast homogenization: Provider.Quenched.SmallContrastCadenceGate

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

The cadence gates: depth reachability, the fixed margin, and the one-window dichotomy

Three gates, checked before the cadence induction.

(a) Reachability. The family quantifier of rows 346-347 reaches every fixed depth m ≤ Hw n (reachability, in the producers' own ℤ-clause form), and the window budget Hw n := n − b satisfies the producers' availability constraints exactly when the fixed bound sits at N₀ + b — the β-window/tree-window bridge is one inequality per constraint, not a construction.

(b) The margin. At the tree's constants the cadence window is a FIXED law-free depth, not the print-frame level-dependent M_λ: the tree's error is already exponential (deltaRec·ra^n), so level-dependence was paid into the rate, and the per-stage margin is c_A with 6A ≤ 3^(α·c_A) — which exists at c_A ≈ log₃(6A)/α and yields the head attenuation A·ra^(c_A) ≤ 1/6 (cadence_head_margin24).

(c) The one-window dichotomy (cadence_one_window_dichotomy): from one family member's recursion at a window of any depth, with the drop history split into the window's telescope and the attenuated head, EITHER the value collapses to four times the head-plus-error floor, OR it sits a strict (1+1/(2A))-factor below the window's top. The drop share and the error share are absorbed with the quadratic dominant — the budget every gate so far has asked for, and here it closes law-free because the plateau branch's quadratic is self-referential. The disjunction is unconditional given the standing smallness 9·A·F ≤ 1, so a cadence induction can consume it at every stage; and its short-window members force δ ≤ A·δ² + err on any flat stretch, which is false — the class admits no plateau, consistently with the membership finding for the staircase.

theorem HCPolySupport.HighContrast.Quenched.cadence_one_window_dichotomy {A Fn FW DS hd err : ℝ} (hA : 1 ≤ A) (hFn0 : 0 ≤ Fn) (hFW0 : 0 ≤ FW) (hsmall : 9 * A * Fn ≤ 1) (hrec : Fn ≤ A * DS + A * FW ^ 2 + err) (hDS : DS ≤ FW - Fn + hd) : Fn ≤ 4 * (A * hd + err) ∨ (1 + 1 / (2 * A)) * Fn < FW

(c) The one-window dichotomy. From one family member's recursion at any window, with the drop history split into the window telescope and the head: either the value collapses to four times the head-plus-error floor, or it sits a strict (1+1/(2A)) factor below the window's top.