bench: bank the Tseitin ladder outcome — axis separation measured

CLAUDE.md

@@ -156,11 +156,29 @@ The solver doubles as a proof-complexity instrument, because a CDCL refutation
   are broken, not that the theorem is wrong. That makes the bench
   self-validating in the way a planted fault validates a checker.
 - Measured on this box: pigeonhole resolutions 39 -> 210 -> 1276 -> 12397 for
-  n = 3..6 (x5.4, x6.1, x9.7, multiplier rising). Tseitin 3x3 = 1974
-  resolutions; 4x4 = 95516 (x48 for one step of the expansion axis, ~450s).
-  The square axis is the real hardness axis, and it goes intractable
-  immediately under the interpreter — hence the odd/even control pair at 3x3
-  instead of a square ladder.
+  n = 3..6 (x5.4, x6.1, x9.7, multiplier rising).
+- **Tseitin has two axes and they are NOT the same** (ladder run 2026-07-29,
+  `benchmarks/TSEITIN_LADDER.md` is the record of record):
+
+  | axis | step | multiplier |
+  |---|---|---|
+  | expansion, `min(rows,cols)` grows | 3x3 -> 4x4 | **x48.4** |
+  | fixed-expansion, formula grows | 4x4 -> 4x5 | **x5.77** |
+
+  Closed cases: 3x3 = 1,974 resolutions (1.7s), 4x4 = 95,516 (429s),
+  4x5 = 551,098 (6,285s). The expansion axis is 8.4x steeper per step, so
+  **scale the square dimension when you want hardness and the rectangular one
+  when you want a bigger formula at constant hardness.** 5x5 exceeded a 6h cap
+  at 1.19M resolutions without closing — it is out of reach here.
+- Space is bounded, size is not: size/space (`resolutions` / `peak_learnts`)
+  climbs 14 -> 115 -> 340 across 3x3/4x4/4x5. Learnt-DB reduction is doing its
+  job; if that ratio ever stops climbing, suspect reduction before suspecting
+  the family.
+- **Long-run caps need margin, not point estimates.** 4x5 closed at 6,285s
+  against a 5,400s cap — missed by under 15 minutes and banked nothing but a
+  bound. A case that nearly closes banks exactly as little as one that never
+  started. Prefer one case with generous headroom over several that each nearly
+  finish.
 
 Honest ceiling: measurement bounds proof size from *above*. Every result that
 matters in proof complexity is a lower bound, and those are theorems. This

benchmarks/TSEITIN_LADDER.md

@@ -170,3 +170,75 @@ same single-case plan.
 expansion-axis multiplier is *decreasing*, which contradicts the rising-
 multiplier pattern pigeonhole shows. This ladder cannot settle that on this
 hardware — it needs either much more time or a faster runtime.
+
+# Outcome
+
+Banked 2026-07-29 20:40 CDT. Written after the predictions above, which are
+unedited. **5x5 is still running** — see the open item at the end.
+
+## Measurements (closed cases only)
+
+| case | vars | clauses | resolutions | conflicts | learnt_lits | peak_learnts | max_level | wall |
+|---|---|---|---|---|---|---|---|---|
+| 3x3 | 18 | 72 | 1,974 | 673 | 3,557 | 143 | 11 | 1.7s |
+| 4x4 | 32 | 128 | 95,516 | 27,388 | 208,781 | 832 | 20 | 429s |
+| 4x5 | 40 | 160 | 551,098 | 135,285 | 1,109,225 | 1,619 | 27 | 6,285s |
+
+## Prediction 2 — band missed, core claim CONFIRMED
+
+Predicted 1.3x-5x per fixed-expansion step, with ~20x as the falsification
+threshold. **Measured 4x4 -> 4x5 = 5.77x.**
+
+The narrow band is missed (5.77 > 5), so the prediction as stated is wrong at
+the margin. The claim it was testing survives cleanly: 5.77x is nowhere near
+the 20x that would mean the rectangular axis is also exponential.
+
+**The axis separation is real and now measured on both sides with closed cases:**
+
+| axis | step | multiplier |
+|---|---|---|
+| expansion (`min(r,c)` grows) | 3x3 -> 4x4 | **x48.4** |
+| fixed-expansion (formula grows) | 4x4 -> 4x5 | **x5.77** |
+
+The expansion axis is **8.4x steeper per step**. That is the ladder's central
+result and it holds.
+
+## Prediction 3 — CONFIRMED
+
+Space grows far slower than size; the size/space ratio climbs steadily, so
+learnt-DB reduction is bounding clause space rather than letting it track proof
+size.
+
+| case | resolutions | peak_learnts | size/space |
+|---|---|---|---|
+| 3x3 | 1,974 | 143 | 14 |
+| 4x4 | 95,516 | 832 | 115 |
+| 4x5 | 551,098 | 1,619 | 340 |
+
+## Prediction 4 — correct
+
+5x5 did exceed its 6h cap, and the trajectory bounded it from below as designed.
+
+## Calibration lesson
+
+4x5 closed at **6,285s** against an original cap of 5,400s — it missed by
+**884 seconds, under 15 minutes.** The first cap was within ~15% of sufficient
+and still produced nothing but a bound. Two things follow for future long runs
+on this box: budget caps with a real margin rather than a point estimate, and
+prefer one case with generous headroom over several that each nearly finish.
+A case that nearly closes banks exactly as little as one that never starts.
+
+## Open: prediction 1
+
+Unresolved. 5x5 needs `>= ~1.9M` resolutions to confirm; the 6h attempt reached
+1,194,575 (`>= 12.5x`) without closing. Relaunched 2026-07-29 20:35 with an
+8.5h cap. Outcomes:
+
+- closes anywhere `>= 1.9M` -> prediction 1 confirmed
+- closes below `~1.9M` -> prediction 1 **falsified**, and the expansion-axis
+  multiplier is *decreasing* (48.4x then under 20x), which would contradict the
+  rising-multiplier pattern pigeonhole shows and is the more interesting result
+- times out again -> bound tightens toward ~18x, still unresolved
+
+Note the asymmetry: a timeout can confirm this prediction but cannot falsify
+it. Only a closed 5x5 can do that.