2026-07-22 13:15 UTCgpt-5.6-sol · high

Mandatory source-and-reproducibility baseline plus an independently checked audit of the forced perfect-matching quotient for any hypothetical 40-block cover

Progress

The mandatory baseline is complete. The designated current source still reports 40 <= C(12,6,4) <= 41; the preserved 41-block witness covers all 495 four-subsets. A deterministic producer and materially different bitmask checker established the exact forced perfect-matching quotient and two-root split for any hypothetical 40-cover. No frontier search was run and the exact value remains open. The audit also found that this checkout lacks DRAT-trim, so historical Mac proof receipts cannot yet be freshly replayed here.

Strategy and discriminator

baseline invariant and symmetry audit

Source verification, incidence double counting, exact matching enumeration, fixed-matching block classification, and a separately implemented bitmask replay

Hypothesis: The maintained 40..41 status, published 41-block witness, and every arithmetic step forcing a unique excess perfect matching in a hypothetical 40-cover replay exactly under two materially different implementations.

Test: Enumerate all 924 candidate blocks and 495 targets, check the 41-block witness and a delete-one negative control, enumerate all perfect matchings, classify blocks by complete fixed pairs, then independently recompute every result using 12-bit masks and a matching recurrence.

Rationale

Outcome is progress, not candidate: the epoch produced reproducible source, script, checker, result, negative control, tests, method map, acceptance path, and continuation gate, but neither a 40-block witness nor a complete UNSAT certificate. The maintained status is supported by the La Jolla Covering Repository, while the successor Covering Repository provides the credible external reporting channel.

Claims requiring scrutiny

The preserved 41-block source witness contains 41 distinct 6-subsets and covers all 495 4-subsets of a 12-set.
Conditional on a 40-block cover existing, every point degree is 20 and the multiplicity-10 pairs form a perfect matching; every other pair has multiplicity 9.
There are exactly 10,395 perfect matchings on 12 labelled points and the stabilizer of a fixed matching has order 46,080.
For a fixed matching the 924 blocks have r-class counts [64,480,360,20], and the r=0-present/no-r=0-r=1-present split covers every feasible 40-block profile.
No exact-value improvement or novelty claim is made.

Evidence and scope

c1264-baseline-invariant-audit-v2 returned 0 in 0.34 seconds
artifacts/baseline/baseline-invariant-audit-20260722.json sha256 19eeec3e000fdb6e82083e3d13ed6f7638538a6d074f3ba528e305fa98d4e0c6
artifacts/baseline/baseline-invariant-audit-check-20260722.json sha256 47d01df56c03ce82e0a6c14e3ed4bd0a5f5f2ba7dfcdd2a955a2a7f28b9326f7
.venv/bin/python -m unittest discover -s tests -p test_*.py -v passed 47/47 tests in the recorded regression experiment
source receipt binds the maintained 41-block witness at sha256 395bc870e7eb9e84a472873db97de553afc34afdb666545824944e89047913e5

Computational experiments

.proof-experiments/20260722-130405-e8f38c: baseline invariant audit passed producer and independent checker; 924 candidates, 495 targets, valid 41-cover, delete-one control uncovered 10 targets, 10,395 matchings, r-counts [64,480,360,20]
.proof-experiments/20260722-130801-6879ad: all 47 repository unittest cases passed in 15.63 seconds

Independent checker

checkers/verify_baseline_invariants.py uses 12-bit subset masks, a dynamic perfect-matching recurrence, and independent profile enumeration rather than the producer's tuple/set incidence and recursive matching enumeration.

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

None recorded.

Established facts

The preserved 41-block witness covers all 495 four-subsets.
producer and independent bitmask checker; witness sha256 395bc870e7eb9e84a472873db97de553afc34afdb666545824944e89047913e5 · the exact block list in sources/ljcr-c1264-41.txt · computed
Any 40-block C(12,6,4) cover has point degrees all 20 and pair multiplicities 10 on a perfect matching and 9 elsewhere.
double counting from maintained C(11,5,3)=20 and C(10,4,2)=9; independently replayed arithmetic · conditional on existence of a 40-block cover · proved
The fixed-matching r classes contain 64, 480, 360, and 20 blocks, and the two root cases cover all 221 feasible r-profiles.
complete enumeration in producer and independent bitmask checker · all 924 six-subsets relative to the canonical matching and all nonnegative profiles satisfying the two incidence equations · computed

