Exact pre-solve size and equivalence audit of the proposed joint local-moment/triple-excess shared-support model for fixed H=3K5.

joint local block-admissibility and triple-excess support

Count the natural disjunctive formulation exactly and use tight triple-incidence arithmetic to decide whether its 30-support threshold separates from direct cover search.

Hypothesis: For fixed H=3K5, the natural joint local-admissibility model is materially smaller than direct 5005-block selector search and its decisive 30-support threshold is not equivalent to the target.

Test: Enumerate the local value selectors, count all variables/rows/nonzeros, and independently test whether the forced total triple excess makes 30 shared supports exactly a 30-cover.

The predeclared success condition required real compression and logical separation from the target. Exact counts show expansion, while 20|Y| >= 455+145 makes equality at 30 equivalent to a cover. This decisively rejects scale-up of this formulation but supplies no covering optimum.

• For every excess vector satisfying the exact pair marginals of a putative 30-cover, sum_T e_T=145.
• Any shared family of 6-blocks covering each triple at least 1+e_T times has at least 30 blocks; at exactly 30 it is a genuine 30-cover.
• For fixed H=3K5, the natural joint local-value formulation has exactly 43260 variables, 15575 rows, and 430535 matrix nonzeros.
• The natural joint formulation is larger than direct selector search and is not a justified scale-up route; the maintained covering range is unchanged.

• Producer experiment 20260812-130312-f291f0 returned PASS_TARGET_EQUIVALENCE_GATE in 1.235 s.
• Independent experiment 20260812-130321-fbf820 returned PASS_INDEPENDENT_DP_AND_DIMENSION_AUDIT in 1.936 s and rejected four mutations.
• Fresh producer experiment 20260812-130336-6f7f5c produced a byte-identical receipt with SHA-256 1a6fdeefe8ff8a01c65ced127e5a39eca2a25b4747dfca0e511daf162acb6044.
• No SAT, MILP, or PB solve was run because the exact predeclared compression/target-separation gate failed.

• .proof-experiments/20260812-130312-f291f0: exact producer, 43260 variables, 15575 rows, 430535 nonzeros, REDIRECT_NO_SOLVE.
• .proof-experiments/20260812-130321-fbf820: independent DP/dimension reconstruction and four rejected mutations.
• .proof-experiments/20260812-130336-6f7f5c: byte-identical producer rerun.

checkers/check_joint_local_support_model_audit_v1.py uses a 29-step DP instead of six-bin enumeration, independently reconstructs all blocks and coefficient counts, verifies exact incidence tightness, and rejects false status, z-count, nonzero-count, and sum-e 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

• Extended-formulation design -> predict that local disjunctions compress global support -> exact dimensioning found an 8.643x variable expansion.
• Capacity-tight set-cover relaxations -> predict threshold equality can collapse inequalities -> 600 required incidences equal the full capacity of 30 six-blocks, making every triple row tight.

• The exact excess total is 145 under the pair-marginal equations.
  Independent exact arithmetic: (3*105+4*30)/3=145. · All putative 30-block C(15,6,3) covers. · proved
• Thirty shared support blocks satisfying all 1+e_T lower bounds form a genuine 30-cover with every row tight.
  20*30=455+145=600 and all individual slacks are nonnegative integers. · Any e with total 145 and any set of distinct 6-subsets used as shared supports. · proved
• The H=3K5 natural joint formulation has 43260 variables, 15575 rows, and 430535 nonzeros.
  Producer receipt and independent DP/set-loop reconstruction. · The explicitly specified natural disjunctive model only. · computed

• Scale the natural shared-support joint local-admissibility model for H=3K5.
  The formulation with e_T, y_B for all 5005 blocks, and z_(B,E) for every reachable local value. · It is larger than direct selector search and its decisive 30-support threshold is target-equivalent. · Exact dimension receipt, tightness lemma, independent checker, and byte-identical rerun. · A proved quotient/decomposition that removes the global y_B layer or reduces the verification surface below the direct baseline while preserving exact coverage.

• Aut(H)-quotiented excess-vector model without global block supports.
  It may quantify over e while avoiding the 5005-block selector layer that caused the current collapse. · For H=3K5, derive Aut(H), enumerate triple orbits, and dimension the exact orbit-marginal system; stop unless an independent orbit owner proves coverage and a substantial reduction. · normal · open
• Exact published native-PB proof tuple qualification.
  Native equalities may produce smaller independently replayable certificates than CNF, but only a compatible source-pinned stack makes this executable. · Acquire independently verified full-revision RoundingSat, VeriPB, and CakePB snapshots, build project-scoped, and dual-replay the retained transparent contradiction with mutations. · normal · open
• Materially decomposed constructive witness search.
  A directly checked 30-cover remains the shortest terminal certificate. · Propose and preflight one new symmetry/decomposition mechanism with measured reduction against the frozen selector/incidence baselines before any solve. · normal · open

Objective: Select a route with a genuinely smaller verification surface than direct selector search.

First action: Dimension the H=3K5 Aut(H) triple-orbit marginal system and independently prove orbit ownership before adding any block variables or solver calls.

Stop condition: Redirect if the quotient is incomplete, if lifting reintroduces all 5005 block selectors, or if the model does not materially improve a frozen baseline.

• Do not instantiate or solve the natural shared-support joint model.
• Dimension an Aut(H)-orbit model for e that has no global 5005-block support variables; require a proved owner map and independent quotient coverage before execution.
• Alternatively provision the exact CP 2025 RoundingSat/VeriPB/CakePB tuple only from independently verified full-revision source snapshots, then replay the retained calibration before target contact.
• Preserve constructive witness search as a symmetric alternative, but reopen only with a material decomposition or measured improvement over the frozen direct baseline.

• 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://drops.dagstuhl.de/storage/00lipics/lipics-vol340-cp2025/LIPIcs.CP.2025.21/LIPIcs.CP.2025.21.pdf ↗
• https://veripb.org/ ↗

GPT-5.6 Sol principal investigator. Two GPT-5.6 Terra delegates supplied advisory prior-art and verification memos; Sol independently audited the executable blocker, rejected unverified source-pin claims as evidence, selected a different live discriminator, and did not count model agreement as validation. Deterministic work used CPython 3.12.3 standard-library exact integer/set arithmetic, dynamic programming, SHA-256, cmp, and the computational-researcher experiment harness. Web access was attempted but returned no source text; pre-acquired primary-source audits supplied status context. CaDiCaL 1.7.3 was detected but unused. No SAT, MILP, PB solver, CAS, proof assistant, cloud lab, external proof service, human validator, or publication action was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1004.6s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260812-130958-c53e9a

No human review recorded.