Derived and tested a globally complete root-block CNF replacing exact point-degree totalizers with theorem-equivalent forward-only degree caps.

proof-preserving global root-block link-cap CNF

Triple coverage proves every point degree is at least 18, so encoding only degree at most 18 preserves the exact search while deleting reverse cardinality implications.

Hypothesis: Replacing fifteen exact-degree totalizers with theorem-equivalent forward-only degree caps reduces CaDiCaL decisions by at least 20 percent at a matched 5000-conflict cap without enlarging the formula.

Test: Independently reconstruct the candidate CNF, replay a full-formula DRAT-to-LRAT smoke proof, then compare baseline and candidate at seeds 0 and 1 under identical 5000-conflict limits.

The arithmetic equivalence is exact, the separate checker reproduced every clause, counter boundary tests passed, the proof stack was positively and negatively controlled, and an independent parser reproduced the telemetry. Since no live SAT or UNSAT status occurred, the evidence supports encoding progress only.

• Every pair in a C(15,5,3) covering occurs in at least five blocks.
• Every point in a C(15,5,3) covering occurs in at least eighteen blocks.
• Triple coverage plus point caps r_x<=18 is equivalent to triple coverage plus exact degrees r_x=18 in the root-block search.
• The checked candidate has 80332 variables and 481880 clauses.
• At both matched seeds, decisions fell from 18207 to 14299 and propagations from 8159494 to 2778592.
• No block family or canonical branch was excluded by the live runs.

• Candidate SHA-256 517e0312dc31a409aecaaa15fb8ec22aac76ea8f23acb9d313d729a6a2695b8b.
• Formula checker reconstructed 481880 clauses and reported valid=true.
• All 258 exhaustive small forward-totalizer cases passed.
• Smoke DRAT SHA-256 28b3508d6a2176499568374d5119012be54b9d12aea7ac14391b19b1a9c734c7 converted to LRAT and replayed.
• The smoke LRAT was rejected against the clean candidate.
• Result SHA-256 90271a177e0d436693aa48f9d2f1c0a867179a1a1705ff851009de4aaa05bad8; independent result-check SHA-256 04c8362599d356380942431a8946f88f34b348f2dfbd10d4e1f435023e88884d.

• .proof-experiments/20260810-081938-a609c0 generated the clean 481880-clause candidate.
• .proof-experiments/20260810-081949-99b680 independently reconstructed the candidate.
• .proof-experiments/20260810-082029-cde7a7, 082030-9c60ba, and 082031-53bbe6 produced and replayed the smoke DRAT/LRAT proof.
• .proof-experiments/20260810-082045-99359b and 082048-4abe54 performed the seed-0 matched comparison.
• .proof-experiments/20260810-082114-02a191 and 082117-f97875 performed the seed-1 adversarial control.
• .proof-experiments/20260810-082144-e8ef7f rejected the smoke proof against the clean formula.
• .proof-experiments/20260810-082212-e5fffc passed all 258 exhaustive small-counter cases.
• .proof-experiments/20260810-082358-36d31f independently reproduced the result arithmetic.

check_root_block_link_cap_cnf_v1.py independently enumerates blocks as masks and reconstructs every clause without importing the producer; check_root_block_link_cap_result_v1.py separately parses solver logs and recomputes the advancement gate.

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

• Schönheim/link counting -> predict exact degrees can be compiled as upper caps -> observed a 30.692172% clause reduction with exact logical coverage.
• C(12,6,4) certificate workflow -> require proof-compatible encoding and wrong-formula rejection before advancement -> DRAT/LRAT smoke replay and rejection both passed.
• Prior redundant pair-cap regression -> predict replacing existing equivalence rows is better than appending theorem-implied rows -> observed 21.464272% fewer decisions instead of a regression.

• For every pair xy, lambda_xy>=5.
  The 13 triples containing xy must be covered, while each block containing xy covers three possible third points. · Every C(15,5,3) covering · proved
