Qualified binary-DRAT transport on a known UNSAT control, then ran one fixed-cap binary-DRAT calibration on the frozen SHA-ranked index-one root-link selector CNF.

proof-format transport on certified root-link selector CNF

Change only CaDiCaL proof serialization from ASCII to binary DRAT, qualify conversion and dual LRAT replay on q0-m0, then test whether the same 16 MiB cap permits the frozen target node to terminate.

Hypothesis: After a known-UNSAT binary-DRAT transport control passes, default binary DRAT lets CaDiCaL 1.7.3 decide the frozen rank-one root-link CNF with a checked model or dual-replayed proof within 60 seconds and 16777216 proof bytes.

Test: Replay binary DRAT on q0-m0; only on success run the target once with seed 0, -P0, 60 seconds, 1 GiB, and a 16 MiB cap, accepting only a checked link or independently reconstructed and dual-replayed LRAT.

The predeclared terminal observables were a directly checked complete link or a complete independently replayed proof. Neither occurred. The validated transport calibration is reusable, but it does not satisfy the contribution gate and decisively triggers the route's redirect condition.

• For the frozen q0-m0 control, binary DRAT is 4170549 bytes versus 8757790 bytes for matched ASCII DRAT, and both convert to the same 4537565-byte LRAT.
• For the frozen rank-one link CNF, binary DRAT hit exactly 16777216 bytes after 12.785724 seconds and returned UNKNOWN.
• The target binary prefix is not an UNSAT certificate; fresh drat-trim rejected it.
• The maintained range remains 30 <= C(15,6,3) <= 31.

• python3 scripts/type2_rank1_binary_drat_v1.py --out-dir artifacts/epoch104-20260812/type2-rank1-binary-drat-v1
• python3 checkers/check_type2_rank1_binary_drat_v1.py --run-dir artifacts/epoch104-20260812/type2-rank1-binary-drat-v1 --out artifacts/epoch104-20260812/type2-rank1-binary-drat-independent-check.json returned PASS_NONTERMINAL and CLOSE_BINARY_SELECTOR_CNF_ROUTE.
• python3 checkers/check_epoch104_receipt_v1.py --out artifacts/epoch104-20260812/aggregate-independent-check.json returned PASS.
• Fresh q0-m0 conversion reproduced LRAT SHA-256 bc1df8123ce77e87b9e8aad3372a663968aad19f48e6147e6da440643a5dcb79; both replay kernels accepted it and both rejected its final-line-deleted mutant.
• Fresh drat-trim rejected target prefix SHA-256 2664b97d89b0f3967a05d5ebd9277de659ba736f35fc94f641f23ab7fe429449.

• .proof-experiments/20260812-013036-a9e0b7: q0-m0 binary transport passed; target hit 16 MiB and returned UNKNOWN.
• .proof-experiments/20260812-013128-d601e2: independent reconstruction, fresh q0 replay, mutation rejection, and target-prefix rejection passed.
• .proof-experiments/20260812-013357-d96d13: hash-bound aggregate receipt audit passed.

checkers/check_type2_rank1_binary_drat_v1.py independently reconstructs both formulas from graph semantics, compiles fresh replay tools, reconverts and dual-replays q0-m0, rejects final-line deletion, and rejects the target prefix; checkers/check_epoch104_receipt_v1.py binds the decisive hashes and measurements.

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

• Binary serialization of proof traces -> predict approximately halved DRAT storage on a matched known-UNSAT control -> observed 47.621021% of ASCII bytes, but the target still saturated the cap, so serialization alone is rejected as a target route.

• The pinned binary-DRAT transport pipeline produces a replayable q0-m0 certificate and the same canonical LRAT as the matched ASCII run.
  Independent fresh conversion, byte-identical LRAT SHA-256 bc1df8123ce77e87b9e8aad3372a663968aad19f48e6147e6da440643a5dcb79, dual replay, and two final-line-deletion rejections. · q0-m0 CNF SHA-256 d81a3160db2fa07522fed34a4ea8aad678aeb0d7d955caf06394d72e7993f924; CaDiCaL 1.7.3 seed 0 -P0. · computed