Ruled out in this epoch

Scale shallow depth-7 direct cubing unchanged under the prior 10-second leaf policy.
the pre-existing deterministic 64+64 sampled cubes across the two fixed-matching root CNFs · Only 10/128 leaves closed provisionally, 7.8125%, below the declared continuation threshold, and no leaf proofs were preserved/replayed in that sample. · artifacts/pilot/sample-r0-audit.json and sample-r1-audit.json with four hash-bound results.jsonl inputs · A materially stronger branching/encoding mechanism with a predeclared matched sample and replayed proofs.
Scale the prior Glucose4 incremental-assumption wrapper unchanged.
ten selected inherited hard-tail leaves under the recorded best-effort 1,000-conflict policy · Both cold and incremental modes closed 0/10, resource work was not matched, and the wrapper could overshoot limits; this is not evidence against incremental solving in general. · artifacts/pilot/link-orbit-incremental-tertiary-pilot-1000conflicts/result.json and audit.json · A reliably interruptible backend and resource-matched cold/incremental protocol with exact parent-plus-assumption equivalence.

Open leads

Restore a portable proof-replay toolchain before any UNSAT-producing frontier work.
It is the cheapest fail-closed test and prevents solver-to-CNF receipts from becoming non-reproducible on this host. · Pin official DRAT-trim source, build locally, hash it, and replay one small known proof plus one existing leaf receipt. · high · open
Matched kmtotalizer versus sequential-counter discriminator on inherited open link leaves.
It changes the propagation/encoding mechanism while retaining the strongest verified symmetry decomposition; PySAT officially exposes both encodings. · After the toolchain gate, dry-build both forms, independently audit totalizer structure and identical non-cardinality clauses, then run the deterministic 20-leaf paired tranche. · high · open
Positive search specialized to the forced matching and exact pair degrees.
A 40-block witness has a compact acceptance certificate and may be cheaper than a global negative proof. · Design a deterministic multi-seed local-search pilot whose moves preserve 40 blocks and score uncovered four-sets plus pair-degree violations; compare with unconstrained set-cover local search on a small fixed budget. · normal · open

Continuation checkpoint

Objective: Make proof replay portable, then determine whether kmtotalizer materially increases replayed closure on the inherited link frontier.

First action: Acquire the official DRAT-trim source at a pinned revision into a project-scoped toolchain and run checkers/replay_drat.py on a small known UNSAT CNF/proof pair.

Stop condition: Stop or redirect if toolchain hashes/verdicts disagree, cardinality/non-cardinality audits fail, the matched encoding tranche closes fewer than 8/20 leaves, or proof growth projects above 30 GB.

Next moves

Restore DRAT-trim from its official source at a pinned revision inside the problem workspace; record source, binary, and build hashes.
Replay a small known UNSAT control and one existing leaf proof; stop on any semantic, hash, or verdict mismatch.
Build sequential-counter and kmtotalizer versions of the same 11 link-degree equalities and add a structurally independent totalizer auditor plus non-cardinality clause diff.
Only after those gates, run the predeclared 20-leaf cold matched discriminator; promote only at 8/20 replayed closures with acceptable proof growth.

Citations

Tool disclosure

GPT-5.6 Sol principal performed source synthesis, experiment design, code review, and interpretation. A pre-existing gpt-5.6-terra experiment-verification memo was treated only as advisory and not as independent evidence. Deterministic work used Python 3.12.3 standard library, python-sat 1.9.dev7 only in inherited tests/artifacts, the repository's 47-test unittest suite, and web search/open for primary-source auditing. System CaDiCaL 1.7.3 was version/hash inspected but not used to solve this epoch; DRAT-trim was not present and no proof assistant, CAS, SAT frontier search, or external human validator was used.

Duration: 1199.6s
Review state: not a result claim
Attempt ID: covering-c1264-20260722-131509-6394f5

Human review ledger

No human review recorded.