Proved and independently audited that the residual missed-triple capacity predicate is implied by completed root-link pair coverage.

residual missed-triple capacity

Map every pair corresponding to a missed triple through y into a pair-covering root-link block avoiding y, then apply a ten-pairs-per-5-block union bound.

Hypothesis: Some completed 12-block pair-cover root link satisfies U_y > 10(12-r_y), making the proposed capacity predicate nonredundant.

Test: Search for the underlying per-pair logical counterexample and independently test the negated implication with SMT.

Every pair {z,w} whose triple with y is missed must still be covered by the root link. Any block covering that pair must avoid y. Thus all such pairs lie in the union of the pairs from the 12-r_y blocks avoiding y, each contributing at most ten pairs.

• For every twelve-block 5-uniform pair-cover link and every point y, U_y<=10(12-r_y).
• The proposed predicate cannot prune completed pair-cover links beyond the base pair-cover constraint.
• The exact covering-number range remains 30<=C(15,6,3)<=31.

• python3 scripts/audit_missed_triple_capacity_v1.py --receipt artifacts/epoch11-20260808/missed_triple_capacity_receipt.json
• The auditor checked 16,777,216 assignments and 527,345 premise cases with zero counterexamples.
• python3 checkers/check_missed_triple_capacity_v1.py artifacts/epoch11-20260808/missed_triple_capacity_receipt.json --receipt artifacts/epoch11-20260808/missed_triple_capacity_check.json
• The independent checker returned SMT UNSAT and rejected five corruptions.
• A byte-for-byte deterministic generator rerun and final hash-manifest verification passed.

• .proof-experiments/20260808-222625-179045: audited all 2^24 Boolean assignments in 2.34 seconds; zero counterexamples.
• .proof-experiments/20260808-222627-0d9bf7: independent Z3 check returned UNSAT and rejected five corruptions.
• .proof-experiments/20260808-222205-5dc883: unsymmetrized degree-8 selector run returned UNKNOWN after 30 seconds.
• .proof-experiments/20260808-222317-f7ec34: symmetry-fixed degree-8 selector run returned UNKNOWN after 45 seconds.

checkers/check_missed_triple_capacity_v1.py uses a materially different Z3 encoding of the negated implication, recomputes all degree rows, and rejects five receipt corruptions.

not_requested

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

Original model outcome

progress

Public classification

progress

• Certified link-orbit SAT for C(12,6,4) -> audit local constraints before catalogue generation -> the proposed C(15,6,3) predicate was sound but redundant.

• Every completed twelve-block 5-uniform pair-cover link satisfies U_y<=10(12-r_y).
  Human set-inclusion proof, exhaustive 2^24 audit, and independent SMT UNSAT check. · All fourteen-point pair-cover links and all five forced degree types. · proved
• The Boolean audit covered exactly 16,777,216 assignments and 527,345 premise cases.
  Hash-bound receipt and independent count reconstruction. · The 24-variable abstraction for twelve block-membership positions. · computed

• Use U_y<=10(12-r_y) as additional pruning after full root-link pair coverage.
  Every completed twelve-block pair-cover link and all five forced degree types. · The predicate is the union bound over pair-covering blocks avoiding y. · artifacts/epoch11-20260808/missed_triple_capacity_redundancy_lemma.md and independently checked receipt · A partial-state implementation that measurably prunes beyond an independently checked remaining-pair-support feasibility test.

• Canonical excess-multigraph two-row prefix audit
  It partitions forced global pair-multiplicity profiles and has a cheap exact 2380-to-5-to-12 reconstruction test. · Generate a hash-bound two-row frontier and independently reconstruct every labelled state. · high · open
• Degree-preserving constructive local search
  A verified 30-block witness would settle the target directly. · Run matched deterministic degree-preserving and unconstrained searches under identical evaluation budgets. · normal · open
• Unfiltered canonical root-link calibration
  It measures catalogue growth without relying on either redundant predicate. · Run only after the excess-prefix audit, under a small fixed canonical-node cap with independent frontier replay. · low · open

Objective: Validate or kill the proposed two-row canonical prefix partition of the forced 4-regular pair-excess multigraph.

First action: Implement a deterministic generator for the five root partitions and twelve second-row branches, then independently reconstruct all 2,380 labelled root rows and their labelled second-row extensions.

Stop condition: Stop or redirect if branch coverage is not exact and disjoint, reconstruction fails, or the predeclared canonical-prefix cap is exceeded.

• Generate the five first-row partitions of a loopless 4-regular excess multigraph and the claimed twelve two-row branch types.
• Write an independent labelled-state reconstructor proving exact and disjoint branch coverage before canonical scale-up.
• Retain degree-preserving constructive search as the direct witness route.
• Keep the six incidence branches held until a material encoding or proof-prefix change exists.

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

GPT-5.6 Sol served as principal investigator. GPT-5.6 Terra delegates supplied advisory prior-art and verification memos; Sol independently derived the proof, and model agreement was not validation. Deterministic tools: Python 3.12.3, Z3 4.13.0, SHA-256, the computational-researcher experiment harness, and CaDiCaL 1.7.3 for two explicitly non-evidentiary UNKNOWN controls. No proof assistant or DRAT/LRAT checker was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1000.0s

Review state

not a result claim

Attempt ID

covering-c1563-20260808-223144-2b4c5d

No human review recorded.