• Binary DRAT does not decide the selected rank-one root-link node under the frozen cap.
  Producer hit exactly 16777216 bytes with status UNKNOWN; independent reconstruction passed and fresh drat-trim rejected the prefix. · Target CNF SHA-256 57c7430a941666bdf1c3a12bb7527b7cf0f4dceb796e16a57b15969790bbd134; CaDiCaL 1.7.3 seed 0 -P0, 60 seconds, 16 MiB. · computed

• Use binary DRAT alone to make the selected selector-CNF node certifiable under 16 MiB.
  Frozen target CNF, CaDiCaL 1.7.3, seed 0, -P0, 60 solver seconds, 75-second watchdog, 1 GiB, 16 MiB proof cap. · The binary proof hit the exact cap and the solver returned UNKNOWN. · Hash-bound producer receipt, independent byte-exact reconstruction, explicit prefix rejection, and aggregate PASS. · A materially different encoding, solver/proof mechanism, or segmented proof-prefix design that passes a matched bounded replay gate.
• Infer that the selected link node is UNSAT, or that C(15,6,3)=31, from the capped prefix.
  One local root-link node and the global covering number. · The prefix derives no verified contradiction and the node remains UNKNOWN. · Fresh drat-trim rejection and independent receipt field global_covering_bound_changed=false. · A directly checked link or cover, or a complete replayed proof with independently checked exhaustive ownership.

• Hash-owned complete canonical root-link catalogue.
  A complete fixed link reduces remaining global incidence positions from 450 to 252 and can support exhaustive completion branches; a partial frontier cannot. · Run a 10000-owned-node or 120-second augmentation pilot only after a separate canonical-deletion parent checker is written. · high · open
• Materially changed exact-degree-12 constructive witness search.
  A 30-block list remains the smallest terminal certificate and should retain symmetric consideration with exclusion routes. · Specify a new global move or encoding outside exhausted local shells and predeclare a short direct-cover gate over all 455 triples. · normal · open
• Proof-producing native pseudo-Boolean decomposition.
  It could avoid totalizer-heavy CNF, but currently lacks a pinned emitter and two-kernel replay premise. · Acquire project-scoped pinned RoundingSat, VeriPB, and CakePB only under a future authorized toolchain task, then qualify the smallest known UNSAT control before target contact. · low · open

Objective: Measure whether a hash-owned canonical augmentation can reach or bound complete root links with independently checked ownership.

First action: Write the full-link pilot predeclaration and a separate canonical-deletion parent checker, then run at most 10000 owned nodes or 120 seconds.

Stop condition: Stop or redirect on parent-coverage failure, unfiltered shallow frontier explosion, or inability to emit a hash-owned completeness frontier; promote only a complete independently validated catalogue, checked cover, or replayed exhaustive proof.

• Close binary selector-CNF proof production for this node under the 16 MiB cap; do not enlarge the cap or batch nodes.
• Predeclare a 10000-owned-node or 120-second canonical full-link augmentation pilot with a separately implemented parent-ownership checker.
• Keep native PB blocked until pinned RoundingSat, VeriPB, and CakePB emitters/checkers pass a known-UNSAT replay calibration.
• Retain constructive witness search only for a materially changed mechanism outside the exhausted local shells and repeated six-representative throughput controls.

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

GPT-5.6 Sol principal investigator; two GPT-5.6 Terra delegates for advisory reconnaissance only. Python 3.12.3, CaDiCaL 1.7.3, GCC, drat-trim, lrat-check, CakeLPR, SHA-256, exact integer/set arithmetic, and the computational-researcher experiment harness were used. No model agreement counted as validation; no CAS, proof assistant, PB solver, cloud lab, external proof service, or human validator produced evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1148.1s

Review state

not a result claim

Attempt ID

covering-c1563-20260812-014132-5d18f2

No human review recorded.