Qualified the proof-producing incidence/PB route by rebuilding hash-pinned CakeLPR and replaying two retained LRAT proofs plus exact final-line-deletion controls.

proof-producing incidence/PB cube decomposition

Remove common-mode verifier risk through a formally verified CakeLPR replay gate before designing a global cube frontier.

Hypothesis: Hash-pinned CakeLPR accepts both retained intact LRAT proofs and rejects both exact final-line-deletion mutants.

Test: Freshly compile the published CakeLPR sources, replay the epoch-27 and epoch-29 CNF/LRAT pairs, and require two VERIFIED UNSAT outputs and rejection of both deletion mutants.

The decisive artifacts bind all source, CNF, proof, and mutant hashes. Fresh CakeLPR builds returned VERIFIED UNSAT on both intact proofs, while exact deletion mutants failed. The result is intentionally limited to verifier qualification because neither proof belongs to an independently checked exhaustive global frontier.

• Hash-pinned CakeLPR accepts the retained epoch-27 and epoch-29 intact LRAT proofs.
• CakeLPR rejects both retained proofs after exact removal of their final line.
• A separate implementation reproduced the source hashes, input hashes, deletion relations, DIMACS-header checks, compilation, and all four replay outcomes.
• No global C(15,6,3) case was eliminated; the maintained range remains 30 <= C(15,6,3) <= 31.

• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py ... python3 scripts/audit_independent_lrat_gate_v1.py --out artifacts/epoch33-20260809/cake-lpr-independent-gate-v1/cake-lpr-gate-receipt.json
• Primary receipt status PASS, SHA-256 0abaf87a6f238be3549e51f50d9d95c65d8309445d4838e82a12181227b98ed6
• Independent recheck status PASS, SHA-256 d89a3e85fbb6b5d7e6d0c3bc3ff9f28a205c7b9dc4cd0eeada9f974d9ac8db98
• sha256sum -c artifacts/epoch33-20260809/cake-lpr-independent-gate-v1/SHA256SUMS passed for every listed artifact
• Primary intact replay times 0.588 and 2.839 seconds; mutant rejection times 0.806 and 2.226 seconds

• .proof-experiments/20260809-213637-9fbb1e: primary CakeLPR gate PASS in 7.051 seconds with two accepted intact proofs and two rejected mutants
• .proof-experiments/20260809-213823-67b9c0: independent rebuild/replay audit PASS in 6.853 seconds

scripts/check_independent_lrat_gate_receipt_v1.py independently rebuilt CakeLPR, verified every decisive hash and DIMACS header, reconstructed both exact deletion mutants, and reproduced all four replay outcomes.

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

• Certified C(12,6,4) SAT pipeline -> CakeLPR should accept retained C(15,6,3) ASCII LRAT instances and reject damaged proofs -> both intact instances passed and both exact deletion mutants failed.

• CakeLPR accepts the epoch-27 overdegree calibration proof.
  Primary and independent replays returned exactly s VERIFIED UNSAT for CNF SHA-256 ac8511e928a532c639f793b66eadd0de3cfcff4a9ad43fcf8ffb7108b046b311 and proof SHA-256 e1c7b54c3d25ef8c0049b62f5d31f2cde96039c59da50df177f1c32700b77ece. · The retained epoch-27 local overdegree calibration instance only · computed
• CakeLPR accepts the epoch-29 r=4 two-open-leaf proof.
  Primary and independent replays returned exactly s VERIFIED UNSAT for CNF SHA-256 b5292c8d982c0afea8cde13a4d8a99d812665119ca33c11f39afae5f72e02ceb and proof SHA-256 9712c8540bae08c2f5bd138f0dec19f148c8dee11e8a6558c520d5ac8d63b343. · The retained epoch-29 fixed local leaf only · computed
• Both retained mutants are exact final-line deletions and are rejected by CakeLPR.
  independent-recheck.json records byte-exact deletion relations and the diagnostic c empty clause not derived at end of proof for both mutants. · The two retained proof pairs · computed
• The proof-producing route now has a materially independent local LRAT replay implementation.
  Hash-pinned CakeLPR source set and two independently recorded PASS receipts. · Verifier qualification; not frontier completeness or global UNSAT · computed

• Treat recompilations of the retained lrat-check.c implementation as independent checker diversity.
  Epoch-27 and epoch-29 legacy replay binaries · The binaries are byte-identical and derive from the same source. · cake-lpr-gate-receipt.json records common binary and source hashes. · A materially different implementation or formally verified kernel, now supplied by CakeLPR.
• Use the current master basis_ffi.c while claiming conformance to the published cake_lpr.sha256 manifest.
  Official repository snapshot audited on 2026-08-09 · The July 22 wrapper source has a different SHA-256; the published manifest still pins its parent revision. · tools/cake_lpr/PROVENANCE.md and the source hash audit · The upstream manifest is updated and the new source set is separately pinned and replay-tested.

• Canonical exactly-one-owner second-block frontier
  It is the smallest remaining prerequisite for accumulating independently replayable global proof leaves. · Enumerate all 5004 normalized second-block choices with primary and independent owner maps; require full coverage and multiplicity exactly one. · high · open
• One bounded proof-size calibration after frontier validation
  A genuine frontier leaf will measure proof-size feasibility without committing to a global run. · Generate one hash-bound assumption-literal leaf, emit LRAT, replay with CakeLPR, and compare proof bytes and wall time with the declared budget. · normal · open
• Fixed-C5 constructive one-orbit tail lookup
  This remains a materially different witness route if proof decomposition stalls. · Run matched fixed-node and fixed-wall controls using an exact residual-cycle-profile tail index. · normal · open

Objective: Build and independently validate a hash-bound disjoint complete second-block frontier.

First action: Implement scripts/audit_second_block_frontier_v1.py over all 5004 normalized choices and run it through run_experiment.py with an exactly-one-owner success condition.

Stop condition: Redirect on any ownership gap, duplicate ownership, domain mismatch, hash drift, or CNF semantic mismatch; a frontier pass authorizes only one bounded leaf calibration.

• Implement a deterministic canonical-owner function for all 5004 normalized second-block choices.
• Independently enumerate the same domain and require exactly-one ownership, full coverage, and no overlap.
• Hash-bind the frontier manifest and reconstruct each leaf CNF from the mathematical specification.
• Only after the frontier audit passes, generate and CakeLPR-replay one bounded assumption-literal leaf to estimate proof size.
• Preserve the constructive incidence and fixed-C5 routes as immediate alternatives if the frontier is incomplete or projects beyond the certificate budget.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://github.com/tanyongkiam/cake_lpr ↗
• https://raw.githubusercontent.com/tanyongkiam/cake_lpr/master/cake_lpr.sha256 ↗
• https://github.com/tanyongkiam/cake_lpr/commit/a36874a8b750b43fe4b385b8ddbf5b033e46a3fa ↗
• https://arxiv.org/html/2607.23766v1#S6 ↗

GPT-5.6 Sol principal designed and audited the epoch. GPT-5.6 Terra delegates supplied advisory prior-art and verification memos; their agreement was not treated as validation. Deterministic work used Python 3.12.3, GCC, SHA-256, jq, the experiment harness, and hash-pinned CakeLPR/CakeML-generated assembly. A read-only GitHub connector acquired official source bytes because shell DNS was unavailable; web search checked current primary sources and literature. The retained LRAT files were generated in earlier epochs by CaDiCaL/drat-trim; no new SAT solving, CAS, or proof-assistant run occurred this epoch.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

991.5s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260809-214442-4cd039

No human review recorded.