Exhaustively project any putative 30-cover onto the intersection-size histogram of one point subset S, eliminate the four triple-type totals through the third binomial moment, and test whether this restricts the internal pair-surplus mass H(S).

one-subset intersection-histogram projection

Quotient 30 blocks by their intersection size with S and enumerate exact moment-compatible histograms instead of selecting among 5005 blocks.

Hypothesis: At least one subset size s and pair-surplus mass H(S) compatible with loopless weighted degree-4 cut arithmetic is excluded by exact one-subset block-intersection moments and all four triple-type covering inequalities.

Test: Enumerate all integer intersection histograms for s=0,...,15 and compare their accepted H(S) values with the 124 degree/cut-compatible integer pairs; independently replay with a third-moment bitset DP.

A single excluded compatible pair would have been a new H-only structural constraint. Zero exclusions under two materially different enumerations falsifies that discriminator at its complete stated scope, but separate subset histograms do not constitute a jointly realizable graph or cover.

• Every hypothetical 30-block cover induces, for every S, the stated exact intersection-histogram moments and four triple-type covering inequalities.
• For all subset sizes 0 through 15, every one of the 124 H(S) values allowed by elementary loopless weighted degree-4 cut arithmetic has an abstract histogram satisfying those one-subset constraints.
• No complete pair-surplus graph, 30-block cover, or covering-number bound is obtained.

• Producer command in experiment 20260812-180218-e42d0a returned PASS_NO_H_ONLY_PRUNING with 124 compatible pairs and 0 excluded.
• Independent experiment 20260812-180322-88fdfa returned PASS_INDEPENDENT_BITSET_DP with 32768 control subsets and five rejected mutations.
• Producer rerun experiment 20260812-180545-9b43bc reproduced the corrected receipt byte-for-byte.

• .proof-experiments/20260812-180218-e42d0a: corrected producer, 124 compatible and 0 excluded in 4.984 seconds
• .proof-experiments/20260812-180322-88fdfa: independent bitset DP and 32768-subset control passed in 118.837 seconds
• .proof-experiments/20260812-180545-9b43bc: producer rerun byte-identical in 3.735 seconds

checkers/check_subset_intersection_profile_v1.py uses an unbounded-type third-moment bitset DP rather than the producer's recursive histogram enumeration; it also checks a separate exact-degree family and five 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

• Classical design intersection equations -> predict that subset triple-type moments might constrain pair-surplus cuts -> exact test found no restriction on any of 124 aggregate H(S) values.

• The one-subset moment lemma and affine third-moment formulas hold for every hypothetical simple 30-block cover.
  Direct incidence proof in subset-intersection-lemma.md plus exact identity checks on all 32768 subsets of a separate exact-degree family. · All point subsets of every hypothetical simple 30-block C(15,6,3) cover. · proved
• All 124 elementary degree/cut-compatible (s,H(S)) pairs admit an abstract one-subset histogram satisfying the lemma.
  Corrected producer receipt, byte-identical rerun, and independent bitset-DP receipt. · Separate aggregate histograms for subset sizes 0 through 15; no joint consistency. · computed

• Use one-subset block-intersection moments and four triple-type cover inequalities to prune the pair-surplus graph through H(S) alone.
  Every subset size s=0,...,15 and all 124 H(S) values allowed by elementary loopless weighted degree-4 cut arithmetic. · Every compatible pair has an explicit abstract histogram, independently replayed. · Result receipt SHA-256 3d6d1f84caa2d3803ab549fa8bd7342b088797b8f6703f492aa6204783bdf214 and independent receipt SHA-256 51bcaa4e9734545e1bf555ae0cf6011292abf15ad5efee545ccb175e3cd0fff1. · A joint multi-subset, edge-resolved, or block-owned constraint that is not implied by separate H(S) histograms and excludes a complete H/profile.

• Two-subset/Venn-cell joint intersection histogram.
  It retains cross-subset consistency absent from the exhausted one-subset projection while still offering a count-only preflight before block selectors. · For one frozen complete H, enumerate joint block cell-intersection types for a small nested or overlapping subset pair and compare exact variable/nonzero counts and exclusions against the direct 5005-selector baseline. · normal · open
• Complete depth-four pair-surplus parent ownership union.
  The remaining scope is exact and already chunk-qualified, but execution is authority-blocked. · After explicit human approval, parent-materialize the remaining 38705 profiles and independently reconcile exactly 62437 records before any SAT leaf. · high · open

Objective: Test whether a joint two-subset projection adds complete-profile pruning without recreating the full block-selector problem.

First action: Write a count-only dimension and feasibility preflight for one frozen H using Venn-cell block types; compare against 5005 variables and 100100 incidence nonzeros before any solver run.

Stop condition: Redirect if the formulation is target-equivalent, has at least 5005 selectors or 100100 nonzeros without a proved quotient, or excludes no complete H/profile control.

• Keep the exact remaining 38705-profile parent-rich ownership union blocked until explicit human approval of that scope.
• Preflight a two-subset/Venn-cell joint histogram on one frozen complete H; require a representation smaller than the 5005-selector baseline and exclusion of a complete profile before scaling.
• Do not rerun the stale type-2 DRAT-to-LRAT control or the epoch-19 root-link catalogue without their recorded reopen conditions.

• 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://doi.org/10.1016/j.jcta.2010.03.005 ↗
• https://arxiv.org/abs/1405.6110 ↗

GPT-5.6 Sol principal investigator; GPT-5.6 Terra delegates supplied advisory memos only and were not validators. CPython 3.12.3 exact integer arithmetic and bitsets, JSON, SHA-256, cmp, and the computational-researcher experiment harness were used. No SAT/PB solver, CAS, proof assistant, cloud lab, external proof service, system installation, or human validator produced evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1651.4s

Review state

not a result claim

Attempt ID

covering-c1563-20260812-181543-71b10b

No human review recorded.