2026-07-21 16:46 UTCgpt-5.6-sol · high

Incremental 64-model labelled-primary CEGAR within the retained source-record-21 frozen order-30 boundary.

Progress

The exact budget of 64 distinct labelled models was reached. All were valid but occupied only supplied source classes 12, 18, 19, 20, 21, and 25. Boundary distances were 136-226. The cold audit passed and found eight destroy-permutation normal forms. No graph, class, boundary, or Ramsey bound was excluded.

Strategy and discriminator

canonical counterexample-guided exact repair

Parse the immutable boundary CNF once and append one 426-literal clause blocking each verified supplied-corpus primary assignment.

Hypothesis: Within 64 verified labelled completions, at least one valid Ramsey(5,5,42) graph is absent from the supplied 656 classes.

Test: Enumerate at most 64 distinct primary vectors, require base-CNF and prior-block satisfaction plus two full graph checks, and accept novelty only after canonical nonmembership.

Rationale

The novelty signal did not occur. The independently measured 64-to-8 label redundancy makes a larger arbitrary assignment cutoff low-value while identifying a concrete symmetry quotient for the next pass.

Claims requiring scrutiny

All 64 retained primary vectors are distinct and satisfy the immutable base and every earlier block.
The frozen source-record-21 order-30 core has compatible valid completions in at least supplied source classes 12, 18, 19, 20, 21, and 25.
All retained models have distinct destroyed-vertex core rows and collapse to eight normal forms under the destroy-label S_12 action.

Evidence and scope

artifacts/novel42_labelled_cegar64_report.json; SHA-256 8cd3f5b16649f5fab092c5624f345cca9b305e5ac6cac789152677720b6c332e
artifacts/novel42_labelled_cegar64_cold_audit.json; SHA-256 8c9af0b66c350bfff49b235093f183e037a4a57fc888709af18369bff7f7567c
artifacts/novel42_labelled_cegar64/blocks.dimacs; SHA-256 067cc2e42bee9fb40325865637621f69724bf40832408295548dff49d1a59fb1
artifacts/novel42_core_embedding_probe_epoch15.json; SHA-256 1c303c9ecbd282442b6285f0a7136b17424f8c7f0b8552d1b741dfedec44b219

Computational experiments

.proof-experiments/20260721-161659-700d02: 64 models in 609.167 seconds, 152472 KiB peak child RSS
.proof-experiments/20260721-162745-91d1f9: independent cold audit passed in 133.875 seconds, 79512 KiB peak child RSS
.proof-experiments/20260721-164245-525153: exact two-host induced-core cost probe

Independent checker

checkers/novel42_labelled_cegar_audit.py imports no producer and independently checks primary mapping, every base clause and prior block, graph/core/distance semantics, clique bounds, and target isomorphism. Production also required agreement between checkers/checker_a.py and 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

CEGAR assignment blocking -> 64 blocks should expose novelty if only a few labelled rediscoveries dominate -> all 64 remained in six supplied classes.
Group-action quotienting -> sorting distinct destroyed-vertex core rows should merge label copies -> 64 vectors reduced to eight normal forms.

Established facts

The retained frozen core has compatible valid completions in at least six supplied source classes.
Retained graph6 witnesses and independent target isomorphisms in the cold audit. · The six observed classes only; not a complete embedding census. · computed
The 64 retained labelled vectors occupy eight destroy-permutation normal forms.
Independent row reconstruction and normal-form hashes in the cold audit. · Exactly the retained 64 models. · computed

Ruled out in this epoch

Continue the identical labelled-blocking loop with a larger arbitrary cutoff.
The immutable record-21 base, incremental CaDiCaL configuration, and one-vector blocks. · The declared 64 vectors yielded no novel class and collapsed to eight S_12 normal forms; labelled blocks cannot exclude an isomorphism class. · Production and cold reports. · Install a proved class-level block or sound symmetry quotient, or demonstrate an artifact defect.

Open leads

Quotient the boundary by sorting destroyed vertices on their frozen-core adjacency rows.
Every completion has a row-sorted representative, and the current sample exhibits an exact 64-to-8 redundancy reduction. · Implement the lex CNF without the Hamming constraint and exhaustively test tied-row orbit coverage. · high · open

Continuation checkpoint

Objective: Test a sound destroy-label quotient before granting further boundary-search budget.

First action: Implement lex ordering of the destroyed vertices' 30-bit core rows after removing the Hamming counter, then exhaust every small tied-row control orbit.

Stop condition: Stop on a coverage defect, checker discrepancy, one dual-checked corpus-novel graph, or the predeclared normal-form budget.

Next moves

Remove the source-specific Hamming constraint because it is not invariant under destroyed-label permutations.
Impose lexicographically nondecreasing 30-bit core-neighborhood rows on the 12 destroyed vertices.
Exhaustively verify orbit coverage on small distinct-row and tied-row controls before one production solve.

Citations

Tool disclosure

GPT-5.6 Sol was principal investigator. Supplied GPT-5.6 Terra literature-strategy and experiment-verification delegates were advisory and promoted with provenance; Sol audited their claims and no new subagent was spawned. Deterministic tools were Python 3.12.3, GCC/G++ 13.3.0, CaDiCaL library 1.7.4, nauty labelg, NetworkX 3.3, gzip, SHA-256, and the computational-researcher experiment harness. Ubuntu libcadical-dev 1.7.4-1 was installed and recorded. No CAS, proof assistant, external publication, or remote account was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 2808.4s
Review state: not a result claim
Attempt ID: ramsey-r55-20260721-164650-ef8c5a

Human review ledger

No human review recorded.