Complete exact enumeration of the hash-bound archival 31-cover's three-delete/two-insert neighborhood using forced point-degree completion and two independent coverage encodings.

degree-completed constructive local exchange

For every deleted source triple, force the incidence sum of two additions from the global degree-12 lemma, enumerate every complementary split once, and test residual triple coverage.

Hypothesis: No 30-block cover is obtained from the exact archival 31-cover by deleting three distinct blocks and inserting two distinct 6-subsets not already retained.

Test: Exhaust all 4,495 deletion triples under forced degree completion; accept either a directly checkable witness or matching zero-repair outputs from packed-mask and independently structured frozenset scans.

The degree-12 lemma forces every possible two-block completion after each deleted source triple. Both implementations enumerate the complete forced frontier with materially different representations and agree exactly; the receipt checker binds scripts, source, metadata, and outputs. The quantified scope is only one fixed cover's neighborhood.

• For the archival 31-cover with SHA-256 289eed03daa87839214706723ff94bbf615f248044ef5591553daf89e120050a, no family formed by deleting three distinct blocks and inserting two distinct nonretained 6-subsets is a 30-block cover.
• Exactly 770 deletion triples admit degree-12 completion by two blocks; 754 also leave at most 40 triples uncovered; these yield exactly 18,313 valid unordered insertion pairs.
• The exact forced-completion kernel is smaller than the naive local representation space by 56,288,682,450/18,313.

• .proof-experiments/20260808-182508-3d8ab2: bitmask scan completed in 0.736 seconds with counts 4495,770,754,18313 and zero repairs.
• .proof-experiments/20260808-182514-c7913a: independent frozenset scan completed in 5.252 seconds with identical counts and zero repairs.
• .proof-experiments/20260808-182720-7ae9a1: receipt checker PASS over both runs and all bound hashes.

• .proof-experiments/20260808-182508-3d8ab2: complete bitmask local scan, zero repairs.
• .proof-experiments/20260808-182514-c7913a: independent set-based local scan, zero repairs.
• .proof-experiments/20260808-182720-7ae9a1: fail-closed receipt verification passed.

checkers/three_for_two_sets_v1.py uses frozenset triples, recomputes each retained union, scans all 5,005 first blocks, and derives the second pointwise; checkers/verify_three_for_two_receipt_v1.py separately validates hashes, metadata, outputs, and counts.

not_requested

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

Original model outcome

progress

Public classification

progress

• Exact-pinnability from slack-zero covering bounds -> predict pointwise forced completion after deletions -> reduced a 56.3-billion local representation space to 18,313 exact tests and both implementations confirmed the predicted frontier.

• The fixed archival 31-cover has no three-delete/two-insert repair to a 30-block cover.
  artifacts/epoch5-20260808/three_for_two_receipt.json and .proof-experiments/20260808-182720-7ae9a1. · All choose(31,3) source deletions and every distinct two-block completion around the exact source hash. · computed
• For each deleted source triple, any two inserted blocks that yield a 30-cover have pointwise incidence sum incidence_D(x)-(degree_F(x)-12).
  The proved global degree-12 lemma and incidence subtraction, independently instantiated by both enumerators. · Three-delete/two-insert transformations of the fixed source cover. · proved
• Exactly 18,313 valid unordered completion pairs remain after exact degree completion and sound capacity pruning.
  Matching independent experiment outputs and receipt check. · The exact archival cover only. · computed

• A three-delete/two-insert repair of the fixed archival 31-cover.
  Every triple of distinct source blocks and every pair of distinct 6-subsets not already retained. · Two independent complete scans found zero repairs. · artifacts/epoch5-20260808/three_for_two_receipt.json · A demonstrated source-hash, forced-completion, enumeration, or receipt-checker defect.
• Use only deletion triples containing one of the previous 165 favorable deletion pairs as an exact three-for-two search.
  The fixed archival cover's three-delete/two-insert neighborhood. · Exact degree completion leaves 754 deletion triples; the proposed restricted start family was not proved to cover this frontier, so the complete deletion loop was required. · Both complete programs explicitly loop over all choose(31,3) deletions. · A proof that every feasible repair contains one of the selected deletion pairs.
• Infer that no arbitrary 30-cover exists from the local miss.
  The global C(15,6,3) problem. · No theorem places every hypothetical 30-cover in this fixed cover's exchange neighborhood. · The receipt's explicit local scope. · A proved global neighborhood theorem or a complete independently replayed SAT exclusion.

• Five-seed matched pair-bound SAT confirmation.
  It is the prepared bounded discriminator closest to the global decision problem. · After a writable-registration signal, run bash scripts/submit_pair_multiseed_lab_v1.sh and require a durable job ID. · high · open
• Bounded rooted pair-excess-multigraph residual comparison.
  It can measure whether structural cubes shrink the global SAT frontier without launching a proof-scale search. · Enumerate one predeclared rooted excess profile and compare residual variables, clauses, and short-run propagation with the unsplit pair-bound CNF. · normal · open

Objective: Obtain global information by executing the prepared pair-bound SAT discriminator or, if still externally blocked, by measuring a structural excess-multigraph partition.

First action: Check for an explicit writable lab-registration signal; if present run bash scripts/submit_pair_multiseed_lab_v1.sh, otherwise instantiate one bounded rooted excess-multigraph comparison without retrying the blocked submission.

Stop condition: A SAT witness triggers dual direct validation; a failed pair-bound gate redirects; provisional UNSAT triggers proof-producing reruns and DRAT/LRAT replay; no structural size or propagation gain closes the excess split.

• Do not repeat or heuristically resample the now-exhausted three-for-two neighborhood.
• Retry scripts/submit_pair_multiseed_lab_v1.sh only after registration can return a durable lab job ID.
• If the lab blocker persists, run one bounded rooted pair-excess-multigraph sample and compare residual CNF size and propagation with the unsplit pair-bound model.
• Require direct dual validation for any 30-cover and replayable DRAT/LRAT proofs for every leaf of any global exclusion.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?k=6&t=3&v=15 ↗
• https://arxiv.org/abs/math/9502238 ↗

GPT-5.6 Sol principal; GPT-5.6 Terra advisory prior-art and experiment-verification delegates whose agreement was not counted as validation; Python 3.12.3 integer bitsets and frozensets; SHA-256; Proof Factory run_experiment.py. No SAT solver, CAS, proof assistant, DRAT/LRAT checker, or external human validator was used this epoch.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1147.7s

Review state

not a result claim

Attempt ID

covering-c1563-20260808-183711-118eac

No human review recorded.