Proved and independently checked a globally complete four-branch normalization based on seven triples uniquely covered by one root block, then ran matched bounded SAT telemetry.

unique-triple root-block normalization

Incidence averaging forces at least seven unique triples in some block; S5 reduces the 120 possible seven-subsets to four orbits, and blocks violating the selected uniqueness conditions are eliminated before CNF generation.

Hypothesis: Every hypothetical 54-cover is represented by one of four seven-unique-triple root-block branches, and at least one reduced branch will terminate or reduce matched 5000-conflict decisions by at least 20 percent.

Test: Exhaust all 120 selected seven-subsets under S5, independently reconstruct all four reduced CNFs, and compare two capped CaDiCaL seeds per branch against the unbranched link-cap baseline.

The incidence lemma is a direct counting proof, the four orbit sizes exhaust all 120 selections, and a separate implementation reconstructed every branch literal. These facts validate the structural reduction. UNKNOWN solver runs cannot support a cover or exclusion claim.

• Every hypothetical 54-cover has at least 370 uniquely covered triples.
• Some block in every hypothetical 54-cover uniquely covers at least seven triples.
• Up to the stabilizer of that block, four selected-seven patterns of sizes 20,10,60,30 cover all possibilities.
• Each canonical branch removes exactly 365 residual blocks and has 2637 primaries, 70842 total variables, and between 419624 and 419753 clauses.
• All eight capped solver runs returned UNKNOWN; no branch was solved.

• python3 scripts/root_block_seven_unique_cnf_v1.py --output-dir artifacts/root-block-seven-unique-triples-20260810 --manifest artifacts/root-block-seven-unique-triples-20260810/manifest.json
• Experiment 20260810-130906-cd6da1: independent C++ checker accepted all four branches.
• Experiments 20260810-130934-* and 20260810-130956/130957-*: eight matched CaDiCaL runs returned UNKNOWN.
• Experiments 20260810-131142-2ec62e, 20260810-131152-bf8787, and 20260810-131207-780c32 replayed the smoke proof; 20260810-131207-a363d6 rejected it against the wrong formula.
• Experiment 20260810-132156-fe6d09 accepted every frozen artifact hash.

• 20260810-125311-edc8a3: generated four branches with orbit sizes 20,10,60,30.
• 20260810-130906-cd6da1: independent C++ reconstruction accepted every branch.
• 20260810-130934-* and 20260810-130956/130957-*: all eight solver runs were UNKNOWN.
• 20260810-131142-2ec62e through 20260810-131207-a363d6: proof smoke passed and wrong-formula replay failed.
• 20260810-131519-2bd178: maintained 55-cover control covered all 455 triples and had a block with eight unique triples.
• 20260810-131550-398b20: fail-closed summary reported structural progress and failed telemetry gate.
• 20260810-132156-fe6d09: final hash-manifest integrity check passed.

checkers/check_root_block_seven_unique_cnf_v1.cpp independently enumerates subsets as packed masks, reconstructs S5 orbits, and compares every DIMACS literal without using the Python producer's data structures.

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome

no_progress

Public classification

no_progress

• C(12,6,4) certificate case splitting -> predict a small globally complete structural split -> observed four exact branches.
• Unlabeled graph/orbit classification -> predict the 120 selected seven-subsets collapse under S5 -> observed four orbits of sizes 20,10,60,30.
• Certificate-first SAT workflow -> require proof replay before solver scaling -> smoke DRAT/LRAT replay passed, but live UNKNOWN telemetry rejected scale-up.

• Every hypothetical 54-cover contains at least 370 triples of multiplicity one.
  540 total incidences minus 455 required incidences leaves excess 85. · All 54-block C(15,5,3) covers. · proved
• Some block uniquely covers at least seven triples.
  Averaging at least 370 unique triples over 54 blocks. · All 54-block C(15,5,3) covers. · proved
• There are exactly four S5 orbits on selected seven-subsets, with sizes 20,10,60,30.
  Python producer and independent C++ packed-mask census agree and sum to 120. · Seven-subsets of the ten triples in a fixed 5-set. · computed
• The four generated CNFs form a globally complete overlapping branch union.
  Incidence lemma, exhaustive orbit coverage, and independent literal reconstruction. · All hypothetical 54-covers up to relabeling. · proved
• All eight bounded live solver runs returned UNKNOWN.
  Hash-bound CaDiCaL 1.7.3 experiment receipts at two seeds per branch. · The four recorded formulas and 5000-conflict protocol only. · computed

• Scale the four current unique-triple CNFs unchanged.
  Four branches, two seeds, 5000-conflict CaDiCaL 1.7.3 runs. · Every run remained UNKNOWN and no branch met the 20 percent decision-reduction gate. · artifacts/root-block-seven-unique-triples-20260810/result.json · A new exact correlation, symmetry reduction, materially different encoding, checked SAT model, or complete replayable UNSAT proof.
• Use the failed Python checker attempts as validation.
  Experiments 20260810-125325-98df48, 20260810-125529-a20731, 20260810-125641-c46666, 20260810-125801-fe9874, and 20260810-125943-c8769a. · They timed out or hit memory limits before producing a valid result. · Fail-closed experiment records. · Not applicable; the separate C++ checker supersedes them.

• Unique-pattern and exact pair-skeleton coupling.
  It combines two global exact structures and can eliminate whole rooted skeleton orbits before SAT. · Enumerate compatibility across all 2145 rooted skeleton orbits and four unique patterns with two implementations. · high · open
• Proof-producing [3,2^6] representative extension leaves.
  A certified 14-leaf quotient exists for this local skeleton fibre. · Pilot the unique size-one leaf only if the global joint compatibility census does not dominate it. · normal · open
• Coverage-aware degree-preserving constructive search.
  A new defect below ten or a 54-cover would provide immediately checkable progress. · Design moves constrained by an exact pair skeleton rather than repeat the existing basin search. · low · open

Objective: Determine whether selected unique-triple patterns exclude exact rooted pair-excess skeleton orbits.

First action: Create a protocol reading artifacts/joint-orbit-census-20260808/manifest.json and artifacts/root-block-seven-unique-triples-20260810/manifest.json, then implement two exact compatibility maps.

Stop condition: Stop or redirect if all 2145 rooted skeleton orbits retain a compatible pattern or the two maps disagree.

• Read the existing 2145 rooted pair-excess skeleton orbit manifest and define compatibility with each selected-unique-triple pattern.
• Implement producer and independent checker for the complete joint orbit map.
• Stop if all 2145 rooted skeleton orbits survive; otherwise preserve whole-orbit exclusions.
• Generate further SAT leaves only if the joint quotient materially strengthens or compresses the four current branches.

• https://ljcr.dmgordon.org/cover/show_cover.php?k=5&t=3&v=15 ↗
• https://arxiv.org/abs/math/9502238 ↗
• https://arxiv.org/abs/2607.23766 ↗
• https://github.com/marijnheule/drat-trim ↗

GPT-5.6 Sol acted as principal investigator. GPT-5.6 Terra delegates supplied advisory prior-art and verification memos only; their assertions were independently audited and were not counted as validation. Python 3.12.3 generated CNFs, controls, and summaries. A separately written C++20 checker compiled with g++ 13 reconstructed the orbit union and formulas. CaDiCaL 1.7.3 ran the bounded searches and emitted the smoke DRAT. Project-scoped drat-trim and lrat-check verified and replayed the smoke proof. SHA-256 bound artifacts. Web search checked the maintained status and nearby primary literature.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

2468.7s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260810-132455-dc7f80

No human review recorded.