Withdraw two unsupported performance claims; add opt-in central-position cubing

[Leo-Y-Zhang]

No mathematical result changes. No published term is affected. What changes is two performance claims that were measured in a way that could not have established them.

The measurement that prompted this

Permuting the clause order handed to the solver is semantically null — same clauses, same variables, same literals. On these instances it moves the conflict count by:

instance	spread
n=45, j=8 [3,4] — the benchmark	2.26× (16 permutations, 887,582 → 2,005,413)
n=42, j=7 [3,4]	1.56×
n=37, j=11 [3,3]	2.15×
n=44, j=8 [3,4] — SAT side	36.4× (19,766 → 719,703)

Conflict counts are deterministic — the same (instance, mode, seed) reproduces bit-for-bit — so that spread is the permutation and nothing else. Not solver-specific either (Cadical153 1.61×, Glucose4 1.40×, Minisat22 1.70×).

Bootstrapping from the 16 samples: two configurations that are genuinely identical, scored one run each, appear to differ by 1.89× at the 95th percentile. Even a median-of-9 protocol manufactures a 1.4× "speedup" from nothing one time in twenty.

Method, full numbers and the protocol to use instead are in the new vdw/BENCHMARKING.md.

What is withdrawn

1. PAPER.md §4.4 / paper/main.tex: the 1.55× revsym speedup. One timed run per configuration. Retested over 12 clause permutations per configuration on the monolithic path, all 24 runs UNSAT:

	N	min	median	max
revsym=True	12	887,582	1,386,901	2,005,413
revsym=False	12	1,009,244	1,194,370	2,117,652

Median ratio 0.861 — the opposite sign. Permutation test on the median difference, 200,000 relabelings: two-sided p = 0.347. The luckiest single pair in this data would have reported 2.39×, the unluckiest 0.50×; 1.55× sits unremarkably inside that.

The constraint is not withdrawn — only the number. The lex-leader argument is a proof of soundness, not a measurement, and it stands. This also does not settle the cube-and-conquer path, where the original figure was actually measured and which was not re-run. Both limits are stated in the text rather than glossed.

2. PAPER.md §4.5 / paper/main.tex: k=4 at 34.1 s against k=6 at 65.1 s. A 1.91× ratio from a single wall-clock pair, inside the floor above, on a shared machine. k=4 stays the default; that comparison doesn't establish it.

3. vdw/revsym_bench.py and vdw/engine_bakeoff.py both report one run per configuration; docstrings now say so. engine_bakeoff additionally doesn't give the engines the same clause order, and its "a 2× engine is worth an hour" framing sits right at the edge of what a 1.56×-floor experiment can resolve.

Also: opt-in central-position cubing

split_positions() and make_cubes_pos() in vdw/vdw4.py, with solve(split=...) defaulting to 'prefix' — nothing changes unless asked for. Splitting on the highest-AP-incidence window rather than the first k positions measured 1.50×–3.66× fewer conflicts summed over the cube set.

Verification

• make_cubes_pos on positions 1..k is identical to the existing make_cubes across 4 target pairs, with colour_sym both on and off
• 14/14 rungs across A217058, A217005 and A217007 correct through central cubes; every SAT witness re-verified by check(), which reads only the colouring and never the CNF
• Porting colour_sym to a non-prefix window is unsound — it can lose a solution ([3,3] j=3 n=19 is SAT but returns UNSAT under a naive port, which is the route to a false term). make_cubes_pos raises rather than allowing it; confirmed it still permits colour_sym on a genuine prefix.
• python verify_all.py → 108 passed, 0 failed
• python scrub_paths.py --check → clean

Caveat carried into the code

cube_certify.py and cube_exhaustive.py still assume prefix cubes. The certification benefit of central cubing is measured but not yet usable — that tail has to be re-derived before any certified value is claimed with central cubes. Noted in the commit message and the docstring.

🤖 Generated with Claude Code

https://claude.ai/code/session_011dH16KSogC4aDoxznH1d5n

---

Generated by Claude Code