2026-08-08 00:16 UTCgpt-5.6-sol · high

Authoritative baseline audit, derivation of forced pair/triple multiplicity structure, and independently reproduced exhaustive exclusion of the regular Z_15-invariant 30-block family.

Progress

The authoritative 30-31 status and historical method chain were audited. A promoted Terra cyclic enumerator was reproduced by a separate set-based implementation, exhaustively excluding the regular Z_15-invariant 30-block family and proving its maximum triple coverage is 440. Conditional pair- and triple-excess lemmas were derived. No unrestricted SAT search or exact-value claim was made.

Strategy and discriminator

pair-excess structural reduction with cyclic constructive control

Exact incidence counting converts a hypothetical cover into constrained excess multigraphs; translation-orbit enumeration then exhausts a sharply scoped constructive family.

Hypothesis: No simple 30-block C(15,6,3) cover invariant under the regular translation action of Z_15 exists, and forced pair multiplicities provide a stronger sound discriminator than point-degree pinning alone.

Test: Enumerate every feasible union of Z_15 block orbits using both a bitset implementation and a clean-room set implementation; separately derive the pair and triple excess identities.

Rationale

The cyclic result is supported by complete orbit coverage, two materially different implementations, deterministic experiment records, and a receipt replay. The structural identities follow by exact incidence double counting. Both results have explicitly limited scope, so they constitute progress rather than a candidate exact solution.

Claims requiring scrutiny

Any hypothetical 30-block cover has point degree 12 at every point.
Its pair excesses e_xy=lambda_xy-4 form a loopless 4-regular multigraph on 15 vertices with total edge multiplicity 30.
Its triple excesses satisfy sum_z(mu_xyz-1)=3+4e_xy, yielding five possible fixed-point link degree multisets.
No simple regular-Z_15-invariant 30-block cover exists.
The maximum triple coverage by such an invariant 30-block system is 440 of 455.

Evidence and scope

python3 artifacts/baseline-20260808/terra/check_cyclic_z15.py -> 335 orbits, 55,278 pairs, zero covers, maximum 440/455
python3 checkers/cyclic_z15_set_checker.py -> independent 5005-block partition guard, zero covers, maximum 440/455
python3 checkers/verify_cyclic_receipt.py artifacts/baseline-20260808/cyclic_z15_receipt.json -> VERIFIED
Human-checkable incidence derivations in artifacts/baseline-20260808/structural_lemmas.md

Computational experiments

.proof-experiments/20260808-001000-47f1ff: promoted Terra bitset enumeration, zero cyclic covers, maximum 440/455
.proof-experiments/20260808-001007-12e4de: clean-room set enumeration, full orbit partition guard, same result
.proof-experiments/20260808-001316-d76406: receipt and cross-output replay VERIFIED
experiments/first-pair-bounds-discriminator.json: designed but not launched

Independent checker

checkers/cyclic_z15_set_checker.py uses ordinary frozenset orbits and triple sets rather than the Terra bitset encoding; checkers/verify_cyclic_receipt.py independently verifies artifact hashes and cross-result agreement.

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

Certified C(12,6,4) link-orbit exclusion -> exact-degree links and dual proof replay should transfer -> verification tooling inventoried, target experiment not yet run
Classical simulated annealing for covering designs -> incremental pair/triple deficit kernels may cheaply seek a witness -> retained only as a constructive route because failure is non-evidence
Group-developed design search -> orbit closure converts a huge block selection into a small exact family -> regular Z_15 family exhaustively excluded

Established facts

The maintained range is 30 <= C(15,6,3) <= 31.
Maintained Covering Repository, legacy table row, and 1995/1996 upper-bound paper · Status audited on 2026-08-08 · computed
Every point has degree 12 in any hypothetical 30-cover.
C(14,5,2)>=12 and total incidence 30*6=15*12 · All hypothetical 30-block covers · proved
Pair excess is a loopless 4-regular multigraph, and triple excess satisfies the stated link identity.
artifacts/baseline-20260808/structural_lemmas.md · All hypothetical 30-block covers · proved
No simple regular-Z_15-invariant 30-block cover exists; the family maximum is 440 covered triples.
artifacts/baseline-20260808/cyclic_z15_receipt.json and two independent exhaustive implementations · Exactly 55,278 regular cyclic candidates · computed

Ruled out in this epoch

Two-orbit regular Z_15-invariant 30-block construction
Every simple 30-block family invariant under regular translations of Z_15 · Only two length-15 orbits can total 30, and all choose(333,2)=55,278 pairs fail direct triple coverage · artifacts/baseline-20260808/cyclic_z15_receipt.json · A demonstrated checker/orbit-partition defect or a materially different group action; merely rerunning the same family is not justified
Raise the lower bound above 30 using the existing first-moment/Schonheim counting chain alone
The recorded slack-zero incidence argument · All 180 point incidences are consumed by the forced minimum degree 12 · artifacts/baseline-20260808/structural_lemmas.md · A genuinely stronger structural inequality or certified exhaustive exclusion

Open leads

Pair-bound propagation pilot
Directly tests whether the new structural constraints reduce exact-search cost before any expensive case split · Run the four-formula protocol in experiments/first-pair-bounds-discriminator.json after controls · high · open
Canonical excess-multigraph split
Every hypothetical cover maps to a loopless 4-regular multigraph, potentially yielding an exhaustive isomorph-free frontier · Enumerate a small rooted canonical sample and compare residual CNF sizes only if pair bounds pass the pilot · normal · open
Constructive incremental local search
Exact degrees and pair deficits permit cheap delta evaluation, and a witness would settle the problem immediately · Run a bounded deterministic multi-seed control after the common incidence kernels are validated · normal · open

Continuation checkpoint

Objective: Determine whether pair multiplicity bounds materially improve the safest fixed-block exact formulation.

First action: Retrieve and independently check the archival 31-cover and pin cake_lpr, then implement the two truth-table-tested encodings specified in experiments/first-pair-bounds-discriminator.json.

Stop condition: SAT triggers direct witness validation; UNSAT triggers complete dual replay; less than 2x median conflict reduction in both encodings with no stronger signal redirects away from excess splitting; timeout remains neutral.

Next moves

Retrieve the exact archival 31-block cover and verify it with independent Python and C checkers plus duplicate/corruption controls.
Pin cake_lpr from its official source and validate it before accepting any future UNSAT result.
Implement and truth-table-test two independent cardinality encodings.
Submit the four-formula degree-only versus degree-plus-pair-bounds comparison to the checkpointed lab.
Enumerate canonical excess-multigraph cases only if the pair-bound pilot shows a material propagation benefit.

Citations

Tool disclosure

The GPT-5.6 Sol principal audited sources, proofs, and artifacts. Two GPT-5.6 Terra delegates supplied advisory prior-art and experiment-design memos; only the promoted cyclic bitset program was relied upon, and it was independently reimplemented and checked by Sol. Python 3.12.3 standard-library programs performed enumeration and hashing. Web search/retrieval checked current and primary sources. CaDiCaL 1.7.3 and a pinned drat-trim binary were inventoried but not used for a mathematical claim; cake_lpr was absent. No SAT solver, CAS, proof assistant, or frontier lab computation was used this epoch.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration: 998.4s
Review state: not a result claim
Attempt ID: covering-c1563-20260808-001644-974dd4

Human review ledger

No human review recorded.