Zero-search independent reconstruction and dual replay of the hash-pinned epoch-94 type-2 local UNSAT certificate as a fail-closed gate for the proof-producing route.

proof-producing incidence/PB cube decomposition

Reconstruct one retained exact incidence CNF with a separate clause constructor, reconvert its DRAT to LRAT, replay with lrat-check and CakeLPR, and reject semantic and proof mutations before authorizing any new cube.

Hypothesis: The hash-pinned epoch-94 type-2 local UNSAT certificate reconstructs and replays without solver search, while every declared semantic and proof mutation fails closed.

Test: Run the clean-room checker once under a 180-second and 1024-MiB cap; require byte-identical CNF reconstruction and LRAT reconversion, intact acceptance by lrat-check and CakeLPR, and rejection of all eleven proof/base mutations.

The deterministic receipt establishes proof-pipeline integrity at its exact local scope. Because it is byte-identical to a prior validated receipt and creates no new exhaustive coverage, it cannot count as mathematical progress or satisfy the exact-optimum gate.

• For CNF SHA-256 9a8e79067683668775004b95a79b7c10dcf6ff5f56fbe2b9ddd3677d91fe173a and DRAT SHA-256 c9bfd06b7aabc91aea5be3d256540cb1cf125a6b093b9e0b76c416090cb64476, fresh conversion yields LRAT SHA-256 85746556ae7f0416c81b33aae4e8d923c882abc6933556f1b00e500f5e6c7368 and both retained proof semantics and fail-closed controls replay in the current environment.
• The new independent receipt is byte-identical to the retained epoch-94 receipt.
• No new C(15,6,3) case was excluded, and the maintained range remains 30 <= C(15,6,3) <= 31.

• sha256sum -c artifacts/epoch94-20260811/SHA256SUMS: every retained input OK.
• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py ... python3 checkers/check_type2_min_leaf_drat_v1.py --run-dir artifacts/epoch94-20260811/type2-min-leaf-drat-v1 --out artifacts/epoch99-20260811/type2-proof-replay-independent-check-v1.json: return code 0 in 18.453 seconds.
• cmp of the epoch-99 and epoch-94 independent receipts returned equal; both hash to 014d6fe125c85729bcdd3952674f99f3f08a0b243f6009ba6c891b8ec97dce15.
• sha256sum -c artifacts/epoch99-20260811/SHA256SUMS: all epoch-99 and decisive retained artifacts OK.

• .proof-experiments/20260811-220245-67f3d0: PASS_TERMINAL/CERTIFIED_LOCAL_TYPE2_MIN_UNSAT in 18.453 seconds, peak child memory 538880 KiB, no solver search, receipt SHA-256 014d6fe125c85729bcdd3952674f99f3f08a0b243f6009ba6c891b8ec97dce15.

check_type2_min_leaf_drat_v1.py does not import the producer; it uses the separate check_root_prefix_global_completion_v1.py constructor, freshly compiles drat-trim, lrat-check, and CakeLPR at a different optimization setting, requires byte-identical reconstruction and conversion, and rejects eleven proof/base mutations.

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

• C(12,6,4) certificate architecture -> predict that a proof route must survive reconstruction, dual replay, and mutation rejection before scale-up -> observed a complete pass for one retained local cylinder, but no ownership or global coverage gain.

• The current pinned environment reproduces the retained epoch-94 independent receipt byte-for-byte.
  Experiment 20260811-220245-67f3d0 and receipt SHA-256 014d6fe125c85729bcdd3952674f99f3f08a0b243f6009ba6c891b8ec97dce15. · Exact retained formula/proof/tool source hashes only. · computed
• The selected type-(6,6,4^12) depth-four cylinder has no completion under the exact 49966-variable, 191177-clause encoding.
  Byte-identical CNF reconstruction, fresh identical LRAT conversion, lrat-check and CakeLPR acceptance, and eleven rejected mutations. · One selected local cylinder only; this is a revalidation of the epoch-94 claim. · computed

