Full proof-producing 30-block completion cylinders for four deterministic canonical type-0 depth-four root-link prefixes

canonical root-prefix global-completion SAT

Fix a canonical four-block root-link prefix, split 30 incidence columns into 12 root and 18 non-root blocks, quotient exchangeable columns by strict lexicographic order, and seek terminal LRAT-certified completion results.

Hypothesis: At least three of four deterministic hash-quartile type-0 depth-four prefixes have globally UNSAT completion cylinders with dual-replayed LRAT proofs within 20 seconds and 8 MiB each.

Test: Construct four independently reproducible 49962-variable, 191161-clause global-completion CNFs, run CaDiCaL 1.7.3 for 20 seconds per leaf, and require at least three intact proofs to replay in both lrat-check and CakeLPR.

The three intact proofs and byte-identical independent reconstructions establish narrowly scoped subtree exclusions. They neither cover the complete prefix frontier nor satisfy the campaign's dual-replay scale gate, so the result is progress rather than a candidate exact value.

• No 30-block cover extends canonical prefix Q???????????????OBsF_ow@{??.
• No 30-block cover extends canonical prefix Q???????????????OO{BoO]@y??.
• No 30-block cover extends canonical prefix Q???????????????^??@{PKPf??.
• Prefix Q???????????????OEkAUBc_MK? remains unresolved at the checked 20-second limit.
• The exact range remains 30 <= C(15,6,3) <= 31.

• Accepted producer command recorded in .proof-experiments/20260811-102949-3b71f7/experiment.json
• Accepted independent audit command recorded in .proof-experiments/20260811-103104-23adb0/experiment.json
• sha256sum -c artifacts/epoch83-20260811/hash-manifest.sha256 returned OK for every listed artifact
• Independent receipt reports four byte-identical reconstructions, three fresh CakeLPR acceptances, zero dual replays, one UNKNOWN, and four rejected mutations

• .proof-experiments/20260811-102949-3b71f7: four-leaf bounded producer run; three CakeLPR-verified UNSAT results and one UNKNOWN
• .proof-experiments/20260811-103104-23adb0: independent audit; four byte-identical CNFs, three fresh CakeLPR acceptances, legacy failures reproduced, four mutations rejected

checkers/check_root_prefix_global_completion_v1.py independently reconstructs every CNF and validates status semantics. CakeLPR accepted all three complete proofs. The intended second replay implementation, lrat-check, segfaulted and therefore did not provide dual validation.

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

• Krug's link/extension certificate architecture -> canonical prefixes coupled to full global completion cylinders should terminate in proof-producing leaves -> three of four sampled leaves produced complete CakeLPR-accepted LRATs, but the dual-checker gate failed

• The maintained range is 30 <= C(15,6,3) <= 31.
  Maintained LJCR entry and its explicit 31-block construction; slack-zero lower bound 30 · Global C(15,6,3) · proved
• Three named canonical type-0 depth-four root-link prefixes have no 30-block completion.
  Byte-identical independent CNF reconstruction and three fresh CakeLPR-accepted LRAT proofs · Exactly Q???????????????OBsF_ow@{??, Q???????????????OO{BoO]@y??, and Q???????????????^??@{PKPf?? · computed
• The fourth sampled prefix was not decided within 20 seconds.
  q2 CaDiCaL log and accepted run manifest · Q???????????????OEkAUBc_MK? under the v4 formula and solver configuration · computed

• Scale the current prefix-completion pipeline immediately to 32 leaves.
  The current direct-LRAT pipeline using pinned lrat-check and CakeLPR · The predeclared dual-replay gate failed: zero of three terminal large proofs passed lrat-check because it segfaulted. · v4 run manifest and independent checker receipt · A second pinned replayer accepts all three stored proofs and rejects proof mutations under the declared resource bound.
• Treat the earlier epoch-20 link-completion encoding as a global completion filter.
  The epoch-20 four-block-to-twelve-block link-only formulas · Those formulas omitted the remaining 18 non-root blocks and could not exclude global covers when link completion was SAT. · scripts/root_link_completion_pilot_v1.py and the epoch-20 scope receipt · Not applicable; use the epoch-83 full global-completion encoding instead.

• Second independent LRAT replayer for the three stored proofs
  It is the cheapest test that can convert the observed three-of-four closure signal into a passed routing gate without rerunning SAT. · Replay q3.cnf/q3.lrat with a pinned alternative checker and two proof mutants under 1 GiB. · high · open
• Frozen 32-prefix global-completion measurement
  If dual replay is repaired, a 29-of-32 closure rate would support a projected tenfold prefix-frontier reduction. · Hash-select 32 lower medians from consecutive buckets and run fresh bounded proof-producing processes. · normal · open
• Alternative encoding for the unresolved q2 leaf
  q2 accumulated the most conflicts and reached the time limit, so a matched DRAT-first or selector encoding can test whether the obstruction is encoding-specific. · Compile q2 under one materially different proof-producing encoding and compare preprocessing dimensions before solving. · low · open

Objective: Repair independent proof replay without rerunning SAT, then decide whether the 32-prefix measurement is licensed.

First action: Run a replacement LRAT checker on artifacts/epoch83-20260811/root-prefix-global-completion-v4/q3.cnf and q3.lrat with final-line-deletion and poisoned-final-hint controls.

Stop condition: Redirect if the checker fails, disagrees with CakeLPR, or exceeds 1 GiB; proceed to 32 prefixes only after all three stored proofs dual-replay.

• Qualify a second pinned LRAT replayer on q3 with intact, final-line-deletion, and poisoned-final-hint controls.
• If all three stored proofs dual-replay, freeze a 32-prefix selection and require at least 29 dual-certified exclusions before further scale-up.
• If the second replayer fails, redirect to a pinned DRAT-to-LRAT transport or a different proof encoding.
• Do not extrapolate sampled closures or rerun the unfiltered root-link catalogue.

• 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/html/2607.23766v1 ↗

GPT-5.6 Sol acted as principal investigator. GPT-5.6 Terra delegates supplied advisory reconnaissance only; their claims were independently audited and were not counted as validation. Python 3.12.3 generated and independently reconstructed CNFs. CaDiCaL 1.7.3 emitted direct ASCII LRAT. CakeLPR from pinned basis_ffi.c and cake_lpr.S verified three proofs. The pinned drat-trim lrat-check.c passed the tiny control but segfaulted on all three large bases. GNU gcc 13.3.0 compiled replayers. Web search checked the maintained repository, LJCR, Gordon–Kuperberg–Patashnik, and Krug 2026. No CAS, proof assistant session, cloud lab, external proof service, or human validator was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1784.7s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260811-103701-e1a983

No human review recorded.