Keep two measurement notes in the repo instead of nowhere - #8
Merged
Merged
Conversation
Both record work already done; neither changes any evidence or value. vdw/SIGMA-EQUIVARIANCE.md — the reversal map i -> n+1-i permutes colourings, which is all the lex-leader argument of PAPER.md 4.4 needs, but it is NOT an automorphism of the encoded CNF: the pysat totalizer builds its auxiliary tree over positions in a fixed left-to-right order, so 24 of 270 clauses at n=14/j=3 and 86 of 2221 at n=45/j=8 are not preserved. Every offender is a cardinality clause; the exactly-one and AP blocks are sigma-closed. Building the totalizer over the reversed input list gives exactly sigma applied to the forward one. The note leads with the fact that no published term is affected, and gives the evidence: 16 rungs x 3 symmetry configurations = 48 solves with 0 disagreements and every witness re-verified, plus 2052/2052 cube-level agreement on sat(F & cube) vs sat(F & sigma(cube)). It also records a claim that did NOT survive testing. An earlier draft asserted that sigma-renamed DRAT proofs are invalid yet drat-trim accepts them anyway. That was measured on a base formula which is itself UNSAT, where every VERIFIED is a true verdict and a wrong acceptance cannot be detected. Redone on a satisfiable base: 0 SAT targets verified, and a deliberately non-symmetric control was rejected 17 of 17. There is no checker bug, the note says so, and it is in the repo so the retraction is on the record rather than the accusation being left as a rumour. vdw/CENTRAL-CUBING.md — what the central-position cubing added earlier is actually worth. The premise partly reproduced: the prefix incidence figures are exact, the central ones are 252 and 213 rather than the 248 and 212 first claimed. Central beats the repo's prefix cubing by 1.50x-3.66x on conflicts, but section 7 states the honest baseline plainly -- cube-and-conquer at these sizes costs more conflicts than simply solving monolithically, so this narrows a self-inflicted regression rather than making cubing a faster way to compute values. Its value is on the certification path, where per-cube proofs are mandatory. Also adds one sentence to PAPER.md 4.4 pointing at the sigma note, since that is where a reader meets the reversal constraint. verify_all.py: 108 passed, 0 failed. scrub_paths.py --check: clean. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011dH16KSogC4aDoxznH1d5n
…aming Fixes the gate failure on the previous commit: scrub_paths.py reported "needs scrubbing: vdw/CENTRAL-CUBING.md". I had run scrub_paths.py --check before git add, and it only walks tracked files, so both new files were skipped. Checked this time with them staged. - vdw/CENTRAL-CUBING.md carried an absolute scratchpad path in section 10 and named the repo's own checkout path in its preamble. - vdw/SIGMA-EQUIVARIANCE.md carried an absolute scratchpad path to the driver script and described the drat-trim binary as "already present in this scratchpad". Both also opened by calling themselves private notes that had not been committed or published, which stopped being true the moment they were added to the repository. They now say what they are: measurement notes recorded 2026-09-17, driven by throwaway scripts that are not retained, against the code that is. CENTRAL-CUBING section 10 no longer lists script filenames that do not exist here. The implementation those scripts exercised is in vdw/vdw4.py, so it names what each section re-derives from split_positions() and make_cubes_pos() instead. No measurement, number or conclusion changed. scrub_paths.py --check: clean, with the files staged. verify_all.py: 108 passed, 0 failed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011dH16KSogC4aDoxznH1d5n
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Both notes record work already done. No evidence changes, no value is affected,
verify_all.pystays at 108/0.These existed only as scratch files outside the repo. That isn't preservation — putting them next to
DRAT.mdandBENCHMARKING.mdis.vdw/SIGMA-EQUIVARIANCE.mdThe reversal map
i → n+1−ipermutes colourings, which is all §4.4's lex-leader argument needs. It is not an automorphism of the encoded CNF: the pysat totalizer builds its auxiliary tree over positions in fixed left-to-right order, so 24 of 270 clauses atn=14, j=3and 86 of 2221 atn=45, j=8aren't preserved. Every offender is a cardinality clause — the exactly-one and AP blocks are σ-closed. Building the totalizer over the reversed input list gives exactly σ applied to the forward one.No published term is affected, and the note leads with that plus the evidence: 16 rungs × 3 symmetry configurations = 48 solves, 0 disagreements, every witness re-verified; plus 2052/2052 cube-level agreement on
sat(F & cube)vssat(F & σ(cube)).It also records a claim that did not survive testing. An earlier draft asserted that σ-renamed DRAT proofs are invalid but drat-trim accepts them anyway. That was measured on a base formula which is itself UNSAT — where every
VERIFIEDis a true verdict and a wrong acceptance is structurally undetectable. Redone on a satisfiable base: 0 SAT targets verified, and a deliberately non-symmetric control was rejected 17 of 17. There is no checker bug. The note says so plainly, which is the point of keeping it here — the retraction is on the record instead of the accusation surviving as a rumour.What does survive is narrower and useful: per-cube proof transport under a geometric symmetry requires a symmetry-equivariant cardinality encoding, and the default totalizer isn't one.
vdw/CENTRAL-CUBING.mdWhat the opt-in central-position cubing is actually worth.
The premise partly reproduced. The prefix incidence figures are exact (144 at t=3, 105 at t=4); the central ones are 252 and 213, not the 248 and 212 first claimed — a full 40-window sweep finds no 6-window at t=3 summing to 248.
Central beats the repo's prefix cubing by 1.50×–3.66× on conflicts. But §7 states the honest baseline: cube-and-conquer at these sizes costs more conflicts than simply solving monolithically, so this narrows a self-inflicted regression rather than making cubing a faster way to compute values. Its real value is the certification path, where per-cube proofs are mandatory and a monolithic solve isn't an option.
§4 documents the soundness trap already guarded in code: porting the colour-symmetry rule to a non-prefix window can lose a solution (
[3,3] j=3 n=19is SAT but returns UNSAT under a naive port).Also
One sentence in
PAPER.md§4.4 pointing at the σ note, since that's where a reader meets the reversal constraint and would want to know its limits.Verification
python verify_all.py→ 108 passed, 0 failedpython scrub_paths.py --check→ clean, no machine-local paths🤖 Generated with Claude Code
https://claude.ai/code/session_011dH16KSogC4aDoxznH1d5n
Generated by Claude Code