2026-07-21 08:29 UTCgpt-5.6-sol · high

Symmetry-normalized proof-logging SAT pilot for the order-42 degree-{20,21} q=20 branch

Progress

All normalization, mapping, degree-counter, Ramsey-ledger, mutation, and small-instance controls passed. The production CNF had 71,421 variables and 1,844,093 clauses. CaDiCaL returned UNKNOWN after 300.226 seconds; peak child RSS was 524,756 KiB. No witness or exclusion was obtained, so 43 <= R(5,5) <= 46 remains unchanged.

Strategy and discriminator

symmetry-normalized certificate-carrying SAT

Represent every complement/relabel orbit by fixing N(0)={1,...,20}, independently audit the resulting 41 units, and run one bounded proof-logging SAT experiment.

Hypothesis: The fixed-root representative makes the q=20 almost-regular branch decidable by CaDiCaL 1.7.3 within 300 seconds and 1 GiB.

Test: Require the normalized formula to equal the retained unsymmetrized body plus exactly 41 audited units, then accept only a dual-checked SAT model, DRAT/LRAT-checked UNSAT proof, or explicit timeout.

Rationale

The experiment closes the saved discriminator honestly: the normalization is sound and reproducible, but it did not resolve the branch under the declared monolithic budget. Fresh drat-trim rejected the interrupted proof stream, preventing an UNSAT overclaim.

Claims requiring scrutiny

Every degree-{20,21} graph on 42 vertices has a complement/relabel-equivalent representative satisfying N(0)={1,...,20}.
The normalized production CNF is byte-for-byte the retained 1,844,052-clause unsymmetrized body followed by exactly 41 declared unit clauses.
The fixed-root CaDiCaL 1.7.3 configuration returned UNKNOWN at 300.226 seconds and therefore establishes neither existence nor nonexistence.

Evidence and scope

artifacts/almost_regular_42_q20_normalized_report.json; SHA-256 c0ee1711e81b6db391bf68a517662e55bd7a92dab3cdd2fab6f6e090a46c5a01
artifacts/almost_regular_42_q20_normalized_cold_audit.json; SHA-256 53b9f0da836d46e869d3c644afce5aff4ca64a8c9e6a3c53e8a5680e0412e626
Normalized CNF uncompressed SHA-256 87b70753dd07b3fc04ddb62799701a8a379efb2cd5c9ea9ddbd026f6679865dd
Root-unit ledger SHA-256 b3b4dfe90f2a1315386893d3ff9197258e046a8fe2372943f93c47253cefe7a6
CHECKPOINT.md contains exact replay commands, hashes, scope limits, and continuation.

Computational experiments

.proof-experiments/20260721-081112-052e15: normalized production run returned UNKNOWN after 300.226 solver seconds; total 336.833 seconds, peak child RSS 524,756 KiB.
.proof-experiments/20260721-081843-52c306: cold audit replayed formula and mutation checks and confirmed drat-trim return code 1 on the partial proof.

Independent checker

checkers/almost_regular_42_normalization_a.py does not import the generator and reconstructs the edge map, 41-unit ledger, base-formula identity, coverage control, and mutations. checkers/almost_regular_42_ledger_b.c independently regenerates all Ramsey clauses. Freshly compiled drat-trim independently rejected the partial production stream.

Contribution gate

not_requested

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

Original model outcome: progress
Public classification: progress

Cross-domain transfers tested

None recorded.

Established facts

The normalized q=20 formula has 71,421 variables and 1,844,093 clauses and is exactly the retained unsymmetrized body plus 41 units.
Production and cold normalization reports, including identical audit hash 7b5c4d6d3423068e4eef8f8352f55abbf628f6623312d5d46e9595a516f2be39. · The fixed-root order-42 degree-{20,21} CNF only. · computed
All 1,760 labelled six-vertex graphs in the degree-{2,3} band admit the analogous fixed-root representative; 70 exercise the complementation case.
Exhaustive scan of all 32,768 labelled six-vertex graphs in q20-normalized.audit-a.json. · Order six semantic control; the general coverage statement has a separate direct proof. · computed
The general fixed-root coverage lemma holds for all degree-{20,21} order-42 graphs.
Choose a degree-20 vertex; if none exists, complement the 21-regular graph, then relabel the root and its neighbors. · All simple order-42 graphs with every degree in {20,21}. · proved

Ruled out in this epoch

Repeat the identical fixed-root q=20 CaDiCaL 1.7.3 run with the same formula, options, 300-second limit, and 1-GiB ceiling.
The exact 71,421-variable, 1,844,093-clause configuration. · It returned UNKNOWN, so an identical replay has low information value. · .proof-experiments/20260721-081112-052e15 · Use a checked cube cover, materially different proof-logging solver or encoding, justified additional resources, or demonstrate an artifact defect.
Treat the normalized run's interrupted DRAT stream as an UNSAT certificate.
The 60,558,002-byte stream with SHA-256 9f62127fecf1f9ebd1b616e4768b7ea20d940da368d59f41c4a2ceca69f22a66. · Freshly compiled drat-trim returned 1 and did not verify it. · artifacts/almost_regular_42_q20_normalized_cold_audit.json · Obtain a completed proof that passes independent DRAT and LRAT checking.

Open leads

Benchmark a 16-leaf proof-carrying cube cover on the audited normalized q=20 formula.
A complete small cover tests resumability and leaf heterogeneity without repeating the failed monolithic configuration. · Branch on four deterministic cross-part edge variables, verify all 16 cubes independently, and run a short proof-logging leaf pilot. · high · open
Test q=17,18,19 only after a q=20 cube, solver, or encoding benchmark shows a material proof-cost improvement.
The normalized q=20 monolith still timed out, so identical runs in additional bands currently have low expected information value. · Retain the bands without executing them until the q=20 cost model changes. · low · open

Continuation checkpoint

Objective: Determine whether a tiny complete cube cover exposes tractable or heterogeneous leaves in the normalized q=20 branch.

First action: Implement a deterministic 16-leaf cover on four declared cross-part edge variables and validate its coverage and certificate path on normalized R(3,3,6).

Stop condition: Stop on any cover, mapping, or proof mismatch; otherwise stop if no production leaf resolves under the short pilot or projected certificate storage is not materially improved.

Next moves

Implement a deterministic 16-leaf cover on four declared cross-part edge variables.
Independently verify cube disjointness and complete coverage and validate the proof path on normalized R(3,3,6).
Run only a short production leaf-cost pilot; stop if no leaf resolves or projected certificate storage does not materially improve.

Citations

Tool disclosure

GPT-5.6 Sol served as principal investigator. Two supplied GPT-5.6 Terra delegates provided advisory literature-strategy and experiment-verification memos; Sol independently audited their claims, and no new subagent was spawned. Deterministic tools were Python 3.12.3, GCC 13.3.0, NetworkX 3.3, CaDiCaL 1.7.3, Debian nauty, drat-trim, lrat-check, SHA-256, and the computational-researcher experiment harness. 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: 1737.4s
Review state: not a result claim
Attempt ID: ramsey-r55-20260721-082900-aea66d

Human review ledger

No human review recorded.