Used exact fixed-block incidence double counting to eliminate minimum-intersection branches r=3,4,5, then built and independently reconstructed the complete normalized r=2 incidence CNF and ran one bounded proof-producing root test.

proof-producing incidence/PB cube decomposition

Exact degree equations restrict the fixed-block intersection frontier; a hash-bound incidence CNF tests the surviving r=2 family, with LRAT output and two independent replayers.

Hypothesis: The complete normalized minimum-intersection r=2 branch returns either a directly checkable 30-block cover or a replayable LRAT proof within 60 solver-seconds and 64 MiB of proof output.

Test: Run pinned CaDiCaL 1.7.3 on the independently reconstructed 33162-variable, 156560-clause r=2 root, accepting only a directly checked witness or UNSAT accepted by both lrat-check and CakeLPR.

The branch elimination follows directly from exact degree 12 and a double count and is independently executable. The root solver observation is independently hash- and log-checked, while both proof checkers reject the incomplete prefix, preventing any false UNSAT promotion.

• In any hypothetical simple 30-block C(15,6,3) cover, after fixing a block F, some other block meets F in at most two points.
• If the minimum fixed-block intersection is two, the 29 remaining blocks have total excess eight and exactly ten possible intersection-count profiles.
• The hash-bound complete normalized r=2 CNF has 33162 variables and 156560 clauses and returned UNKNOWN under the recorded 60-second CaDiCaL 1.7.3 protocol.

• Exact proof: sum over p in F of d(p)=6*12=72, but r>=3 forces 6+29r>=93.
• python3 checkers/check_min_intersection_incidence_lemma_v1.py --receipt artifacts/epoch35-20260809/minimum-intersection-incidence-lemma-receipt.json
• python3 checkers/check_r2_min_branch_semantics_v1.py --artifact-dir artifacts/epoch35-20260809/r2-min-branch-v1 --receipt artifacts/epoch35-20260809/r2-min-branch-v1/semantic-check.json
• python3 scripts/solve_r2_min_branch_lrat_v1.py --artifact-dir artifacts/epoch35-20260809/r2-min-branch-v1
• python3 checkers/check_r2_min_branch_result_v1.py --artifact-dir artifacts/epoch35-20260809/r2-min-branch-v1 --receipt artifacts/epoch35-20260809/r2-min-branch-v1/result-recheck.json
• sha256sum -c artifacts/epoch35-20260809/SHA256SUMS passed

• .proof-experiments/20260809-224627-dcc9da: built the canonical 33162-variable, 156560-clause r=2 CNF
• .proof-experiments/20260809-224702-3019ce: clean-room clause reconstruction and semantic controls PASS
• .proof-experiments/20260809-224715-9c27f2: complete r=2 root returned UNKNOWN after 60.02 real seconds
• .proof-experiments/20260809-225047-d50ed0: independent UNKNOWN reparse and two partial-proof rejections PASS
• .proof-experiments/20260809-225226-156205: incidence lemma, r>=3 elimination, and ten-profile enumeration PASS

The incidence lemma has a separate exact tuple enumerator; the CNF checker independently regenerates every clause without importing the delta emitter; the result checker reparses raw logs and freshly compiles lrat-check and CakeLPR.

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

• C(12,6,4) dual-replayer certificate pipeline -> predict that proof-producing incidence roots can be made fail-closed for C(15,6,3) -> the pipeline worked, but the complete r=2 root remained UNKNOWN and therefore triggered profile cubing.

• Minimum fixed-block intersection is at most two.
  Exact double count and minimum-intersection-incidence-lemma-receipt.json · All hypothetical simple 30-block C(15,6,3) covers · proved
• The r=2 intersection-count frontier consists of exactly ten profiles with total excess eight.
  Exact integer enumeration; duplicate-F control changes the count from ten to fifteen · Simple normalized r=2 families · computed
• The complete normalized r=2 CNF is structurally and semantically reconstructed.
  semantic-check.json PASS over all 156560 clauses and 1792 ban truth-table cases · CNF SHA-256 08e4e52f73899acca41ab707eeabd20b7fbd775cd9486466e91a06facc846300 · computed
• The bounded root run is UNKNOWN and its retained LRAT prefix is incomplete.
  result-recheck.json; both lrat-check and CakeLPR rejected the prefix · CaDiCaL 1.7.3, seed 0, recorded options, 60-second limit · computed

• Minimum-intersection branches r=3, r=4, and r=5
  All hypothetical simple 30-block covers after fixing any block F · They require at least 6+29r fixed-block incidences, exceeding the exact total 72. · minimum-intersection-incidence-lemma-receipt.json · A defect in the established degree-12 lemma or fixed-block double count
• Increase the timeout of the unchanged monolithic r=2 root
  The recorded seed-0 CaDiCaL 1.7.3 formula and options · The predeclared 60-second discriminator returned UNKNOWN; profile cubing has higher next information value. · result-recheck.json · A material encoding change, proof-prefix reuse design, or profile-cube measurements that change the projected value
• Treat the 18.9 MB LRAT prefix as an UNSAT certificate
  The epoch-35 r=2 root · No empty clause was derived and both independent replayers rejected it. · result-recheck.json · A complete proof deriving the empty clause and accepted by both replayers

• Ten-profile r=2 cube frontier
  It is an exact disjoint compression of the unresolved branch and directly addresses the monolithic UNKNOWN. · Emit all ten profile assumptions and independently prove exactly-one coverage before solving one smallest leaf. · high · open
• Fixed-C5 constructive one-orbit tail lookup
  A witness settles the problem immediately and supplies information independent of the exclusion route. · Run the saved matched one-orbit-tail pilot and directly validate any 30-block cover. · normal · open
• r=0 and r=1 proof-oriented branches
  These remain necessary for a global negative result even if r=2 is eventually excluded. · Defer scaling until the r=2 profile-cube calibration measures proof growth and reusable prefix behavior. · normal · open

Objective: Turn the exact ten-profile r=2 restriction into a complete independently checked proof frontier and calibrate one smallest leaf.

First action: Enumerate the ten tuples (n2,n3,n4,n5), emit their assumption constraints, and run a separate gap/overlap checker before invoking a solver.

Stop condition: Stop or redirect on frontier overlap/gap, semantic or hash mismatch, proof projection above budget, replay failure, or a directly verified witness.

• Generate the ten r=2 profile constraints as an exactly-one, gap-free frontier.
• Write a separate checker that reconstructs profile coverage and rejects omitted, overlapping, or altered profiles.
• Run one smallest assumption-literal profile leaf with the same 60-second and 64 MiB proof limits.
• Replay any UNSAT leaf with both lrat-check and CakeLPR; directly validate any SAT witness against all 455 triples.
• Retain r=0, r=1, and constructive witness routes.

• 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://www.dmgordon.org/papers/cover.pdf ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol served as principal investigator. GPT-5.6 Terra delegates supplied advisory challenger and verification memos; Sol re-derived and deterministically checked every relied-on claim, and model agreement was not validation. Deterministic tools were Python 3.12.3, CaDiCaL 1.7.3, GCC, SHA-256, lrat-check.c, CakeLPR, exact integer enumeration, and the computational-researcher experiment harness. No CAS, proof assistant, external lab job, or untracked background process was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1424.8s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260809-230018-5dc524

No human review recorded.