Certified residual-SAT exclusion for the record-21 frozen order-30 core after blocking all eight supplied-class boundary vectors

complete known-class boundary blocking

Freeze a 30-vertex core, quotient the twelve residual labels by row-lex order, block eight validated 426-bit supplied-class assignments, and verify UNSAT with DRAT

Hypothesis: After blocking all eight boundary vectors induced by the validated supplied 656-class corpus, no Ramsey(5,5,42) completion remains in the record-21 frozen-core S12 row-lex quotient.

Test: Construct the exact 745-variable, 198920-clause CNF and run one seed-1 CaDiCaL solve, accepting UNSAT only after two drat-trim checks.

Exact reconstruction agreement, corruption controls, a retained physical CNF, and two proof checks support the scoped UNSAT conclusion. Incomplete cold census replay and absent external usefulness prevent candidate promotion.

• The physical CNF with SHA-256 cb3347f62affdb58e2c018fd156429165724ed1fc1375b17f7cdf20c85c81d54 is UNSAT.
• That CNF represents only the record-21 frozen order-30 core, S12 row-lex quotient, and eight exact supplied-class blocks.
• No conclusion about R(5,5) or all order-42 Ramsey graphs follows from this exclusion.

• Preflight: 196998 raw Ramsey clauses + 1914 lex clauses + 8 blocks; all three mutations rejected.
• CaDiCaL 1.7.3 seed 1: UNSAT in 3.801555 seconds.
• Production drat-trim: s VERIFIED in 2.544180 seconds.
• Fresh cold drat-trim: s VERIFIED in 2.482 seconds.
• Cold semantic replay: hosts 0..6 reproduced; checkpoint next_host=7.

• .proof-experiments/20260722-040756-4a31ae: preflight passed with exact counts and three rejected mutations
• .proof-experiments/20260722-041055-58db63: UNSAT in 3.802 seconds; production proof check passed
• .proof-experiments/20260722-041214-e6c3af: independently rebuilt drat-trim returned s VERIFIED
• .proof-experiments/20260722-041240-f41777: cold replay timed out as declared after checkpointing next_host=7

A separately written cold auditor reconstructs the formula without importing producer code, and a second fresh drat-trim build verified the physical proof. Its all-host semantic census replay is incomplete at 7/656.

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 exclusions -> compact fixed-core boundary -> rapid verified UNSAT
• Graph-label symmetry -> sorted residual core-neighbourhood rows -> covering S12 quotient
• Census deduplication -> exact assignment blocks -> 12 occurrences compressed to 8 clauses

• The maintained range remains 43 <= R(5,5) <= 46.
  Dynamic Survey DS1.18 and Angeltveit–McKay · Status checked through the April 24, 2026 survey revision · proved
• The blocked record-21 fixed-core row-lex CNF is UNSAT.
  CNF cb3347f6…d54 and DRAT a0f0e2e6…e231, verified twice · Exactly the retained 745-variable, 198920-clause formula · proved
• Cold semantic replay agrees through canonical host 6.
  Coverage checkpoint f8117ad7…b08e with next_host=7 · Supplied hosts 0..6 only · computed

• A ninth or otherwise unblocked completion exists in the represented record-21 frozen-core row-lex boundary family.
  The exact physical CNF after eight supplied-vector blocks · Verified UNSAT · DRAT proof a0f0e2e6…e231 and two s VERIFIED checks · A demonstrated mismatch in CNF generation, proof checking, block semantics, or symmetry coverage
• Promote the result as fully cold-validated now.
  Current epoch packet · Fresh semantic replay covers only 7 of 656 hosts. · cold-audit coverage checkpoint next_host=7 and absent final audit JSON · Complete all 656 host replays and final cold formula/proof audit

• Complete the cold all-host audit from its hash-bound host-7 checkpoint.
  This is the only missing internal validation step for the scoped fixed-core exclusion. · Run the unchanged cold auditor in a writable checkpointed lab with a progress-mirroring wrapper. · high · open
• Deletion-minimize one distance-3 two-orbit raw K5-origin core.
  It is a structurally different fallback if the cold audit or external usefulness gate fails. · Run duplicate-preserving minimization and stop unless the exact core has at most 20 origins. · normal · open

Objective: Independently validate the complete fixed-core UNSAT packet.

First action: Implement a wrapper around checkers/known_class_residual_sat_audit.py that mirrors next_host from artifacts/known-class-residual-sat-epoch20/cold-audit.json.coverage-checkpoint.json into lab progress JSON, then submit the unchanged auditor resuming at host 7.

Stop condition: Stop on any hash or semantic mismatch; validate only at next_host=656 with final physical DIMACS equality and cold drat-trim s VERIFIED.

• Create a lab wrapper that mirrors the unchanged auditor checkpoint into standard progress JSON without changing the auditor hash.
• Resume cold replay from host 7 and require all 656 hosts, physical DIMACS equality, and final cold drat-trim verification.
• If validation completes, ask an R(5,5) specialist whether this fixed-core exclusion materially benefits an accepted search.

• https://www.cs.rit.edu/~spr/ElJC/sur.pdf ↗
• https://arxiv.org/abs/2409.15709 ↗
• https://users.cecs.anu.edu.au/~bdm/papers/r55.pdf ↗
• https://users.cecs.anu.edu.au/~bdm/data/ramsey.html ↗
• https://arxiv.org/abs/1801.06620 ↗

GPT-5.6 Sol served as principal investigator. A supplied GPT-5.6 Terra experiment-verification memo was advisory and promoted with provenance; Sol independently reproduced every relied-on computation. No subagent was spawned. Deterministic tools: Python 3.12.3, NetworkX 3.3, CaDiCaL 1.7.3, GCC/cc 13.3.0, drat-trim pinned to 2e3b2dc0ecf938addbd779d42877b6ed69d9a985, nauty tools, SHA-256, exact Python/C graph checkers, and the computational-researcher experiment harness.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1207.7s

Review state

not a result claim

Attempt ID

ramsey-r55-20260722-042015-10c217

No human review recorded.