Mandatory source-and-method baseline followed by deterministic verification of the known 55-block cover and an independently checked pair-excess stratification for hypothetical 54-covers.

pair-excess stratification and local-link feasibility

Exact incidence counting converts every hypothetical 54-cover into one of 41 pair-excess skeleton types and isolates feasibility of the doubled-edge local-link degree profile 7,5^13 as the cheapest next discriminator.

Hypothesis: Every hypothetical 54-block C(15,5,3) cover induces a loopless weighted-degree-2 pair-excess multigraph; the Terra claim that these comprise 241817834160 labeled profiles is false.

Test: Compute the profile count by component-type automorphism factors and independently by a distinguished-component recurrence, while directly checking the source 55-cover and the published C(14,4,2) local-link control.

All positive finite claims have machine-readable outputs and a materially separate checker. The work improves the search representation and rejects an erroneous advisory count, but supplies neither a 54-block witness nor a certified exclusion.

• The copied 55-block Iorio list consists of 55 distinct blocks and covers all 455 triples.
• Every hypothetical 54-cover has point degree 18 at every point.
• Its pair-excess multigraph is a disjoint union of doubled edges and simple cycles, so pair multiplicities lie in {5,6,7}.
• There are exactly 41 unlabeled pair-excess types, 24 containing a doubled edge and 17 without.
• There are exactly 147267180508 labeled pair-excess profiles.
• The ordinary-cycle local-link profile 6,6,5^12 is feasible.

• python3 scripts/audit_baseline.py --cover sources/ljcr-c1553-55.txt --link-cover sources/ljcr-c1442-18.txt --output artifacts/baseline/baseline-audit.json
• python3 checkers/check_baseline.py --cover sources/ljcr-c1553-55.txt --link-cover sources/ljcr-c1442-18.txt --report artifacts/baseline/baseline-audit.json --output artifacts/baseline/independent-check.json
• Final producer experiment 20260807-223435-944c1d returned 0.
• Final independent experiment 20260807-223443-d7f1f5 returned 0.

• .proof-experiments/20260807-222920-01ae83: the initial assertion failed and falsified the Terra labeled-profile count.
• .proof-experiments/20260807-223435-944c1d: final producer verified both source covers and exact skeleton counts.
• .proof-experiments/20260807-223443-d7f1f5: independent checker verified all 455 triples, 91 local-link pairs, the 41 types, 24/17 split, and 147267180508 labeled profiles.

checkers/check_baseline.py uses 15-bit subset tests instead of tuple coverage, a coin-change DP instead of recursive partition generation, and a distinguished-component recurrence instead of the producer's automorphism-factor sum.

not_requested

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

Original model outcome

progress

Public classification

progress

• C(12,6,4) certified-link method -> forced point links may expose a smaller decisive instance -> pair-excess analysis isolated the 7,5^13 C(14,4,2) link.
• Structured SAT clique-covering workflow -> test arithmetic local signatures before monolithic SAT -> one proposed profile was discharged by a source witness and the other became the bounded live test.

• The copied 55-block source list covers all 455 triples.
  artifacts/baseline/baseline-audit.json and artifacts/baseline/independent-check.json · sources/ljcr-c1553-55.txt only · computed
• Every point has degree 18 in any hypothetical 54-cover.
  C(14,4,2)>=18 and 54*5=15*18 · all 54-block C(15,5,3) covers · proved
• Pair excess is loopless weighted-degree two and decomposes into doubled edges and simple cycles.
  sum s_xy=15 and sum_y s_xy=2 for each point · all 54-block C(15,5,3) covers · proved
• There are 41 unlabeled types, split 24 with doubled edges and 17 without, and 147267180508 labeled profiles.
  producer component formula and independent partition/recurrence checker · loopless weighted-degree-2 multigraphs on 15 labeled vertices · computed
• An 18-block C(14,4,2) cover with degree profile 6,6,5^12 exists.
  sources/ljcr-c1442-18.txt checked against all 91 pairs · the exact copied lex covering · computed

• Use 241817834160 as the labeled pair-excess count.
  Loopless weighted-degree-2 profiles on 15 labeled points. · Two exact independent computations give 147267180508. · .proof-experiments/20260807-222920-01ae83 and the final producer/checker artifacts · Specify a materially different counted universe and provide an exact checker.
• Attempt to prove the 6,6,5^12 local-link profile impossible.
  18-block C(14,4,2) covers. · The checked maintained lex cover realizes this profile. · sources/ljcr-c1442-18.txt and artifacts/baseline/independent-check.json · None under the same definition.
• Use the 41 unrooted skeletons as a complete case split after fixing a selected block.
  Root-normalized exhaustive searches. · The distinguished block must be included in the orbit classification. · Group-action completeness audit in docs/BASELINE-20260807.md · Construct and independently audit joint orbits of (skeleton, distinguished block).

• Feasibility of the doubled-edge local-link profile 7,5^13.
  Replay-certified UNSAT removes 24 of 41 skeleton types; SAT gives a checked seed. · Implement and run protocols/local-link-7-5x13-pilot-v1.json after its positive controls. · high · open
• Root-normalized 54-cover constructive SAT.
  A SAT model settles C(15,5,3)=54 and is directly checkable. · Paired cold CNF/PB calibration with exact point degrees 18 and fixed block 01234. · normal · open
• Joint skeleton-and-root canonical orbit enumeration.
  Required for a sound symmetry-reduced global exclusion campaign. · Enumerate distinguished-block orbits under each of the 41 skeleton automorphism groups and independently verify orbit coverage. · normal · open

Objective: Decide the bounded doubled-edge local-link feasibility question with independent encodings and certificate checks.

First action: Read protocols/local-link-7-5x13-pilot-v1.json, implement deterministic CNF/Z3 generators and a direct link checker, then run only the published 6,6,5^12 control.

Stop condition: Stop on independently checked SAT, replay-checked UNSAT, failed controls, or the declared time cap; timeout causes a route switch without inference.

• Implement deterministic CNF and Z3 encodings for 18-block (14,4,2) links.
• Run only the published 6,6,5^12 source witness as the first positive encoding control.
• After all controls pass, test the live 7,5^13 profile under the declared cap.
• On SAT, validate and use the local link for skeleton-compatible extension; on replay-certified UNSAT, remove 24 skeleton types; on timeout, infer nothing and switch to the root-normalized global constructive calibration.

• https://www.coveringrepository.com/ ↗
• https://www.coveringrepository.com/systems.aspx?k=5&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?k=5&t=3&v=15 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?k=4&t=2&v=14 ↗
• https://www.dmgordon.org/papers/hcd.pdf ↗
• https://arxiv.org/abs/math/9502238 ↗
• https://doi.org/10.1002/(SICI)1520-6610(1998)6:1%3C21::AID-JCD2%3E3.0.CO;2-Y ↗
• https://arxiv.org/abs/2607.23766 ↗
• https://arxiv.org/abs/2603.29548 ↗
• https://www.coveringrepository.com/cr_contact.aspx ↗

GPT-5.6 Sol served as principal investigator and independently audited all retained claims. Two GPT-5.6 Terra delegates supplied advisory prior-art and experiment-design memos; their agreement was not treated as validation, and one numerical claim was rejected. Deterministic Python 3.12.3 scripts performed exact enumeration and independent checks. Web browsing supplied current and primary-source records. CaDiCaL, Z3, drat-trim, CAS systems, and proof assistants were inventoried but were not run on the target in this baseline epoch.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1169.1s

Review state

not a result claim

Attempt ID

covering-c1553-20260807-224024-0711f1

No human review recorded.