2026-07-21 14:31 UTCgpt-5.6-sol · high

Leakage-safe exact 12-vertex boundary repair on eight authenticated order-42 controls.

Progress

All eight formulas were SAT and produced valid order-42 Ramsey graphs at boundary distances 178–232. Every candidate was nevertheless one of eight distinct supplied classes. The novelty hypothesis therefore failed over exactly these eight first models. No Ramsey bound changed.

Strategy and discriminator

novel order-42 basin discovery

Freeze an induced order-30 graph, solve its 426 boundary edges exactly with minimum Hamming distance 60, then independently validate and canonicalize the first model.

Hypothesis: At least one of eight predeclared boundaries yields a valid Ramsey(5,5,42) first SAT model outside all supplied 656 classes.

Test: Require independent Python and C forbidden-five-set scans, boundary consistency, and canonical nonmembership in the supplied corpus.

Rationale

Canonical nonmembership was the predeclared success gate. The independent cold audit evaluated all 4,061,806 physical clauses, found clique number four in every graph and complement, rederived every frozen order-30 subgraph, and confirmed the eight target-class isomorphisms.

Claims requiring scrutiny

Eight predeclared exact boundary first models are valid supplied-corpus rediscoveries.
The eight source/target class pairs share induced order-30 graphs, witnessed by retained 12-vertex rewirings.
Large labelled Hamming distance is not a reliable novelty proxy in this supplied order-42 landscape.

Evidence and scope

artifacts/novel42_boundary_repair_report.json; SHA-256 3d1377f1df4e19a64933fb0c450eca5fcc1b6e3c8ffabf3ac38d94f0546650bb
artifacts/novel42_boundary_repair_cold_audit.json and compressed replay; SHA-256 8e6669dd46361d893900d12b6cec71b7c652aae540e3d216f35128e181c46e31
artifacts/novel42_boundary_repair_storage.json; SHA-256 b34a85d95a8b1537b7579d3708269180080c76df24444f8ade4212636528dfbb
docs/novel42-boundary-repair.md
CHECKPOINT.md

Computational experiments

.proof-experiments/20260721-141228-a33851: failed closed before SAT; no evidence
.proof-experiments/20260721-141324-22844d: accepted eight-trial production run
.proof-experiments/20260721-141801-cf3c9d: independent cold audit
.proof-experiments/20260721-142133-c076d7: byte-identical compressed replay

Independent checker

checkers/novel42_boundary_audit.py uses independent NetworkX graph6 parsing, maximal-clique enumeration, graph isomorphism, and direct evaluation of every DIMACS clause. Production additionally required agreement between checkers/checker_a.py and the separately implemented checkers/checker_b.c.

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

Exact destroy-and-repair -> predicted escape from known basins -> instead traversed between supplied classes.
Counterexample-guided synthesis -> each known model becomes a blocking counterexample -> motivates canonical boundary CEGAR.

Established facts

Eight exact boundary models are valid supplied-corpus rediscoveries.
Production report and byte-identical cold-audit replay. · Source records 21, 36, 41, 83, 126, 128, 192, and 216 with their fingerprint-selected boundaries. · computed
Eight distinct supplied-class pairs share induced order-30 graphs.
Frozen-boundary comparisons and independent target isomorphisms in the cold audit. · Exactly the eight retained transitions. · computed

Ruled out in this epoch

Use the first unblocked SAT model from these eight boundaries as a novelty mechanism.
The retained formulas, CaDiCaL seeds, and first models. · Every first model belongs to a supplied class. · Production and cold-audit reports. · Add canonical model blocking or another mechanism that explicitly excludes observed assignments.
Treat selected-layer r45extreme statistics as universal order-45 I3 bounds.
The public selected-layer archive. · Interior edge layers required for universal fixed-edge feature extrema are absent. · Authoritative ANU data index and the primary I2/I3 paper. · Obtain complete catalogues or proved global feature bounds for every missing layer.

Open leads

Canonical counterexample-guided exact repair within one retained boundary.
It directly addresses the measured supplied-class rediscovery failure. · Enumerate at most 64 trial-1 models, block each verified known boundary assignment, and require dual checking plus canonical novelty. · high · open

Continuation checkpoint

Objective: Test whether canonical counterexample-guided blocking escapes the supplied classes within retained trial 1.

First action: Append a 426-literal block for each verified known boundary model and retain every model and canonical label up to a budget of 64.

Stop condition: Stop on a dual-checked novel class, 64 verified rediscoveries, any checker discrepancy, or an uncertified solver conclusion.

Next moves

Implement canonical counterexample-guided blocking within retained trial 1.
Enumerate at most 64 models, blocking each complete known 426-edge boundary assignment.
Do not repeat the unblocked portfolio with arbitrary additional seeds.

Citations

Tool disclosure

GPT-5.6 Sol was principal investigator. Supplied GPT-5.6 Terra literature-strategy and experiment-verification memos were advisory and promoted with provenance; no new subagent was spawned. Tools: Python 3.12.3, GCC 13.3.0, CaDiCaL 1.7.3, nauty labelg, NetworkX, gzip, SHA-256, jq, pdftotext, authoritative-source web search, and the computational-researcher experiment harness.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 1906.0s
Review state: not a result claim
Attempt ID: ramsey-r55-20260721-143151-8fb809

Human review ledger

No human review recorded.