review: retract the axis-separation claim and prediction 3

[InauguralPhysicist]

Adversarial review of my own ladder claims. Two withdrawn, one review hypothesis refuted, and the generator gets the structural oracle it should have had from the start.

F1 — RETRACTED: "the expansion axis is 8.4× steeper"

The headline compared steps with unequal variable increments — 3×3→4×4 adds 14 vars, 4×4→4×5 adds 8. Normalised:

step	axis	+vars	ratio	per-variable
3×3 → 4×4	expansion	+14	×48.39	1.319×
4×4 → 4×5	flat	+8	×5.77	1.245×
4×5 → 5×5	expansion	+10	≥×2.81	≥1.109×

Per-variable growth is monotonically decreasing and indifferent to which axis moved. And the only clean single-dimension expansion step (4×5→5×5, min 4→5) is ≥2.81× — lower than the flat step's 5.77×.

Design confound: 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 it is a size-matched pair: 4×6 (48 vars, min=4) vs 5×5 (50 vars, min=5) — and I killed 4×6 mid-run as "more of the same on the cheap axis", destroying the control for my own headline.

Prediction 2's 20× threshold still wasn't crossed, so nothing shows the rectangular axis is exponential either. Open question; 4×6 is the cheapest experiment that moves it.

F2 — WITHDRAWN: prediction 3 was vacuous

resolutions is cumulative and unbounded; peak_learnts is pinned to the reduction schedule (learnt_limit starts at 4, +2 per reduce run, so peak ≈ 4 + 2·runs — the banked 143/832/1619/1842 imply ~70/~414/~808/~919 runs). The climbing ratio restates the DB policy, not a property of Tseitin.

F3 — REFUTED (review hypothesis)

I suspected the 76→35 res/s decay was an artifact of count_active_learnts being O(total clauses) per conflict. Tested with an incremental counter: 4×4 went 429.2s → 410.4s, only 4.4%, counters byte-identical. Refuted — the decay isn't that scan, and "5×5 is out of reach under the interpreter" stands.

F4 — that optimization is a bad trade anyway

It adds an invariant only build_cdcl_state maintains; the hand-built reduce_state in test_solver.eigs broke instantly ("cannot compare none and num"). count_active_learnts derives from the arrays and needs no invariant. Both recorded in CLAUDE.md so neither is re-attempted.

What survives

• The generator is genuine. Every edge appears in exactly two vertices' incident lists; every vertex is degree-4 with distinct edges. Verified for 3×3, 3×4, 4×4, 4×5, 5×5, 3×7, 6×4. 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. Now tests/test_tseitin_invariant.eigs in the smoke suite, planted-fault validated (duplicating an incident edge makes it fail).
• Closed measurements: 1,974 / 95,516 / 551,098.
• DRAT oracle: single emission site, compaction doesn't route through it.
• Pigeonhole == coloring, refined: CNFs are not byte-identical (clause order differs) but identical var/clause counts and byte-identical counters.

🤖 Generated with Claude Code