Derived the forced excess-triple marginal system over a complete weighted pair-surplus graph and tested exact bounded integer realizability on two canonical controls plus 48 deterministic labelled samples.

pair-surplus to bounded triangle-decomposition relaxation

Double count triple multiplicities around every pair, then solve and independently check the resulting 455-variable bounded integer triangle-decomposition system.

Hypothesis: The two canonical controls and 48 deterministic sampled weighted 4-regular surplus graphs all pass the forced excess-triple integer-realizability condition.

Test: Solve 105 exact pair-marginal equations with 455 bounded integer triple variables for each frozen H, then validate every returned vector using a solver-independent exact checker.

The lemma is exact and global, while the computation is deliberately limited to 50 stored labelled graphs. Direct witness checking makes every positive feasibility result independently verifiable, but feasibility is only necessary and supplies no cover. All controls passing makes another arbitrary sample low-value.

• In every hypothetical 30-block C(15,6,3) cover, e_xyz=mu_xyz-1 satisfies sum_z e_xyz=3+4h_xy and e_xyz<=3+min(h_xy,h_xz,h_yz), where h_xy=lambda_xy-4.
• The named labelled surplus graphs 3K5 and 2C15 and the 48 stored deterministic seed-0 labelled samples each admit an exact vector satisfying those equations and caps.
• No tested surplus graph was excluded and the maintained covering range is unchanged.

• Producer command under the experiment harness returned PASS_ALL_FEASIBLE for 50 cases in 23.667 seconds.
• Independent checker command returned PASS_INDEPENDENT for 50 cases in 0.124 seconds and rejected three mutations.
• Fresh producer rerun completed in 22.761 seconds; cmp returned 0 and both receipts have SHA-256 9ac620d5a6a1137125916ed398cdc0ec128ae6e90c6755ce9f5a78611de09fdd.
• Exact scope: two named labelled controls plus 48 deterministic labelled samples; no quotient or global graph fraction.

• .proof-experiments/20260812-092451-b9dc72: 50/50 exact feasible vectors, 23.667 seconds, 117788 KiB peak child memory.
• .proof-experiments/20260812-092524-2a71fa: independent exact check PASS, three mutations rejected, 0.124 seconds.
• .proof-experiments/20260812-092531-a165d6: fresh producer rerun, byte-identical receipt, 22.761 seconds.

checkers/check_triple_excess_realizability_v1.py does not import SciPy or invoke a solver; it independently regenerates every H and checks the sparse e vectors by exact integer marginal accumulation, caps, totals, digests, and three mutations.

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

• Multigraph triangle decomposition -> predict pair-multiplicity marginals can cheaply reject some complete surplus H -> both canonical controls and all 48 deterministic samples instead admitted exact bounded decompositions.

• Every putative 30-cover induces the capped triple-excess marginal system over its weighted 4-regular pair-surplus H.
  Direct double count and multiplicity bound in artifacts/epoch114-20260812/technical-report.md. · All hypothetical 30-block C(15,6,3) covers. · proved
• All 50 stored labelled H admit exact feasible capped triple-excess vectors.
  Producer receipt and solver-independent PASS_INDEPENDENT checker; byte-identical rerun. · The exact two controls and 48 deterministic seed-0 samples stored in the producer receipt. · computed

• Use unstructured random sampling of the triple-excess marginal relaxation as the next bulk pair-surplus elimination route.
  The two canonical controls and 48 deterministic labelled samples, with an exploratory pilot also finding the first 60 samples feasible but not claimed as evidence. · Every frozen case passes; passing samples do not establish redundancy and another arbitrary cutoff has low information value. · artifacts/epoch114-20260812/triple-excess-realizability-v1/producer-receipt.json and independent-check.json · A complete owned H requires screening, or a materially stronger block-incidence coupling is derived and fails a canonical control.
• Treat feasible triple-excess marginals as evidence that a cover exists.
  All H. · The relaxation forgets the requirement that all multiplicities arise from one family of 30 six-subsets. · One-sided derivation in the technical report and explicit non-claim in the producer receipt. · An exact lifting theorem from every feasible e to 30 six-subsets, independently proved and checked.

• Apply triple-excess feasibility as a prefilter on complete owned surplus graphs.
  Infeasibility would safely remove a whole H before cover SAT, while feasibility is cheap to check. · After full-ledger approval and complete-H ownership, run one smallest owned complete H through the checker and certify any infeasibility exactly. · normal · open
• Couple excess-triple marginals to global block-intersection moments.
  The observed failure signature is loss of common six-block incidence; intersection moments restore part of that information without a full incidence CNF. · Derive the exact first three intersection moments and test the strengthened integer system on 3K5 and 2C15 under a 30-second cap. · normal · open

Objective: Secure exact-scope approval and finish the parent-rich depth-four union before extending to complete H or solver leaves.

First action: Present the remaining 38705-profile scope from epoch 113, including oversized-orbit qualifications, for human approval.

Stop condition: Hold on refusal or missing approval; after approval, stop on any count, ownership, hash, restart, or checker mismatch.

• Obtain human approval for the exact remaining 38705-profile parent-rich ledger scope from epoch 113.
• After a complete 62437-profile union independently validates, extend ownership to complete H and run the triple-excess checker only as a cheap prefilter.
• If a future complete H fails the integer system, generate a replayable SAT/PB infeasibility certificate before claiming a local exclusion.
• Keep native PB held until pinned RoundingSat, VeriPB, and CakePB pass the transparent calibration.

• 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 ↗
• https://arxiv.org/abs/2607.23766 ↗
• https://veripb.org/ ↗

GPT-5.6 Sol was principal investigator. Two GPT-5.6 Terra delegates supplied advisory route-triage memos; Sol independently audited their relevant claims and did not treat agreement as evidence. Deterministic work used Python 3.12.3, NumPy 1.26.4, SciPy 1.11.4 with HiGHS MILP, an independently written exact Python checker, SHA-256, cmp, and the computational-researcher experiment harness. CaDiCaL, RoundingSat, VeriPB, CakePB, CAS, proof assistants, cloud lab, and external proof services were not used for the result.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1280.5s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260812-093359-2df264

No human review recorded.