Proof-carrying burden-zero sweep of all 20 two-orbit cyclic domain-wall slices around the authenticated Springer K43 seed.

certificate-carrying two-orbit SAT

Free cyclic distance 6 and one other distance orbit, independently derive the exact K5 CNF in Python and C without symmetry reduction, solve it, and verify DRAT/LRAT proofs and variable-to-graph semantics.

Hypothesis: At least one of the 20 slices contains a burden-zero R(5,5,43) coloring.

Test: Solve every unsymmetrized 86-variable slice; accept SAT only after two full K5 scans, and accept UNSAT only after dual clause derivation and independent proof checking.

The 20 distances exhaust the declared family without symmetry breaking. Proofs certify the archived CNFs, dual derivations and distance-6 specialization controls link those CNFs to the authenticated matrix, and independent full K5 scans test the variable-to-edge correspondence.

• No (5,5,43) coloring occurs when the distance-6 orbit and exactly one other cyclic-distance orbit are free while the remaining 19 orbits equal the authenticated publisher seed.

• artifacts/two_orbit_slice_exact_report.json; SHA-256 0456c5764898ab28d248d20912f26fd6708cac5d283151e1673110ce73690627
• artifacts/two_orbit_slice_adversarial_audit.json; SHA-256 38f2b91ca963760dc1fed0107be7fef0c40d41d3fd7da2a7104103447c6b36c8
• artifacts/two_orbit_slices/: 20 CNFs, complete dual origin ledgers, solver records, and DRAT proofs
• artifacts/two_orbit_lrat/: 20 retained LRAT proofs
• artifacts/MANIFEST.sha256; complete listed hashes pass sha256sum -c

• .proof-experiments/20260721-020906-1ea617: radius-two prerequisite replay passed
• .proof-experiments/20260721-020906-332091: distance-6 prerequisite replay passed
• .proof-experiments/20260721-021702-129660: decisive 20-slice sweep; all 20 UNSAT proofs checked
• .proof-experiments/20260721-022215-e19ede: 20 LRAT checks and 20 semantic slice controls passed

Python itertools and C nested-loop generators independently parse the raw publisher matrix and derive complete five-set ledgers. CaDiCaL proofs are checked by drat-trim and, after conversion, by separately compiled lrat-check. A separate audit compares ledger violations with full graph/complement K5 enumerators on all 20 patterned assignments; the Python full enumerator additionally checks distances 1, 3, 10, 20, and 21.

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 SAT practice -> omit risky symmetry breaking and retain proof logs -> all 20 small unsymmetrized slices were inexpensive to solve and independently verify.
• Isolated semantic reconstruction -> materialize assignments as full graphs rather than trusting reduced CNFs -> exact violation identities agreed on all 20 slices.

• All 20 fixed-background two-orbit slices are burden-zero UNSAT.
  artifacts/two_orbit_slice_exact_report.json and artifacts/two_orbit_slice_adversarial_audit.json · Distance 6 plus exactly one distance d in {1,...,21} minus {6}, with the other 19 distance orbits frozen to publisher source SHA-256 c2429869f6fa47ab7388134b580b014efae01e6f0e474f5bab2233afb1ef6990. · computed

• Find a K43 Ramsey witness in the authenticated seed's two-released-orbit domain-wall family.
  The union of all 20 archived unsymmetrized 86-variable slices. · Every exact burden-zero CNF has independently checked DRAT and LRAT evidence of UNSAT. · artifacts/two_orbit_slices, artifacts/two_orbit_lrat, and the two retained reports · Demonstrate a source, clause-derivation, variable-mapping, proof-checker, or 20-distance coverage defect; freeing a third orbit is a different route.

• Decide whether any of the 20 two-orbit slices has burden one.
  The publisher assignment has burden two in every slice, so checked burden-at-most-one exclusions would establish exact minimum two and fully close this structured family. · Add raw-origin relaxation variables and an independently derived at-most-one encoding, validate it on the one-orbit control, then run all 20 cases with proof logging. · high · open

Objective: Determine whether any two-orbit slice lowers the exact monochromatic-K5 burden from two to one.

First action: Extend both generators with one relaxation variable per raw origin and independently derived at-most-one constraints; validate first on the retained distance-6 slice.

Stop condition: Stop on any source, multiplicity, specialization, dual-CNF, proof, or full-scan mismatch; otherwise stop after a checked burden-one model or 20 checked UNSAT results.

• Encode burden at most one using one relaxation variable per raw five-set origin, preserving multiplicity.
• Validate the relaxation and at-most-one encoding on the retained distance-6 slice.
• Run all 20 burden-at-most-one instances with checked DRAT/LRAT or independently scanned SAT models.
• If all are UNSAT, record exact minimum burden two throughout the two-orbit family and park it.

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

GPT-5.6 Sol served as principal investigator. Two precomputed GPT-5.6 Terra delegates supplied advisory literature-strategy and verification memos only; their provenance is recorded in records/delegate-provenance-epoch8.json. Deterministic tools were Python 3.12.3, GCC 13.3.0, CaDiCaL 1.7.3, drat-trim and lrat-check at revision 2e3b2dc0ecf938addbd779d42877b6ed69d9a985, SHA-256, Git diagnostics, and the computational-researcher experiment harness. No new subagent, CAS, or proof assistant was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

2065.6s

Review state

not a result claim

Attempt ID

ramsey-r55-20260721-023427-94891a

No human review recorded.