bench: pre-register the Tseitin torus ladder + resumable long-run harness

[InauguralPhysicist]

Pre-registration, committed before any ladder data is collected so the predictions can be falsified rather than fitted after the fact.

Why a ladder

The two Tseitin points banked so far (3×3 = 1,974 resolutions; 4×4 = 95,516) conflate two axes. Tseitin refutations need size 2^Ω(expansion), and for an r × c torus expansion is governed by min(r, c):

• Expansion axis — 3×3, 4×4, 5×5. Where the exponential is claimed to live.
• Fixed-expansion axis — 4×4 … 4×7. Formula grows, min(r,c) stays 4, so hardness should grow much more slowly.

Predictions (registered)

1. 5×5 resolutions ≥ 20× the 4×4 figure (≥ ~1.9M). Within ~5× would falsify "min(rows,cols) is the hardness axis" — and the first suspect would be the generator (odd charge? four distinct incident edges?), not Urquhart.
2. Each 4×N → 4×(N+1) step multiplies resolutions by only ~1.3×–5×, matching the rows=3 reference (1,974 → 5,008 → 6,747 → 11,888). A step above ~20× breaks the two-axis story.
3. peak_learnts grows sub-linearly in resolutions. If space tracks size proportionally, learnt-DB reduction isn't working — that would be a solver finding, not a proof-complexity one.
4. 5×5 may well exceed its 6h cap. A capped result still counts: the progress trajectory bounds the answer from below.

Harness: built for the daily reboot

This box reboots ~05:57 (mac80211 CSA kernel bug), wiping /tmp and killing whatever runs. A plain nohup would lose the night. So:

• results land under ~/eigenminisat-runs, never /tmp
• each case is a separate timeout-capped process, appending as it goes
• cases already in banked.log are skipped → re-running resumes; a @reboot cron entry does it automatically
• flock stops the cron resume racing a manual run (4GB box — one heavy job at a time)
• progress every 300s via stdbuf -oL, so a killed case leaves a conflicts-vs-time trajectory instead of nothing

DRAT recording is off for the ladder — proofs buffer whole in memory (see GAPS.md) and a multi-million-step refutation would exhaust RAM.

Verification

• The runner reproduces the banked 3×3 numbers exactly (673 conflicts / 1,974 resolutions) through the budgeted-session path — cross-validates it against the one-shot solve
• Driver smoke-tested for resume-skip, timeout recording, and idempotent banking (exactly one DONE line after repeated runs)
• bash -n clean

No changes to the solver, the suite, or any existing bench mode — this is additive harness plus a registration document.

🤖 Generated with Claude Code