Freeze and independently audit a 32-leaf stratified type-0 DRAT pilot, then execute and reproduce exactly its first leaf under 60-second and 8-MiB proof caps.

stratified canonical root-link DRAT calibration

Hash-stratify the independently audited depth-four type-0 frontier, reconstruct selected completion CNFs through two encodings, and measure certificate termination under fixed proof-output limits.

Hypothesis: The first frozen stratified type-0 cylinder terminates as SAT or replayable UNSAT within 60 seconds and an 8-MiB DRAT cap.

Test: Run CaDiCaL 1.7.3 with seed 0 and -P0 on q0-m0 after byte-for-byte independent CNF reconstruction; reproduce once and separately audit the result.

Independent CNF equality, two identical capped proof prefixes, exact SIGXFSZ exits, absence of terminal solver lines, and a separate checker establish the scoped proof-output failure. They establish no satisfiability or covering claim.

• The frozen post-q0-q3 manifest contains exactly 32 unique leaves, eight midpoint ranks in each of four quartiles of sizes 563,564,563,564.
• For q0-m0, two CaDiCaL 1.7.3 seed-0 -P0 runs produced the same 8388608-byte DRAT prefix and exited by SIGXFSZ before SAT/UNSAT.
• The exact covering range remains 30 <= C(15,6,3) <= 31.

• python3 scripts/freeze_type0_leaf_pilot_v1.py --frontier artifacts/epoch86-20260811/cleanroom-type0-frontier-primary.json --exclusions artifacts/epoch83-20260811/root-prefix-global-completion-v4/selection.json --manifest artifacts/epoch87-20260811/type0-32-leaf-pilot-manifest.json
• python3 checkers/check_type0_leaf_pilot_manifest_v1.py --historical-source artifacts/epoch19-20260809/root_link_canonical_primary_receipt.json --manifest artifacts/epoch87-20260811/type0-32-leaf-pilot-manifest.json --receipt artifacts/epoch87-20260811/type0-32-leaf-pilot-independent-check.json
• Primary and reproduction q0-m0 runs returned UNKNOWN_PROOF_CAP with identical CNF and DRAT hashes.
• sha256sum -c artifacts/epoch87-20260811/SHA256SUMS passed for every listed artifact.

• .proof-experiments/20260811-131734-828d0a: froze 32 unique leaves from a 2254-key post-exclusion population.
• .proof-experiments/20260811-131744-cbf3c5: independently reconstructed all 32 owners and passed three controls.
• .proof-experiments/20260811-132309-a21bc6: q0-m0 reached exactly 8388608 DRAT bytes and SIGXFSZ without terminal status.
• .proof-experiments/20260811-132344-3585fe: reproduced the same CNF and capped DRAT prefix.
• .proof-experiments/20260811-132446-c6f75b: separate checker confirmed exact-cap nontermination and rejected misclassification.

checkers/check_type0_first_leaf_cap_v1.py independently rebuilds q0-m0 using checkers/check_root_prefix_global_completion_v1.py, verifies dimensions and bytes, audits both logs and checkpoints, compares proof-prefix hashes, and ensures no capped result is reported as UNSAT.

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 certified link-orbit decomposition -> predict that representative local cylinders can yield compact replayable certificates -> q0-m0 instead saturated the DRAT cap before termination, so proof-format efficiency must be discriminated before scaling.

• The frozen 32-key selection has exactly eight unique midpoint ranks in each post-exclusion hash quartile.
  type0-32-leaf-pilot-independent-check.json · The 2254 type-0 depth-four keys remaining after q0-q3 are omitted from sampling. · computed
• q0-m0 deterministically produces the same exact-cap DRAT prefix in two matched runs.
  CNF SHA-256 d81a3160db2fa07522fed34a4ea8aad678aeb0d7d955caf06394d72e7993f924; DRAT SHA-256 b5a08a8e8c3b26d28199ceadc072257b0a0652d3d46b741653b09828c72b49c6 · CaDiCaL 1.7.3 seed 0 -P0, canonical q0-m0 CNF, 8-MiB DRAT cap · computed

• Obtain a terminal q0-m0 result with unchanged CaDiCaL 1.7.3 seed-0 -P0 DRAT emission under an 8-MiB cap.
  The exact q0-m0 CNF and fixed solver protocol only · Two deterministic runs filled the cap and received SIGXFSZ before SAT/UNSAT. · artifacts/epoch87-20260811/type0-first-leaf-cap-independent-check.json · A material proof-emission change, verified compression mechanism, or explicitly justified larger raw-proof budget

• Native external LRAT on q0-m0
  It directly separates DRAT-conversion overhead from inherent proof volume on the same formula. · Run one native-LRAT q0-m0 process with the same cap and CakeLPR controls. · high · open
• Constructive incidence search with a material propagation enhancement
  A valid 30-block witness remains the cheapest terminal certificate and avoids proof-volume scaling. · Predeclare and compare one new symmetry or propagation constraint against the retained six-case incidence baseline. · normal · open
• Canonical ownership bridge
  Even successful leaf proofs cannot aggregate without exact coverage and uniqueness. · Formalize deletion ownership and test it on bounded completed-link examples. · normal · open

Objective: Determine whether q0-m0's failure is DRAT-format-specific.

First action: Implement and run a single native-external-LRAT q0-m0 mode with exact CNF binding, an 8-MiB cap, CakeLPR replay, and final-line-deletion rejection.

Stop condition: Redirect if native LRAT also reaches 8 MiB before termination or any replay/control fails; compare bytes and time before any scale-up if it succeeds.

• Test native external LRAT on exactly q0-m0 under the same raw 8-MiB cap.
• Require CakeLPR replay and final-line-deletion rejection before retaining a terminal native-LRAT result.
• Do not submit or run the 32-leaf tranche until lab registration works and the proof-emission mechanism passes the q0-m0 matched-format test.

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

GPT-5.6 Sol principal designed, implemented, and audited the epoch. Two pre-completed GPT-5.6 Terra delegates supplied advisory reconnaissance but were not independent validators, and no delegate artifact was promoted. Deterministic tools were CPython 3.12.3, CaDiCaL 1.7.3, GCC, drat-trim and CakeLPR source builds, exact graph6 reconstruction, SHA-256, and the computational-researcher experiment harness. The web connector was queried but returned no usable source content. No PB solver, CAS, proof assistant, external proof service, system installation, publication action, or human validator was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1161.9s

Review state

not a result claim

Attempt ID

covering-c1563-20260811-133032-3109dc

No human review recorded.