O9 scoping — what the nine-window table costs as an interval object

Date: 2026-08-13. Code: o9_scoping.py, test_o9_scoping.py (17 pins). Reads: RETENTION-PROBLEM.md §4 (the obligations) and §7 (the arithmetic). Writes nothing into the Lean package — this is a cost estimate for a build that has not started, produced before starting it rather than after.

Run:

.venv/bin/python hunts/frontier_math/o9_scoping.py
.venv/bin/python -m pytest -q hunts/frontier_math/test_o9_scoping.py

0. Why this file exists

RETENTION-PROBLEM.md §4 names O9 — the damage cap table on [28/5, 60] x [0, 1/2] — as "the only real work" left in the k = 1 retention chain, the other four open obligations being small. PROOF-LEDGER.md prices the same item as "the real remaining cost: a two-variable interval-arithmetic statement, the analogue of the BandCert leaf tables already in this package". Neither says how large that table is, and the number turns out to decide the shape of the build.

1. The headline

O9 as written cannot be held by interval arithmetic at all, and the reason is not size. The recorded caps c_k are defined in §4 as the supremum of Dam(y,s)/y^2 over each window box, rounded up. Recomputing them finds the supremum attained, to four figures, at an interior point of every window, always at y = 1/2:

An inequality that is an equality somewhere has no margin, and an enclosure of positive width can never close it: bisection refines forever around the maximiser. Measured, at inflation 1.00x the first window alone burns 14 398 leaves and still hits a depth-30 wall (test_the_bare_caps_do_not_terminate).

The same tangency appears a second time, at the window edges: I_k is by construction the set where Qim^2 - Qre^2 > 0, so on the complement the companion claim "no damage outside the windows" is an equality at every endpoint. Bare, the complement also fails to close (404 leaves, depth wall).

Both are presentational, and both have room to be fixed.

2. The two knobs, and how much each one has

Knob A — inflate the caps. O9 feeds §7 only as an upper bound, so replacing c_k by lambda * c_k weakens the statement in the safe direction. The cost is paid in the final arithmetic, where the caps enter through the integer trade P(c,q). Reproducing §7 exactly from the table:

Bisecting on lambda, the largest inflation §7 still absorbs is 1.3945x. That is the whole of the 1.6345x margin the chain already reports, spent on the windows alone.

Knob B — widen the windows. The recorded I_k are the damage support, and they sit in a [28/5, 60] interval at a 15.3 % duty cycle: width ~0.96 at spacing >6.16. Growing each window on both sides costs nothing on the cap side, because the added strips carry no damage — grid suprema over the widened boxes stay under c_k at every k (test_widening_a_window_does_not_raise_its_cap) — and it buys a strict margin on the complement.

But knob B has a ceiling, and it is O3, not taste. §5 step 3 groups the offsets inside one window and charges every pair of them Kpair >= 39/50, which O3 supplies only on |u| <= 1. A widened window wider than 1 holds two of its own points further apart than that, and the charge is gone: Kpair is decreasing there, and Kpair(1.01) = 0.77943 is already under 39/50. The widest recorded window is 0.9861, so

the widening may not exceed (1 - 0.9861)/2 = 0.00695.

This is asserted in o9_scoping.py rather than remembered. An earlier draft of this file recommended 0.02, which silently breaks O3.

3. The measured cost

Windows widened by 1/200 = 0.005 (inside the O3 ceiling), adaptive bisection on the longer side, Arb balls at 160 bits:

The complement, over the ten gaps between the widened windows:

Recommended operating point: inflation 1.20x, widening 1/200. That is 110 + 279 = 389 leaves, maximum depth 16, and it leaves the §7 arithmetic a surplus of 2.599e-02 against a budget of 1.2986e-01 — a 1.16x margin still in hand against the 1.3945x wall. The whole sweep runs in under a second.

For scale: BandCert/Data.lean, which already compiles in this package, records 3005 integers in 70 KB. O9 at the recommended point is roughly an eighth of that. Size was never the obstacle.

4. What the build actually needs

1. Qre_closed / Qim_closed are already kernel-checked (EForm3/ClosedForm.lean), so the enclosure never has to carry a quadrature. O9 is interval arithmetic on an explicit elementary expression — the same position BandCert was in.
2. One new leaf is needed: the removable branch Qim(y,s)/y. Writing the check as Qim^2 - Qre^2 <= c y^2 directly forces every box touching y = 0 to establish Qim^2 <= Qre^2, which is false at the zeros of Qre(0, .); that alone accounted for most of the cost in the first run of this probe. Rewriting it as y^2 (R^2 - c) <= Qre^2 with R = Qim/y removes the degeneracy. R needs sinh(a/2)/a, and Leaves.lean already carries the same device for sin(u/2)/u (its sfnL series), so this is a copy of an existing pattern rather than new machinery.
3. Argument reduction to s/2 <= 30. Leaves.lean L3 already has it, with a 2^-64 enclosure of pi.
4. The recorded table changes shape: nine rows of (s_lo, s_hi, cap) become nine widened rows with caps inflated 1.20x, plus a leaf list per window and per gap. Both numbers are small enough that decide — which is what Check.lean uses, not native_decide — stays plausible; that should be the first thing measured once the checker exists, since kernel reduction, not leaf count, is the real risk at this size.

5. Scope, and what this is not

This is a probe. It measures a cost and reports a shape; it lands nothing in zeta23ext and moves no obligation from open to closed. O9 remains open, the k = 1 chain remains at hardened grade, and k >= 2 — the 1.99x budget shortfall of PROOF-LEDGER.md, which is on the budget side and is not touched by anything here — remains the actual open mathematics. Nothing in this file is evidence about RH.

The grid suprema in §1 are grid maxima, so they are lower bounds on the true suprema: they can show a cap is attained, which is what they are used for, and they cannot show a cap is safe. The enclosure sweep in §3 is what carries the inequality, and it carries it for the inflated caps only.