Complete 16-leaf physical-CNF cube pilot on the normalized order-42 degree-{20,21} q=20 branch

certificate-carrying cube-and-conquer

Partition the frozen normalized formula on four declared cross-part primary variables, independently verify the cover and physical leaf reconstruction, and require a checked model or DRAT/LRAT certificate per resolved leaf.

Hypothesis: At least one of the 16 normalized q=20 leaves is decidable by CaDiCaL 1.7.3 within 20 seconds and 1 GiB with a checkable SAT model or UNSAT proof.

Test: First require all 16 normalized R(3,3,6) physical leaves to pass DRAT-to-LRAT conversion and LRAT checking; then execute all 16 q=20 leaves for 20 seconds each.

The predeclared tractable-leaf hypothesis was falsified for this exact configuration. The independently audited manifest/checker remains a reusable research artifact, but partial streams and timing variation provide no logical progress.

• Variables 212, 213, 234, and 235 define a complete, pairwise-disjoint 16-cube cover of the frozen normalized q=20 formula.
• The selected P5 pattern gives 10 path-reversal orbit classes, but all 16 raw cubes were retained and no symmetry quotient was used.
• All 16 normalized R(3,3,6) cube leaves have checked DRAT and LRAT certificates.
• All 16 production leaves returned UNKNOWN, and none of their retained streams is a valid DRAT certificate.

• artifacts/q20_cube16_pilot_report.json; SHA-256 864f2c67df3e963ba358e1c430880b1f2f39e89508830aca9fdfb06faa427251
• artifacts/q20_cube16_pilot_cold_audit.json; SHA-256 7e09c6ef485d05e5de2ff4a858c484289252b83f96969693d7d488ca73ffd812
• artifacts/q20_cube16_pilot/production/cube-manifest.json; SHA-256 d1d18434b21fbb66d40d936a60084fd5dfaaad5dcf5140f5a17d73871be12180
• Primary and cold manifest audits both have SHA-256 3c72ddc8e307fea078243ba72df74cd321ee930acd6d77020a81d03c4e136eff
• .proof-experiments/20260721-101546-136ce5/experiment.json; SHA-256 0d13b0caa5500d441c145039a95220b97acbba492dbdbadbdd12b2e6dc791444
• .proof-experiments/20260721-102428-af542e/experiment.json; SHA-256 5e1828729ef838804f3b46b018302b0a4fab6b6e9f355f14d4611f1cf2aa88e4

• .proof-experiments/20260721-101546-136ce5: 377.962 seconds total, 484396 KiB peak child RSS, 16 toy leaves verified and 16 production leaves UNKNOWN.
• .proof-experiments/20260721-102428-af542e: 155.831 seconds total, 411008 KiB peak child RSS, all toy certificates replayed and all production partial proofs rejected.

checkers/cube_manifest_a.py imports neither the producer nor Ramsey generator. It reconstructs the complete edge map, variables, assignments, suffixes, leaf hashes, disjointness, coverage, orbit ledger, and nine mutations. The cold audit freshly compiles drat-trim/lrat-check, reconstructs every production leaf, replays all toy certificates, and rejects every production partial stream.

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome

progress

Public classification

progress

• Certificate-carrying cube-and-conquer -> a small explicit partition may expose tractable leaf heterogeneity -> the verification pipeline succeeded, but all 16 production leaves remained UNKNOWN.

• The four-variable manifest exactly covers all assignments and reconstructs 16 physical q=20 leaf CNFs at locked hashes.
  Production manifest and identical primary/cold audit hashes. · Frozen normalized q=20 parent only. · computed
• All 16 normalized R(3,3,6) leaf proofs pass DRAT-to-LRAT conversion and LRAT checking.
  Primary and cold certificate replays. · Six-vertex control only. · computed
• All 16 production leaves returned UNKNOWN and all partial proof streams fail fresh DRAT verification.
  Primary pilot and cold-audit reports. · Exact CaDiCaL 1.7.3, 20-second-per-leaf configuration only. · computed

• Repeat the same four-variable q=20 cube pilot with CaDiCaL 1.7.3 and 20 seconds per leaf.
  All 16 physical leaf CNFs in the retained manifest. · Every leaf returned UNKNOWN; an identical replay has low information value. · artifacts/q20_cube16_pilot_report.json · Use a materially different proof-logging solver or encoding, justified branching/budget evidence, or demonstrate an artifact defect.
• Treat any retained production timeout stream as an UNSAT certificate.
  All 16 partial streams, totaling 128241561 uncompressed bytes. · Fresh drat-trim rejected every stream against its cold-reconstructed leaf CNF. · artifacts/q20_cube16_pilot_cold_audit.json · Supply a completed proof bound to the exact leaf hash and passing DRAT-to-LRAT conversion and LRAT checking.

• Test the exact adjacency-row pair-distance relaxation before constructing a custom SDP.
  It is a materially different, cheap structural discriminator with authenticated positive controls. · Extract exact row-weight, pair-intersection, and edge/nonedge distance distributions from all 656 controls and compare a rational pair-moment LP against published degree/subgraph restrictions for n=43–45. · high · open
• Revisit q=20 only after a solver, encoding, or branching change has a measured reason to alter certificate throughput.
  The monolith and every short cube leaf are currently unresolved. · Benchmark a materially different proof-logging configuration first on normalized R(3,3,6) and a declared bounded q=20 subset. · low · open

Objective: Run the cheapest exact adjacency-row pair-distance LP discriminator before any custom SDP or q=20 retry.

First action: Extract exact row-weight, pair-intersection, and edge/nonedge distance distributions from all 656 authenticated controls, then encode the rational pair-moment relaxation for admissible n=43–45 profiles.

Stop condition: Park the route if it cuts no profile beyond published constraints, cuts a known control, or yields only a numerical dual that cannot be rationalized and checked exactly.

• Park this exact cube configuration and do not launch q=17–19 from its UNKNOWN results.
• Run the saved exact adjacency-row pair-distance LP discriminator against authenticated controls and currently admissible n=43–45 profiles.
• Reopen q=20 only with a materially different proof-logging solver or encoding, justified branching evidence, or a demonstrated packet defect.

• https://www.cs.rit.edu/~spr/ElJC/sur.pdf ↗
• https://arxiv.org/abs/2409.15709 ↗
• https://github.com/marijnheule/drat-trim ↗

GPT-5.6 Sol was principal investigator. Two supplied GPT-5.6 Terra delegates provided advisory literature-strategy and experiment-verification memos; Sol independently audited all relied-on claims, and no new subagent was spawned. Deterministic tools were Python 3.12.3, GCC 13.3.0, CaDiCaL 1.7.3, freshly compiled drat-trim and lrat-check, the independent C recursive-bitset graph checker, SHA-256, jq, and the computational-researcher experiment harness. Web access checked DS1.18 and arXiv. No CAS, proof assistant, external publication, or system-level modification was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

2251.1s

Review state

not a result claim

Attempt ID

ramsey-r55-20260721-103733-ba8afb

No human review recorded.