• For every point x, r_x>=18.
  4r_x=sum_{y!=x}lambda_xy>=14*5=70. · Every C(15,5,3) covering · proved
• The clean link-cap formula is equivalent to the root-normalized exact-degree 54-cover search.
  Coverage supplies r_x>=18 and the CNF supplies r_x<=18; S_15 root-block transitivity preserves existence. · All putative 54-block covers up to relabeling · proved
• The link-cap candidate contains 80332 variables and 481880 independently reconstructed clauses.
  candidate-manifest.json and independent-check.json · Protocol root-block-link-cap-cnf-v1 · computed
• The two-seed bounded advancement gate passed.
  result.json and result-independent-check.json · CaDiCaL 1.7.3, seeds 0 and 1, 5000 conflicts · computed

• Rerun the injected complete fixed-pair-link gate as a new discriminator.
  All 395 saved signatures and 754 signature/e_45 targets. · The prior complete fixed-pair experiment retained every target under independent checking. · Prior result SHA-256 b5eb3ccf2ad757c0f2ec3098553a6c89ac47adb7c8cd68d10a2fa11ddd5ae9fb. · Add genuinely new labelled information beyond the complete fixed-pair link.
• Infer a cover or global exclusion from link-cap protocol v1.
  Four matched conflict-capped live runs. · Every run stopped at 5000 conflicts without SAT or UNSAT. · The four experiment receipts and independent result audit. · A directly checked SAT model or a complete replayed UNSAT proof.
• Dispatch the 3072-cell layer-five successor without owner approval.
  Twelve proposed 256-cell local union formulas. · The durable campaign checkpoint explicitly requires approval of that exact scope. · Epoch-44 receipt and epoch-47 checkpoint. · Explicit human-owner approval for exactly 3072 hash-bound cells.

• Canonical pair-branch link-cap transfer
  Combines a measured globally sound compression with the four complete structural branches rather than merely raising a cutoff. · Build and independently reconstruct type 2, then compare it with live-type2.cnf at 25000 conflicts. · high · open
• Proof-replayed layer-five local successor
  Its 288-cell predecessor is replay-certified, but the proposed successor remains local and approval-gated. · After explicit approval, double-generate and replay batch 0 before any remaining batch. · normal · open
• Constructive coverage-aware search
  A checked 54-cover would immediately settle the target, but prior exact-degree searches plateaued at defect 10. · Design a genuinely new coverage-aware move family with a below-10 defect gate. · low · open

Objective: Determine whether link-cap compression transfers to the complete multiplicity-five pair normalization.

First action: Implement a canonical type-2 generator retaining the five common blocks and uncovered triples while replacing residual exact degrees by forward-only upper caps.

Stop condition: Stop on any reconstruction mismatch, proof failure, or less than 20 percent decision reduction; validate SAT directly and replay UNSAT completely.

• Implement the link-cap replacement inside canonical pair-normalization type 2.
• Independently reconstruct every clause and residual cap before solver contact.
• Compare against the existing type-2 exact-degree CNF at seed 0 and 25000 conflicts.
• Stop on less than 20 percent decision reduction, any semantic mismatch, or proof-stack failure.
• Directly validate SAT; replay any live UNSAT result completely through DRAT and LRAT.
• Keep the 3072-cell layer-five job blocked until explicit owner approval.

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

GPT-5.6 Sol served as principal investigator. GPT-5.6 Terra delegates supplied advisory reconnaissance only; their memos were promoted with provenance and independently audited, and model agreement was not treated as validation. Python 3.12.3 generated and independently reconstructed the CNFs and parsed telemetry. CaDiCaL 1.7.3 ran bounded searches and emitted DRAT. Pinned drat-trim verified and converted DRAT to LRAT; pinned lrat-check replayed LRAT and rejected wrong-formula substitution. SHA-256 and the computational-researcher experiment harness bound artifacts. No new sub-agent, lab job, external write, publication, CAS, or proof assistant was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1281.2s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260810-083112-59a043

No human review recorded.