review: retract the axis-separation claim and prediction 3

CLAUDE.md

@@ -157,23 +157,38 @@ The solver doubles as a proof-complexity instrument, because a CDCL refutation
   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 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.
+- **Tseitin closed measurements** (ladder run 2026-07-29,
+  `benchmarks/TSEITIN_LADDER.md` is the record of record): 3x3 = 1,974
+  resolutions (1.7s), 4x4 = 95,516 (429s), 4x5 = 551,098 (6,285s). 5x5 is out
+  of reach here — two attempts totalling 14.5h reached only 1,549,543 without
+  closing.
+- **RETRACTED 2026-07-30 (adversarial review): there is no measured "two axis"
+  separation.** An earlier version of this file claimed the expansion axis was
+  8.4x steeper than the fixed-expansion axis and told you to scale the square
+  dimension for hardness. That compared steps with unequal variable increments
+  (3x3->4x4 adds 14 vars, 4x4->4x5 adds 8). Normalised per variable the growth
+  is 1.319x, 1.245x, then `>=`1.109x — *decreasing*, and indifferent to which
+  axis moved. Worse, the only clean single-dimension expansion step in the data
+  (4x5 -> 5x5) is `>=`2.81x, which is *lower* than the flat step's 5.77x. The
+  size-matched control that could settle it is **4x6 (48 vars, min=4) against
+  5x5 (50 vars, min=5)** — and 4x6 was killed mid-run as "more of the same on
+  the cheap axis", destroying the control. Do not repeat the claim without
+  running 4x6.
+- **Do not read `resolutions` / `peak_learnts` as a size-vs-space finding.**
+  That ratio climbs by construction: `resolutions` is cumulative and unbounded
+  while `peak_learnts` is pinned to the reduction schedule
+  (`learnt_limit` starts at 4 and grows +2 per reduce run, so
+  `peak_learnts ~= 4 + 2 * reduce_runs`). It measures the DB policy, not the
+  formula family. A real size-vs-space result needs proof space for a *fixed*
+  refutation, not a policy-capped high-water mark.
+- **`count_active_learnts` is O(total clauses) and runs every conflict** (via
+  `reduce_learnt_db`), but it is NOT the bottleneck: replacing it with an
+  incrementally maintained counter bought only **4.4%** at 4x4 (429.2s ->
+  410.4s, counters byte-identical). Do not "fix" it — the incremental version
+  adds a state invariant that only `build_cdcl_state` maintains, and the
+  hand-built `reduce_state` in `tests/test_solver.eigs` breaks immediately
+  ("cannot compare none and num"). `count_active_learnts` derives from the
+  arrays and needs no invariant; that robustness is worth 4%.
 - **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

benchmarks/TSEITIN_LADDER.md

@@ -308,3 +308,78 @@ Either of these before any further 5x5 attempt:
 
 The ladder's central result (axis separation, x48.4 vs x5.77) does not depend
 on 5x5 and stands.
+
+# Adversarial review — 2026-07-30
+
+Review of this document's own claims. Two are withdrawn.
+
+## F1 — RETRACTED: the axis-separation result
+
+The "expansion axis is 8.4x steeper" headline compared **steps with unequal
+variable increments**: 3x3 -> 4x4 adds 14 variables, 4x4 -> 4x5 adds 8. Part of
+the x48.4 vs x5.77 gap is simply the bigger jump.
+
+Normalised per variable:
+
+| step | axis | +vars | ratio | per-variable |
+|---|---|---|---|---|
+| 3x3 -> 4x4 | expansion | +14 | x48.39 | 1.319x |
+| 4x4 -> 4x5 | flat | +8 | x5.77 | 1.245x |
+| 4x5 -> 5x5 | expansion | +10 | `>=`x2.81 | `>=`1.109x |
+
+Growth per variable is **monotonically decreasing and indifferent to which axis
+moved.** And the one clean single-dimension expansion step available
+(4x5 -> 5x5, where `min` goes 4 -> 5) is `>=`2.81x — *lower* than the flat
+step's 5.77x, i.e. currently the opposite direction.
+
+Note the design confound: starting from a square torus you cannot raise
+`min(r,c)` without adding both a row and a column, so "square cases" bundles
+expansion with a double-size jump. The step that breaks the confound is a
+**size-matched pair: 4x6 (48 vars, min=4) vs 5x5 (50 vars, min=5)**. 4x6 was
+killed mid-run as "more of the same on the cheap axis" — that judgement
+destroyed the control for the headline claim.
+
+**Status: the two-axis story is unsupported by this data.** Prediction 2's
+falsification threshold (20x) still was not crossed, so nothing here shows the
+rectangular axis *is* exponential either. The question is open, and 4x6 is the
+cheapest experiment that would move it.
+
+## F2 — WITHDRAWN: prediction 3 was vacuous
+
+"Space grows sub-linearly in size" is true but says nothing about Tseitin.
+`resolutions` is cumulative and unbounded; `peak_learnts` is pinned to the
+reduction schedule — `learnt_limit` starts at 4 and grows +2 per reduce run, so
+`peak_learnts ~= 4 + 2 * reduce_runs` (143, 832, 1619, 1842 imply ~70, ~414,
+~808, ~919 reduce runs). The ratio climbing is a restatement of the DB policy.
+A real size-vs-space result needs proof space for a *fixed* refutation.
+
+## F3 — REFUTED (a review hypothesis, not a prior claim)
+
+Hypothesis: the rate decay (76 -> 35 res/s) is an implementation artifact,
+because `count_active_learnts` is O(total clauses) and runs every conflict.
+Tested with an incrementally maintained counter: 4x4 went 429.2s -> **410.4s,
+just 4.4%**, with byte-identical counters. **Refuted.** The decay is not that
+scan, and the conclusion that 5x5 is out of reach under the interpreter stands.
+
+## F4 — the O(1) counter is a bad trade regardless
+
+It introduces an invariant only `build_cdcl_state` maintains. The hand-built
+`reduce_state` in `tests/test_solver.eigs` broke instantly with "cannot compare
+none and num". `count_active_learnts` derives from the arrays and needs no
+invariant — worth keeping for 4%, especially with the EigenOS ROM-bundle path
+constructing state independently.
+
+## What survives the review
+
+- **The generator is genuine.** Every edge appears in exactly two vertices'
+  incident lists, every vertex has degree 4 with four distinct edges, verified
+  for 3x3, 3x4, 4x4, 4x5, 5x5, 3x7, 6x4. That incidence-exactly-2 property is
+  what makes XOR-ing all vertex constraints cancel every edge and leave
+  `0 = sum(charges)`, so odd charge really does imply UNSAT.
+- **The closed measurements**: 3x3 = 1,974, 4x4 = 95,516, 4x5 = 551,098.
+- **The DRAT oracle.** Only one `add_cdcl_clause` site emits (learnt=1);
+  compaction does not route through it, so there is no double-emission. With
+  drat-trim verification plus the planted-fault rejection, the claim holds.
+- **Pigeonhole == coloring**, refined: the CNFs are *not* byte-identical (clause
+  order differs) but have identical variable and clause counts and produce
+  byte-identical solver counters. Same principle, as claimed.

