diff --git a/PAPER.md b/PAPER.md
index bf07089..25f6e2d 100644
--- a/PAPER.md
+++ b/PAPER.md
@@ -178,6 +178,14 @@ common difference; it fixes every class and the wildcard count. Requiring a
 colouring to be lexicographically no greater than its own reversal is therefore
 a sound lex-leader constraint, and it halves the search space.
 
+A note on what that soundness does and does not extend to: `i -> n+1-i` permutes
+*colourings*, which is all a lex-leader needs, but it is **not** an automorphism
+of the encoded CNF — the totalizer builds its auxiliary tree over positions in a
+fixed left-to-right order, so 86 of 2221 clauses at `n=45, j=8` are not preserved.
+That costs nothing here and no published value is affected, but it does rule out
+transporting proofs between symmetric cubes by renaming. Measured in
+`vdw/SIGMA-EQUIVARIANCE.md`.
+
 This matters more than it might appear. The pre-existing implementation broke
 only the symmetry between classes *sharing* a target value. A217058 has targets
 `3` and `4`, which differ, so that rule emitted **no clauses at all** and every
diff --git a/vdw/CENTRAL-CUBING.md b/vdw/CENTRAL-CUBING.md
new file mode 100644
index 0000000..b12f112
--- /dev/null
+++ b/vdw/CENTRAL-CUBING.md
@@ -0,0 +1,296 @@
+# Central-position cubing for vdw4 — what it is, what it is worth
+
+A measurement note, recorded 2026-09-17, on the central-position cubing that
+`vdw/vdw4.py` now offers as `split_positions()` / `make_cubes_pos()`, with
+`solve(split=...)` defaulting to `'prefix'` so nothing changes unless asked.
+
+Every number below was measured in this session on this machine, single-threaded,
+in-process, with pysat's `Cadical195` and `s.accum_stats()`. Conflicts and propagations
+are deterministic; wall-clock numbers are flagged where the box was shared.
+
+## Verdict in one paragraph
+
+The premise is essentially right and the patch's own claim reproduces: splitting on
+central positions instead of a prefix costs **1.50x–3.66x fewer conflicts** across five
+UNSAT instances in two families (2.10x–3.66x at k=6), and 3.24x fewer at the repo's
+headline configuration (n=45, j=8, [3,4], k=6). But the honest baseline kills it as a way
+to compute values: **cube-and-conquer with central splitting still costs 1.61x–5.30x more
+conflicts than simply solving the formula monolithically**, at every size tested. Central splitting does not
+turn cubing into a win, it makes a self-inflicted regression smaller. It is worth having
+for the **certification path**, where per-cube proofs are mandatory and the monolithic
+solve is not an option; there the patch cuts total proof work by ~3x and the hardest
+single cube by 3.2x. It is not a way to reach a(13) faster.
+
+One wall-clock caveat that cuts the other way is recorded in §7 — do not skip it.
+
+## 1. What the patch does
+
+`vdw/vdw4.py` currently splits on the first k **positions**: `make_cubes()` enumerates
+all class assignments of positions 1..k, drops a prefix that already contains a
+monochromatic target-length AP, that blows the wildcard budget, or (optionally) that
+violates the colour-symmetry rule.
+
+The patch adds, without touching `make_cubes()` or any existing default:
+
+- `ap_incidence(n, targets)` — how many target-length APs pass through each position.
+- `split_positions(n, k, mode, targets)` — `'prefix'` (unchanged behaviour),
+  `'central'` (the middle window of k positions), `'incidence'` (the k positions of
+  highest AP incidence).
+- `make_cubes_pos(n, j, targets, positions, colour_sym=False)` — `make_cubes()`
+  generalised to an arbitrary **set** of split positions. Cubes come back as tuples of
+  `(position, class)` pairs. A cube is dropped only when a clause already in `build()`'s
+  output refutes it: a monochromatic AP lying wholly inside the split positions, or more
+  than j wildcards among them.
+- `_cube_pairs()` — accepts both cube shapes, so `_cube_job()` is a one-line change and
+  legacy flat prefix cubes keep working unchanged.
+- `solve(..., split='prefix')` — new keyword; `'central'`/`'incidence'` route through
+  `make_cubes_pos`. Default behaviour is bit-for-bit what it was.
+
+`colour_sym=True` is **refused** off a prefix. See §4; this is the one place where a
+careless port of the existing code would produce a false term.
+
+## 2. The premise: AP incidence (claim partly confirmed, numbers corrected)
+
+Claimed: central positions carry far more AP incidence than a prefix — "248 vs 144 at
+t=3 and 212 vs 105 at t=4" at n=45.
+
+Measured at n=45, k=6 (sum over the six positions of the number of t-term APs through
+each):
+
+| | t=3 | t=4 |
+|---|---|---|
+| prefix, positions 1..6 | **144** | **105** |
+| central, positions 20..25 | **252** | **213** |
+| claimed central | 248 | 212 |
+
+The prefix figures reproduce **exactly**. The central figures do not: I measure 252 and
+213. I swept every contiguous 6-window at n=45. **No window at t=3 sums to 248** — the
+maximum over all 40 windows is 252, attained at 20..25 and 21..26. At t=4, 212 does
+occur, but only at the off-centre windows 15..20 and 26..31; every window from 17..22
+through 23..28 gives exactly 213, and 213 is the maximum. So one claimed figure is
+unattainable and the other belongs to a window that is not central. The direction and
+rough size of the effect (1.75x at t=3, 2.03x at t=4) are right, the figures are not.
+Do not quote 248/212; the central k=6 values at n=45 are 252 and 213.
+
+Full profile at n=45, t=3: incidence rises 22, 22, 24, 24, ... to 44 at position 23 and
+falls symmetrically. At t=4 it rises from 14 to ~36 and plateaus, oscillating between 35
+and 36 over the middle third — which is why 'central' and 'incidence' pick nearly the
+same positions and behave nearly identically everywhere below.
+
+## 3. Cube sets are exhaustive and sound (checked, not argued)
+
+- **Tautology over the split positions.** For every configuration tried, I enumerated all
+  (r+1)^k assignments of the split positions and classified each one: it is a cube, or it
+  is refuted by a named clause of F (a monochromatic AP inside the split set, or the
+  wildcard cardinality bound). Zero uncovered branches, zero cubes kept that F refutes.
+  Checked at n=45 j=8 [3,4] for k=4, 6, 8 in all three modes (e.g. k=6 central:
+  603 cubes + 126 AP-drops + 0 budget-drops = 729 = 3^6), and with a tight budget to
+  exercise the cardinality drop (n=45 j=3 k=8 central: 2914 + 2074 + 1573 = 6561), plus
+  n=35 j=2 [3,3] k=7 and n=55 j=4 [4,5] k=6 with a non-contiguous incidence set.
+- **Cubes are pairwise disjoint** over the split positions (no assignment in two cubes).
+- **Known witness lands in exactly one cube.** The n=44 j=8 [3,4] SAT colouring
+  (verified by `check`: 8 wildcards, no mono AP) falls in exactly 1 of the 603 cubes for
+  prefix, central and incidence splitting.
+- **Prefix mode is byte-identical to the repo.** `make_cubes_pos` on positions 1..k
+  returns exactly `make_cubes(..., colour_sym=False)` across 2520 configurations
+  (5 target pairs x n in 10..49 x j in 0..8 x k in 3..6), 0 mismatches.
+
+## 4. The trap: do not port the colour-symmetry rule to a window
+
+`make_cubes()`'s `colour_sym` rule orders the **first occurrences** of interchangeable
+colours. That is a statement about the whole word. Read off a central window it orders
+first occurrences *within the window*, which is not a symmetry of F — a colouring may
+legitimately start colour 1 outside the window and colour 2 inside it.
+
+This is not hypothetical. Measured: **[3,3] j=3 n=19 is SAT** (monolithic solve, 33
+conflicts; A217005 a(3)=20 so n=19 must be SAT). With a central k=6 window and the rule
+ported naively, plus the formula's own colour-swap symmetry breaking, the cube set
+returns **UNSAT** — a lost solution, i.e. exactly the failure mode that publishes a false
+new term. With `build(symbreak=False)` the same cube set returns SAT, which is why the
+bug can hide: it only bites when both symmetry breakings are on.
+
+The patch therefore raises `ValueError` if `colour_sym=True` is requested off a prefix.
+Non-prefix splitting always runs with the rule off, which is what certification requires
+anyway.
+
+## 5. Correctness: 13 OEIS rungs across four families, 0 disagreements
+
+Each rung solved through the cube path with the monolithic probe disabled, at k=6, in
+prefix and central modes (plus incidence on the first six rungs); every SAT answer
+re-verified by `check()`, which reads the colouring only and never the CNF.
+
+| family | j | a(j) | n=a(j)-1 | n=a(j) |
+|---|---|---|---|---|
+| A217058 [3,4] | 0,1,2,3,4,5 | 18,21,25,29,33,36 | SAT (verified) | UNSAT |
+| A217005 [3,3] | 0,1,4,5 | 9,14,21,24 | SAT (verified) | UNSAT |
+| A217007 [4,4] | 0,1 | 35,40 | SAT (verified) | UNSAT |
+| A217059 [3,5] | 0 | 22 | SAT (verified) | UNSAT |
+
+Plus the two big ones used for benchmarking: n=44 j=8 [3,4] SAT (verified, 8 wildcards)
+and n=45 j=8 [3,4] UNSAT, 2486 clauses, 1,396,228 conflicts — matching the recorded
+baseline exactly.
+
+13 rungs, i.e. 26 instances (each a(j)-1 and a(j)). The first six rungs ([3,4] j=0..3,
+[3,3] j=0,1) were run in all three modes, the remaining seven in prefix and central:
+64 solved instances in total, 0 disagreements with OEIS and 0 failed `check()`
+verifications.
+
+## 6. Benchmark (a): central vs the repo's prefix cubing — the claim holds
+
+Sum of conflicts and propagations over the whole cube set, every cube solved (no early
+exit), fresh solver per cube with the cube as assumptions, i.e. the repo's own
+`_cube_job` shape.
+
+| instance | k | split | cubes | conflicts (sum) | propagations (sum) | vs prefix | vs monolithic |
+|---|---|---|---|---|---|---|---|
+| **n=33 j=5 [3,3]** | - | **monolithic (no cubes)** | - | 4,710 | 235,763 | - | 1.00x |
+| n=33 j=5 [3,3] | 4 | prefix | 71 | 18,958 | 1,019,491 | 1.00x | 4.03x worse |
+| n=33 j=5 [3,3] | 4 | central | 71 | 10,568 | 598,164 | 1.79x | 2.24x worse |
+| n=33 j=5 [3,3] | 4 | incidence | 71 | 10,568 | 598,164 | 1.79x | 2.24x worse |
+| n=33 j=5 [3,3] | 6 | prefix | 522 | 40,803 | 2,266,556 | 1.00x | 8.66x worse |
+| n=33 j=5 [3,3] | 6 | central | 522 | 19,419 | 1,130,300 | 2.10x | 4.12x worse |
+| n=33 j=5 [3,3] | 6 | incidence | 510 | 19,640 | 1,151,517 | 2.08x | 4.17x worse |
+| **n=35 j=6 [3,3]** | - | **monolithic (no cubes)** | - | 9,117 | 437,345 | - | 1.00x |
+| n=35 j=6 [3,3] | 4 | prefix | 71 | 34,635 | 1,886,134 | 1.00x | 3.80x worse |
+| n=35 j=6 [3,3] | 4 | central | 71 | 23,151 | 1,350,224 | 1.50x | 2.54x worse |
+| n=35 j=6 [3,3] | 4 | incidence | 71 | 22,770 | 1,351,656 | 1.52x | 2.50x worse |
+| n=35 j=6 [3,3] | 6 | prefix | 523 | 99,458 | 5,711,974 | 1.00x | 10.91x worse |
+| n=35 j=6 [3,3] | 6 | central | 523 | 44,041 | 2,684,316 | 2.26x | 4.83x worse |
+| n=35 j=6 [3,3] | 6 | incidence | 523 | 44,041 | 2,684,316 | 2.26x | 4.83x worse |
+| **n=40 j=6 [3,4]** | - | **monolithic (no cubes)** | - | 175,224 | 6,410,524 | - | 1.00x |
+| n=40 j=6 [3,4] | 4 | prefix | 75 | 1,485,102 | 64,414,700 | 1.00x | 8.48x worse |
+| n=40 j=6 [3,4] | 4 | central | 75 | 712,483 | 34,247,977 | 2.08x | 4.07x worse |
+| n=40 j=6 [3,4] | 4 | incidence | 75 | 712,483 | 34,247,977 | 2.08x | 4.07x worse |
+| n=40 j=6 [3,4] | 6 | prefix | 603 | 3,818,704 | 197,439,174 | 1.00x | 21.79x worse |
+| n=40 j=6 [3,4] | 6 | central | 603 | 1,043,755 | 61,068,250 | 3.66x | 5.96x worse |
+| n=40 j=6 [3,4] | 6 | incidence | 603 | 1,043,755 | 61,068,250 | 3.66x | 5.96x worse |
+| **n=42 j=7 [3,4]** | - | **monolithic (no cubes)** | - | 913,916 | 27,457,287 | - | 1.00x |
+| n=42 j=7 [3,4] | 4 | prefix | 75 | 3,488,334 | 141,802,768 | 1.00x | 3.82x worse |
+| n=42 j=7 [3,4] | 4 | central | 75 | 1,474,177 | 66,045,152 | 2.37x | 1.61x worse |
+| n=42 j=7 [3,4] | 4 | incidence | 75 | 1,474,177 | 66,045,152 | 2.37x | 1.61x worse |
+| n=42 j=7 [3,4] | 6 | prefix | 603 | 10,508,539 | 479,222,774 | 1.00x | 11.50x worse |
+| n=42 j=7 [3,4] | 6 | central | 603 | 3,022,063 | 168,689,654 | 3.48x | 3.31x worse |
+| n=42 j=7 [3,4] | 6 | incidence | 603 | 3,022,063 | 168,689,654 | 3.48x | 3.31x worse |
+| **n=45 j=8 [3,4]** | - | **monolithic (no cubes)** | - | 1,396,228 | 42,924,439 | - | 1.00x |
+| n=45 j=8 [3,4] | 4 | prefix | 75 | 8,424,168 | 327,348,082 | 1.00x | 6.03x worse |
+| n=45 j=8 [3,4] | 4 | central | 75 | 2,984,075 | 130,827,127 | 2.82x | 2.14x worse |
+| n=45 j=8 [3,4] | 4 | incidence | 76 | 2,946,820 | 128,255,068 | 2.86x | 2.11x worse |
+| n=45 j=8 [3,4] | 6 | prefix | 603 | 23,980,575 | 1,031,616,290 | 1.00x | 17.18x worse |
+| n=45 j=8 [3,4] | 6 | central | 603 | 7,402,577 | 363,200,098 | 3.24x | 5.30x worse |
+| n=45 j=8 [3,4] | 6 | incidence | 597 | 7,554,095 | 368,396,939 | 3.17x | 5.41x worse |
+
+Central beats prefix in all ten comparisons: **1.50x–2.82x at k=4** (median 2.08x) and
+**2.10x–3.66x at k=6** (median 3.24x). The reported "~2.10x" is in range — it is exactly
+what I measure at k=4 on n=40 [3,4] (2.08x) and at k=6 on n=33 [3,3] (2.10x); at the
+headline n=45 j=8 k=6 the gain is larger, 3.24x, and at the smallest [3,3] instance at
+k=4 it is only 1.50x.
+
+`incidence` is not distinguishable from `central`: it picks the same or nearly the same
+positions and lands within 2% everywhere. Not worth the extra code path on its own; it
+is in the patch because it costs three lines and generalises to targets whose incidence
+profile is not symmetric.
+
+**Why it works, and a caveat on the explanation.** A control at n=40 j=6 [3,4] k=4,
+varying only the split positions:
+
+| positions | AP incidence | conflicts |
+|---|---|---|
+| 1,2,3,4 (prefix) | 140 | 1,485,102 |
+| 37,38,39,40 (suffix) | 140 | 1,036,244 |
+| 4,14,33,38 (random) | 186 | 1,177,417 |
+| 5,7,24,35 (random) | 197 | 1,107,832 |
+| 4,10,21,26 (random) | 226 | 914,304 |
+| 10,11,12,13 (quarter) | 230 | 913,548 |
+| 19,20,21,22 (central) | 276 | **712,483** |
+
+Conflicts fall broadly with incidence (the ordering is monotone once the two
+equal-incidence endpoints are set aside) — but note the suffix: same incidence as the
+prefix, 1.43x fewer conflicts. So incidence is not the whole story. Part of the prefix's
+weakness is that it overlaps the reversal lex-leader constraint, which already pins down
+the front of the word; fixing those same positions buys less new information. I did not
+chase this further, and the write-up should not claim incidence is the sole mechanism.
+
+## 7. Benchmark (b): central cubing vs just solving it — the honest baseline
+
+Same table, last column. Against a single monolithic `Cadical195` call on the same
+formula:
+
+| instance | monolithic | best cubing (central/incidence) | cubing penalty |
+|---|---|---|---|
+| n=33 j=5 [3,3] | 4,710 | 10,568 (k=4) | 2.24x worse |
+| n=35 j=6 [3,3] | 9,117 | 22,770 (k=4) | 2.50x worse |
+| n=40 j=6 [3,4] | 175,224 | 712,483 (k=4) | 4.07x worse |
+| n=42 j=7 [3,4] | 913,916 | 1,474,177 (k=4) | 1.61x worse |
+| n=45 j=8 [3,4] | 1,396,228 | 2,946,820 (k=4) | 2.11x worse |
+| n=45 j=8 [3,4] | 1,396,228 | 7,402,577 (k=6) | 5.30x worse |
+
+In conflicts, cubing loses at every size tested, with or without the patch. The patch
+narrows the loss (at n=45 k=6, from 17.2x to 5.3x) but never closes it. Deeper cubing is
+worse, not better: k=6 costs 2.5x the conflicts of k=4 in central mode at n=45.
+
+**The wall-clock caveat.** Conflicts are not seconds. Measured serially on an otherwise
+idle box, n=45 j=8 [3,4]:
+
+| run | conflicts | wall |
+|---|---|---|
+| monolithic (rep 1) | 1,396,228 | 79.8s |
+| monolithic (rep 2) | 1,396,228 | 78.6s |
+| central k=4, 75 cubes | 2,984,075 | **55.9s** |
+| central k=6, 603 cubes | 7,402,577 | 114.9s |
+| prefix k=4, 75 cubes | 8,424,168 | 212.6s |
+| prefix k=6, 603 cubes | 23,980,575 | 472.6s |
+
+So at k=4, central cubing runs ~1.4x **faster** in wall-clock than the monolithic solve
+despite 2.1x more conflicts: a cube's conflicts are cheaper than the monolithic run's,
+whose learnt-clause database grows large. Single-threaded and at this one size. That is
+one data point against my own summary, and it is the one worth re-testing before
+anybody concludes cubing is useless here: with 4 workers the k=4 central cube path would
+plausibly beat the monolithic solve outright in wall-clock. I did not measure the
+parallel path (the repo's `ProcessPoolExecutor`), and the per-cube CNF rebuild in
+`_cube_job` is included in these timings.
+
+The conflict-count statement ("cubing is a net loss") is therefore solid only as a
+statement about search work, not about elapsed time.
+
+## 8. Where it does help: certification
+
+`cube_certify.py` needs a DRAT proof per cube — the monolithic solve is not an
+alternative there, the per-cube work must happen. For that path the patch is a real,
+unambiguous gain:
+
+- total per-cube work at n=45 j=8 k=6: 23,980,575 -> 7,402,577 conflicts (3.24x).
+- hardest single cube at n=45 j=8 k=4: 323,555 -> 101,494 conflicts (3.19x). That is the
+  quantity that sets the makespan and the largest proof file.
+- 4-core LPT makespan over the same cube set: 2,113,920 -> 752,196 conflicts (2.81x).
+
+**Limitation, not yet done.** The patch changes the search path only. `cube_certify.py`
+and `cube_exhaustive.py` both call `make_cubes()` directly, parse cubes as flat class
+tuples, and walk a prefix tree. Using central cubes for a certification run requires
+extending those two files to the `(position, class)` shape and relabelling the tree walk.
+That generalisation looks mechanical — the tree is the same (r+1)-ary tree with different
+variable labels — but it is **not implemented and not tested here**, and the
+exhaustiveness DRAT tail in particular must be re-derived and re-checked before any
+certified value is claimed with central cubes.
+
+## 9. Plain statement of when to use it
+
+- Computing a new value of one of these sequences: **use the monolithic solve**
+  (`solve_direct`, or `solve(..., probe=...)` with a large budget). Cubing, prefix or
+  central, costs more search. The patch does not change that.
+- Running the certification pipeline, where per-cube proofs are mandatory: **use
+  `split='central'`**, k=4 rather than k=6, after extending the two certification tools.
+  Expect ~3x less total work and ~3x smaller hardest cube.
+- Never enable `colour_sym` with a non-prefix split. The patch refuses it; if you port
+  this code anywhere else, keep that refusal.
+- Do not quote the incidence figures 248/212; they are 252/213.
+
+## 10. Reproducing
+
+The measurements were driven by throwaway scripts that are not retained. The
+implementation they exercised is the one now in `vdw/vdw4.py`, so each section is
+reproducible from `split_positions()` and `make_cubes_pos()` directly: incidence
+sums (§2), cube-set exhaustiveness and disjointness (§3), the colour-symmetry
+hazard (§4), the rung sweep (§5), and the two benchmarks (§6, §7), each summing
+conflicts over the whole cube set in one process.
+
+Environment: python 3.11.15, python-sat 1.9.dev15, Cadical195, 4 cores, 15 GB.
diff --git a/vdw/SIGMA-EQUIVARIANCE.md b/vdw/SIGMA-EQUIVARIANCE.md
new file mode 100644
index 0000000..591758b
--- /dev/null
+++ b/vdw/SIGMA-EQUIVARIANCE.md
@@ -0,0 +1,248 @@
+# The sigma-equivariance trap: a symmetric constraint with an asymmetric encoding
+
+A measurement note, recorded 2026-09-17. Every number below was measured in one
+session against `vdw/vdw4.py` as it then stood, by throwaway driver scripts that
+are not retained; the properties they check are cheap to re-derive from the
+description in each section, and section 3 gives the exact clause-set comparison.
+Nothing here is copied from an earlier run.
+
+---
+
+## READ THIS FIRST: the published values are NOT affected
+
+**No published term of A217058, A217005, A217007, A217059 or A217236 is put in
+doubt by anything in this note.** The finding is about a *proof-engineering*
+technique that was never used to produce them.
+
+Two independent lines of evidence, both measured here.
+
+**(1) Verdicts are identical with and without the reversal lex-leader.**
+16 rungs — j = 0..3 for `[3,4]` (A217058) and `[3,3]` (A217005), each at both
+`n = a(j) - 1` (should be SAT) and `n = a(j)` (should be UNSAT) — solved three
+ways: `(symbreak=False, revsym=False)`, `(True, False)`, `(True, True)`.
+48 full solves, Cadical195, no cube split, no conflict budget.
+
+- disagreements between the three configurations: **0 / 16 rungs**
+- verdicts matching the published sequences: **16 / 16**
+- SAT witnesses re-verified by `vdw4.check` (reads only the colouring): **all pass**
+
+**(2) sigma is a semantic symmetry of the formula, cube by cube, exhaustively.**
+Over 6 instances and **2052 cubes total**, comparing `sat(F & cube)` against
+`sat(F & sigma(cube))` with `F` built symmetry-breaking-**off**:
+
+| instance | cubes | cubes where the two verdicts differ |
+|---|---:|---:|
+| n=24 j=2 `[3,4]` k=6 | 376 | **0** |
+| n=28 j=3 `[3,4]` k=6 | 530 | **0** |
+| n=33 j=4 `[3,4]` k=5 | 212 | **0** |
+| n=19 j=3 `[3,3]` k=6 | 450 | **0** |
+| n=16 j=2 `[3,3]` k=6 | 302 | **0** |
+| n=20 j=3 `[3,3]` k=5 | 182 | **0** |
+
+Perfect agreement, 2052 for 2052.
+
+This is the whole point, and it is worth stating precisely because it is easy to
+scare oneself with the headline finding below:
+
+> The paper's reversal argument is about the **colouring**, not about the CNF.
+> Reversal maps valid colourings to valid colourings (it sends a *t*-term AP to a
+> *t*-term AP and fixes the wildcard count), so requiring `colouring <=_lex
+> reversal(colouring)` keeps at least one representative of every orbit and
+> therefore preserves satisfiability. **That argument never needed sigma to be an
+> automorphism of the CNF.** A lex-leader constraint needs the symmetry to act on
+> the *solution set*; it does not care how the auxiliary variables are wired.
+
+So the headline finding is a real property of the encoding and a real obstacle to
+one specific *optimisation*, and it has no bearing on the published numbers.
+
+---
+
+## The finding: sigma is not a CNF automorphism
+
+Let `sigma : v(i,c) -> v(n+1-i, c)`, identity on every auxiliary variable.
+Build with `symbreak=False, revsym=False` so only the raw encoding is present.
+Clauses canonicalised as sorted tuples of distinct literals.
+
+| instance | clauses | `|F \ sigma(F)|` | `|sigma(F) \ F|` | automorphism? |
+|---|---:|---:|---:|---|
+| n=14 j=3 `[3,4]` | 270 | **24** | **24** | No |
+| n=45 j=8 `[3,4]` | 2221 | **86** | **86** | No |
+
+Both counts reproduce exactly. (For reference, with `symbreak=True, revsym=True`
+the same two instances are 355 and 2486 clauses; 96 / 386 variables raw.)
+
+### Attribution, demonstrated rather than asserted
+
+Each block tested separately for closure under sigma:
+
+| block | n=14 clauses | offenders | sigma-closed? | n=45 clauses | offenders | sigma-closed? |
+|---|---:|---:|---|---:|---:|---|
+| exactly-one | 56 | **0** | yes | 180 | **0** | yes |
+| AP | 68 | **0** | yes | 799 | **0** | yes |
+| cardinality (totalizer) | 146 | **24** | **no** | 1242 | **86** | **no** |
+
+The exactly-one and AP blocks *together* form a sigma-invariant set (checked
+directly: `True` at both sizes). Every clause of the symmetric difference — 48
+clauses at n=14, 172 at n=45 — lies in the totalizer block or is a sigma-image of
+one. **Confirmed: every offender is a totalizer clause.**
+
+The cause is exactly as suspected. The constraint "at most *j* of the `v(i,0)`
+are true" is completely symmetric in its inputs. The *totalizer* is not: pysat
+builds a binary counting tree over the literal list in the order given, and each
+internal node's auxiliary variables mean "at least *m* of *this subtree's*
+positions." Reversing positions permutes which positions sit under which node,
+but sigma leaves the auxiliary variables alone, so the mirrored clause talks
+about the old subtree with the new positions. The semantics survive; the syntax
+does not.
+
+### The repair works exactly
+
+Build the totalizer over the **reversed** literal list, same pool, v-variables
+allocated in the same order:
+
+| instance | forward clauses | reversed clauses | `sigma(forward) == reversed`? |
+|---|---:|---:|---|
+| n=14 j=3 | 146 | 146 | **True** |
+| n=45 j=8 | 1242 | 1242 | **True** |
+
+Exact clause-set equality, both sizes. (The forward totalizer is of course not
+sigma-invariant on its own — `False` — which is the finding restated.)
+
+So a sigma-equivariant encoding is available for free: emit both orderings, or
+choose an encoding whose auxiliary structure is itself mirror-symmetric. That is
+the precondition any per-cube proof-transport scheme would need.
+
+---
+
+## The second claim did NOT survive: drat-trim is not wrongly accepting anything
+
+The sharper claim was: renaming a DRAT proof under sigma yields an **invalid**
+proof that drat-trim nevertheless **accepts** (reported 9 of 12). The observable
+half reproduces. The interpretation does not, and I could not make it fail in
+any way that convicts the checker.
+
+**Setup.** A `drat-trim` binary already built in the working environment from
+upstream `drat-trim.c`, `sha256 = d834b649f437e091597f5347f259b9f681087f89ca0844d0cee250a1a1a0c2ee`,
+matching the hash recorded in `vdw/DRAT.md`. It could not be re-downloaded and
+re-compiled in that session (network blocked), so it was reused, not rebuilt.
+Checker controls run here: real proof vs UNSAT formula → `VERIFIED`; the same
+proof vs a satisfiable formula → `NOT VERIFIED`; bare empty clause → `NOT
+VERIFIED`. (A fourth "bogus lemma" control I wrote was not actually bogus — the
+lemma was genuinely RAT — so drat-trim was right to accept it. My error, noted
+so it is not mistaken for a checker fault.)
+
+**Correction to `DRAT.md`.** That file says pysat returns a truncated proof from
+*every* solver it ships. Measured here: `Cadical195`, `Cadical153` and
+`Cadical103` return **0 proof lines**, as described — but **`Glucose4` emits a
+complete proof ending in the empty clause** on these formulas, and drat-trim
+verifies it. All proofs below come from Glucose4.
+
+**Why the first result was vacuous.** Transporting proofs at n=25, j=2, `[3,4]`,
+k=5 gave **12 of 12 renamed proofs `VERIFIED`** — which looks alarming until you
+notice that `F` *itself* is UNSAT at n=25. Every cube target is UNSAT, so
+`VERIFIED` is a true verdict and no wrong acceptance is possible. That
+experiment cannot detect the thing it was meant to detect.
+
+**On a satisfiable base formula** (n=24, j=2, `[3,4]`, k=6, 120 cubes with
+transportable proofs), the pass rate is real but the failures are too:
+
+| renaming | target UNSAT → VERIFIED | target UNSAT → NOT VERIFIED | target SAT → VERIFIED |
+|---|---:|---:|---:|
+| sigma (reversal) | 88 | 32 | **0** |
+| rho (cyclic shift by 1) | 72 | 48 | **0** |
+
+So ~73% of sigma-renamed proofs still check — comparable to the reported 9/12 —
+but **every single acceptance is on a genuinely unsatisfiable target.** Nothing
+false was certified.
+
+**The acid test.** The only way to convict the checker is to hand it a renamed
+proof whose target is *satisfiable*. `rho`, a cyclic shift, is deliberately not
+a symmetry (APs wrap around the boundary). Scanning the 2052 cubes above found
+**17 cubes where `F & cube` is UNSAT but `F & rho(cube)` is SAT**. Transporting
+the UNSAT proof onto the SAT target in each case:
+
+| outcome | count |
+|---|---:|
+| drat-trim `VERIFIED` (would certify a falsehood) | **0** |
+| drat-trim `NOT VERIFIED` (correct rejection) | **17** |
+
+**17 of 17 correctly rejected.**
+
+**Conclusion.** The claim "the renamed proofs are invalid but drat-trim accepts
+them" is **refuted as stated**. A DRAT proof *is* valid exactly when each lemma
+is RAT against the accumulated formula and the empty clause is derived — which
+is what drat-trim checks. When sigma-renaming produces an accepted proof here,
+the proof genuinely is valid and the target genuinely is unsatisfiable, because
+sigma is a semantic symmetry (evidence: 2052/2052 above). When a renaming is
+*not* a semantic symmetry and the target is actually satisfiable, drat-trim
+catches it every time. There is no checker bug in evidence, and I would not
+write one up.
+
+What *is* true, and is the only defensible version of the claim:
+
+> Naive literal renaming under sigma is an **unreliable** proof-transport
+> shortcut, not an unsound one. 32 of 120 transported proofs failed to check
+> here, because the totalizer's auxiliary variables are not mirror-equivariant
+> and the renamed lemmas about them no longer propagate. Transport that is
+> *supposed* to work requires a sigma-equivariant cardinality encoding
+> (the reversed-input totalizer above gives one exactly).
+
+---
+
+## The precondition, stated once
+
+Per-cube proof transport under a geometric symmetry `s` of a problem needs two
+separate things, and they are easy to conflate:
+
+1. **`s` is a symmetry of the solution set.** This is what a lex-leader
+   symmetry-breaking constraint needs, and it is what `vdw4`'s reversal argument
+   establishes. It is about the colouring. **This holds here.**
+2. **`s` is an automorphism of the CNF**, i.e. the encoding is `s`-equivariant
+   including its auxiliary variables. This is what *renaming a proof* needs.
+   **This does not hold here**, and the sole reason is the totalizer's fixed
+   left-to-right tree.
+
+Condition 1 without condition 2 is the normal situation for any encoding with
+order-dependent auxiliary structure — totalizer, sequential counter, commander,
+most BDD-based cardinality encodings. Failing condition 2 costs you the
+*optimisation*. It does not cost you the *result*, and it does not make a
+checker unsound: the checker re-derives everything from the formula it is given
+and does not know or care that a renaming was involved.
+
+The trap is assuming that because the mathematics is reversal-symmetric, the CNF
+is too.
+
+---
+
+## Caveats
+
+- `drat-trim` was reused from an earlier session's build rather than rebuilt here
+  (network fetch and compile were blocked). Its hash matches upstream and it
+  passed the three negative controls listed above, but I did not compile it
+  myself in this session.
+- Proof emission worked only via `Glucose4`; the Cadical family returns empty
+  proofs through pysat, so the transport results rest on one solver's proofs.
+- Step 4 covers j = 0..3 in two families (16 rungs, 48 solves). It does not
+  reach the large j where the published headline terms live; the argument that
+  those are unaffected is the structural one in part (2) plus the cube scan,
+  not an exhaustive re-solve of the sequences.
+- The rho control found 17 danger cubes in 4 instances. Absence of a wrong
+  acceptance in 17 cases is strong but is not a proof that drat-trim has no such
+  bug.
+
+---
+
+## Appendix: baseline re-measured, so the build path is known to be the right one
+
+Single-threaded, in-process, Cadical195, `symbreak=True, revsym=True`,
+no cube split, no conflict budget:
+
+| instance | verdict | clauses | conflicts | wall |
+|---|---|---:|---:|---:|
+| n=44 j=8 `[3,4]` | SAT | 2395 | 61,398 | 1.3 s |
+| n=45 j=8 `[3,4]` | UNSAT | 2486 | 1,396,228 | 79.0 s |
+
+The conflict counts are deterministic and load-independent; the wall times on
+this box are not, and the 79.0 s should be read as "same order", not as a
+measurement. This is here only to confirm that the formulas analysed above are
+the same formulas the project actually solves.