2026-07-21 04:34 UTCgpt-5.6-sol · high

Proof-carrying raw-origin burden-at-most-one exclusion for all 20 fixed-background two-orbit cyclic slices

Progress

The hypothesis was falsified at its exact scope. All 20 slices are UNSAT under both independent encodings. The authenticated publisher assignment has burden two in every slice, so every slice has exact minimum burden two. This concerns only the declared fixed-background family and changes no Ramsey bound.

Strategy and discriminator

certificate-carrying two-orbit SAT

Assign one relaxation variable to every raw five-set/color origin, impose independently derived prefix and suffix sequential at-most-one constraints, solve both encodings, and verify DRAT, LRAT, specialization, and full-graph semantics.

Hypothesis: At least one of the 20 fixed-background two-orbit slices has raw monochromatic-K5 burden at most one.

Test: For each second distance, solve two unsymmetrized per-origin burden-at-most-one CNFs; accept SAT only after two exact full-graph scans, and accept UNSAT only after DRAT and LRAT verification.

Rationale

The two generators preserve all 33,626 raw origins and produce byte-identical origin ledgers and relaxation maps while using opposite-direction AMO encodings. All 40 DRAT proofs and all 40 converted LRAT proofs verified. Independent specialization, full-graph identity scans, and deliberate multiplicity, cardinality, mapping, and source mutations passed.

Claims requiring scrutiny

For every d in {1,...,21} minus {6}, when cyclic distances 6 and d are free and the other 19 distance orbits are frozen to the authenticated Springer matrix, the exact minimum number of monochromatic K5s is two.

Evidence and scope

artifacts/two_orbit_burden_one_exact_report.json; SHA-256 993adc7236b0c7a241b9d17457b28e144e745e7c2d890bae17ef9c81dcbf689f
artifacts/two_orbit_burden_one_adversarial_audit.json; SHA-256 0026e4d53f31b2fb8409bb52a0090035306cd6366e4a59c527bbc35b316167ff
artifacts/two_orbit_burden_one/ contains both CNFs, raw ledgers, mappings, and 40 checked DRAT proofs
artifacts/two_orbit_burden_one_lrat/ contains 40 independently checked LRAT proofs
CHECKPOINT.md records exact scope, sizes, hashes, commands, controls, and replay instructions

Computational experiments

.proof-experiments/20260721-040843-0eda2b: radius-two prerequisite replay passed
.proof-experiments/20260721-040843-9177f0: distance-6 exact-minimum replay passed
.proof-experiments/20260721-041736-6aa1db: 215-origin pilot passed with two checked UNSAT proofs
.proof-experiments/20260721-041804-395e81: all 20 slices UNSAT in both encodings; 40 DRAT checks passed
.proof-experiments/20260721-042400-d28272: all 40 LRAT checks and semantic/mutation controls passed

Independent checker

The Python generator uses direct itertools enumeration and a prefix AMO; the C generator uses five nested loops and a suffix AMO. A separately written audit reconstructs every formula, converts DRAT to LRAT, checks LRAT, specializes every ledger independently, and compares graph identities with separate Python and C full K5 enumerators.

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

Weighted MaxSAT per-origin relaxation -> duplicate graph clauses must retain distinct violation variables -> the distance-1 duplicate sentinel demonstrated that deduplication falsely makes a burden-two seed satisfy bound one.
Certificate-carrying SAT -> opposite-direction encodings should agree while retaining independently checkable proofs -> all 40 DRAT and LRAT certificate chains passed.
Adversarial software verification -> semantic mutations should fail for distinct reasons -> relaxation-sign, AMO-link, y-index, source-hash, and duplicate-merge controls were all detected.

Established facts

Every specified fixed-background two-orbit slice has exact minimum raw monochromatic-K5 burden two.
Dual per-origin UNSAT encodings, 40 checked DRAT proofs, 40 checked LRAT proofs, and the authenticated publisher burden-two assignment. · Exactly the 20 unsymmetrized slices freeing cyclic distance 6 and one other cyclic distance while freezing the remaining 19 orbits. · computed

Ruled out in this epoch

Lower the monochromatic-K5 burden below two in the fixed-background two-released-orbit family.
All 20 declared 86-edge slices. · Both raw-origin burden-at-most-one encodings are proof-checked UNSAT in every slice. · artifacts/two_orbit_burden_one, artifacts/two_orbit_burden_one_lrat, and the two retained reports. · Demonstrate a source, raw-origin multiplicity, specialization, cardinality, graph-mapping, proof-checker, or distance-coverage defect.

Open leads

Test the recognized almost-regular order-42 Ramsey slice with a deterministic degree-constrained SAT encoding.
None of the authenticated supplied 656 graphs is almost regular, so a valid result would be outside that corpus and address a named structural slice. · Hash-lock the corpus report, reproduce its degree spreads, validate the degree counter on small known instances, then run a 300-second/1-GiB proof-logging pilot. · high · open

Continuation checkpoint

Objective: Run the cheapest exact feasibility discriminator for the almost-regular order-42 slice.

First action: Hash-lock artifacts/authenticated_corpus_report.json, extract all supplied degree spreads, and implement a small-control-tested degree-spread-at-most-one counter.

Stop condition: Stop on any corpus, graph6, degree-counter, CNF-to-graph, proof, or full-scan mismatch; otherwise stop after a dual-checked new graph, a checked bounded exclusion, or the 300-second/1-GiB pilot timeout.

Next moves

Park the two-orbit family; do not release a third orbit without a new structural discriminator.
Run a bounded proof-logging feasibility pilot for the almost-regular order-42 slice after validating its degree counter on small controls.
Treat any pilot timeout as inconclusive and retain exact source, encoding, and proof artifacts.

Citations

Tool disclosure

GPT-5.6 Sol acted as principal investigator. Supplied GPT-5.6 Terra literature-strategy and experiment-verification delegates were advisory and are hash-linked in records/delegate-provenance-epoch9.json; their agreement was not evidence. Deterministic tools were Python 3.12.3, GCC 13.3.0, CaDiCaL 1.7.3, pinned drat-trim/lrat-check, SHA-256, Git diagnostics, and the computational-researcher experiment harness. No new subagent, CAS, proof assistant, external message, or publication action was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 2059.5s
Review state: not a result claim
Attempt ID: ramsey-r55-20260721-043422-7a2274

Human review ledger

No human review recorded.