tests/run_smoke.sh

@@ -8,6 +8,7 @@ EIGS="${EIGENSCRIPT_BIN:-$(command -v eigenscript || echo ../EigenScript/src/eig
 
 cd "$ROOT"
 "$EIGS" tests/test_solver.eigs
+"$EIGS" tests/test_tseitin_invariant.eigs
 "$EIGS" minisat.eigs tests/fixtures/simple_sat.cnf
 "$EIGS" minisat.eigs --watched tests/fixtures/simple_sat.cnf
 "$EIGS" minisat.eigs --persistent tests/fixtures/simple_sat.cnf

tests/test_tseitin_invariant.eigs

@@ -0,0 +1,53 @@
+# Structural oracle for the Tseitin generator: every edge must appear in EXACTLY
+# two vertices' incident-edge lists. That is what makes XOR-ing all vertex
+# constraints cancel every edge and leave 0 = sum(charges), so odd charge implies
+# UNSAT. Cheap (no solving), and it is the check that separates "a genuine Tseitin
+# formula" from "some UNSAT CNF that happens to look like one".
+load_file of "lib/int_vector.eigs"
+load_file of "lib/dimacs.eigs"
+load_file of "lib/solver.eigs"
+load_file of "lib/bench.eigs"
+
+# ADVERSARIAL INVARIANT: in a Tseitin formula every edge must appear in EXACTLY
+# two vertices' incident-edge lists. That is what makes XOR-ing all vertex
+# constraints cancel every edge and leave 0 = sum(charges), which is the whole
+# reason odd charge implies UNSAT. If any edge appears 1 or 3 times, the object
+# is not a Tseitin formula and every number banked from it is meaningless.
+for spec in [[3, 3], [3, 4], [4, 4], [4, 5], [5, 5], [3, 7], [6, 4]]:
+    rows is spec[0]
+    cols is spec[1]
+    counts is int_vector_filled of [(2 * rows * cols) + 1, 0]
+    degree_ok is 1
+    for r in range of rows:
+        for c in range of cols:
+            edges is tseitin_vertex_edges of [r, c, rows, cols]
+            if (len of edges) != 4:
+                degree_ok is 0
+            # distinctness within the vertex
+            for i in range of 4:
+                for j in range of 4:
+                    if i < j:
+                        if edges[i] == edges[j]:
+                            degree_ok is 0
+            for e in edges:
+                counts[e] += 1
+    bad is 0
+    lo is 99
+    hi is 0
+    for v in range of (2 * rows * cols):
+        n is counts[v + 1]
+        if n != 2:
+            bad += 1
+        if n < lo:
+            lo is n
+        if n > hi:
+            hi is n
+    verdict is "FAIL"
+    if bad == 0:
+        if degree_ok == 1:
+            verdict is "ok"
+    assert of [bad == 0, f"tseitin edge incidence != 2 for {rows}x{cols}"]
+    assert of [degree_ok == 1, f"tseitin vertex not degree-4-distinct for {rows}x{cols}"]
+    print of f"{rows}x{cols}: edges={2 * rows * cols} incidence_min={lo} incidence_max={hi} wrong_incidence={bad} degree4_distinct={degree_ok} -> {verdict}"
+
+print of "=== Tseitin structural invariant: ok ==="