• Treat the epoch-99 replay as a new local or global mathematical exclusion.
  This epoch's exact byte-identical replication control. · It reproduces the same formula, proof, and result receipt as epoch 94 and excludes no additional family. · Both independent receipts have SHA-256 014d6fe125c85729bcdd3952674f99f3f08a0b243f6009ba6c891b8ec97dce15. · A distinct owned cylinder with a separately replayed terminal proof or a globally valid cover.
• Rerun an unchanged fixed-second six-representative proof cube.
  Existing incidence/PB formulas and the recorded short-run protocol. · The six cases overlap at solution level; a genuine r=5 run and multiple exact-profile proof calibrations are already nonterminal or below continuation gates. · artifacts/epoch99-20260811/source-prior-art-audit.md and the cited internal attempts. · Independently checked exactly-once ownership, a material encoding/proof change, or terminal SAT/dual-replayed UNSAT evidence.
• Scale flat local proof accumulation after the replay pass.
  Unowned depth-four local cylinders analogous to epoch 94. · A local proof does not aggregate without complete ownership, and the prior projected certificate volume is prohibitive. · Epoch-94 technical report and the unchanged absence of a complete owner frontier. · A hash-bound exactly-once frontier and measured certificate budget showing feasible exhaustive coverage.

• Receipt-valid pair-surplus depth-two owner layer.
  It attacks the missing global ownership premise and repairs the injected epoch-98 receipt-validation problem before relying on that result. · Rerun the saved producer and independent checker, bind every decisive immutable input in SHA256SUMS, and require byte-identical output plus all five mutation rejections. · high · open
• Dual canonical owner-pair controls on 3K5 and the saved circulant H.
  Agreement plus automorphism-induced tie checking is the cheapest discriminator for extending an owner prefix toward a global decomposition. · Implement two materially different rooted colored-graph codes and compare owner orbits, digests, and parent assignments on both controls. · high · open
• Materially different constructive exact-degree-12 search.
  A checked 30-block witness settles the target without an exhaustive negative certificate. · Predeclare a new global move or encoding not covered by closed support-two/support-three and six-representative runs, then require a short direct-model or measured throughput gate. · normal · open

Objective: Repair and qualify a globally relevant pair-surplus ownership prefix before any new proof leaf.

First action: Run the epoch-98 pair_surplus_depth2_ownership_v1 producer and independent checker from immutable inputs, create a minimal valid evidence receipt and SHA256SUMS, and require exact digest and mutation agreement.

Stop condition: Stop or redirect on input hash drift, receipt invalidation, canonicalizer disagreement, a non-automorphic owner tie, missing or duplicate parent, or projected frontier/certificate volume beyond the declared cap.

• Reproduce the epoch-98 pair-surplus depth-two producer and independent checker from immutable inputs and create a receipt that passes the evidence-file contract.
• If that receipt passes, implement two independent rooted-colored-multigraph canonicalizers on the saved 3K5 and circulant controls; reject non-automorphic ties or any disagreement.
• Only after exactly-once ownership survives should one new proof leaf be compiled with a predeclared certificate budget.
• Keep a materially different constructive degree-12 witness route active because any directly checked 30-block cover is globally decisive.

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

GPT-5.6 Sol was principal investigator. A GPT-5.6 Terra experiment-verification delegate supplied the advisory replay suggestion; Sol promoted it with provenance, independently audited all claims, and did not count model agreement as validation. Deterministic tools were CPython 3.12.3, GCC 13.3.0, SHA-256, freshly compiled drat-trim, lrat-check, CakeLPR, and the computational-researcher experiment harness. CaDiCaL 1.7.3 was version-audited but performed no search. Web access checked LJCR, the maintained Covering Repository context, original covering-design literature, and arXiv:2607.23766. No PB solver, CAS, proof assistant, checkpointed lab, external proof service, external expert, publication, or system-level modification was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

937.8s

Review state

not a result claim

Attempt ID

covering-c1563-20260811-221052-7cdcbc

No human review recorded.