Provision and independently validate replayable LRAT proof plumbing on the full r=5 incidence encoding using its smallest monotone exact-degree overfull calibration cube.

proof-producing incidence/PB cube decomposition

Reuse the structurally audited six-representative incidence encoding, emit ASCII external LRAT with pinned CaDiCaL, and replay it using independently sourced pinned lrat-check.

Hypothesis: Pinned CaDiCaL 1.7.3 and an independently sourced LRAT checker can emit and replay a proof for the full r=5 incidence formula under the smallest overdegree calibration cube.

Test: Force point 0 into eleven residual columns, making its degree at least 13 against exact degree 12; require solver UNSAT, independent VERIFIED replay, correct DIMACS dimensions, proof below 64 MiB, and rejection after deleting the final LRAT line.

The hash-bound final CNF, proof, solver log, replay logs, independently regenerated receipt, and mutation failure establish proof-pipeline compatibility. Because the cube is deliberately overfull and outside any exhaustive frontier, the evidence supports infrastructure progress only.

• CaDiCaL 1.7.3 emitted an independently replayable LRAT proof for the specified 33162-variable, 156403-clause r=5 calibration CNF.
• The proof contains 2745 lines and 313528 bytes and has SHA-256 e1c7b54c3d25ef8c0049b62f5d31f2cde96039c59da50df177f1c32700b77ece.
• Deleting the proof's final line causes both replay attempts to return NOT VERIFIED.
• No global C(15,6,3) search cube, witness, or lower-bound case was resolved.

• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py ... python3 scripts/proof_replay_calibration_v1.py --out-dir artifacts/epoch27-20260809/r5-lrat-calibration-v2
• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py ... python3 checkers/check_proof_replay_calibration_v1.py --artifact-dir artifacts/epoch27-20260809/r5-lrat-calibration-v2 --receipt artifacts/epoch27-20260809/independent_checker_receipt.json
• Hash-manifest audit: 21 files checked, zero mismatches.

• .proof-experiments/20260809-161051-d8920f: corrected proof-producing calibration passed in 1.729 seconds total; proof size 313528 bytes.
• .proof-experiments/20260809-161148-c9fc4d: clean-room reconstruction, recompile, replay, and mutation rejection passed in 0.881 seconds.
• .proof-experiments/20260809-160928-dc90f4: excluded development control; exposed octal parsing of zero-padded dimensions.

Marijn Heule's pinned lrat-check.c replayed the LRAT derivation. check_proof_replay_calibration_v1.py independently reconstructed the CNF delta, compiled a fresh checker binary, replayed the proof, verified dimensions, and rejected the truncated proof.

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

• Ramsey proof-certificate tooling -> a pre-acquired pinned lrat-check source should interoperate with CaDiCaL external ASCII LRAT -> verified after correcting the DIMACS header format.
• Mutation testing from certified exhaustive searches -> deleting the terminal empty-clause derivation should fail closed -> both checker runs returned NOT VERIFIED.

• The final calibration CNF is the audited r=5 source body plus exactly eleven units for point 0 in columns 2 through 12, with an unpadded updated header.
  artifacts/epoch27-20260809/independent_checker_receipt.json · CNF SHA-256 ac8511e928a532c639f793b66eadd0de3cfcff4a9ad43fcf8ffb7108b046b311 · computed
• The calibration CNF is UNSAT.
  LRAT proof SHA-256 e1c7b54c3d25ef8c0049b62f5d31f2cde96039c59da50df177f1c32700b77ece independently replayed to the empty clause. · Only the declared r=5 overdegree calibration. · proved
• The final-line-deleted proof is not accepted by the pinned checker.
  artifacts/epoch27-20260809/r5-lrat-calibration-v2/lrat-check-drop-final-line.log and the independent checker receipt · The exact mutated proof SHA-256 8d5e53766858414482d7e281704997942bd516222e56a1371eb45e666c59d1c6 · computed

• The proof-producing incidence route is blocked because no independent LRAT replayer is available.
  Current project-scoped toolchain on 2026-08-09. · A pinned upstream lrat-check source was found in pre-acquired project data, promoted with provenance, compiled, and passed positive and negative controls. · artifacts/epoch27-20260809/independent_checker_receipt.json · A future source/hash mismatch, replay defect, or incompatibility with production proofs.
• Use the zero-padded v1 calibration as evidence.
  artifacts/epoch27-20260809/r5-lrat-calibration-v1 and experiment 20260809-160928-dc90f4. · lrat-check's scanf %i interpreted padded dimensions as octal. · The v1 replay log reported 13938 variables and 56579 clauses instead of 33162 and 156403. · none; use the corrected v2 artifact.
• Repeat the delegate-proposed archival three-delete/two-insert census.
  All such repairs of the fixed archival 31-cover. · Epoch 5 already exhaustively checked 18313 valid candidate pairs using two implementations and found zero repairs. · artifacts/epoch5-20260808/three_for_two_receipt.json · A demonstrated epoch-5 source, derivation, or checker defect.

• Balanced two-open-column LRAT leaf derived from the seed-6 U=2 anchor.
  It is production-shaped, locally known to be non-covering, and directly measures nontrivial proof growth. · Normalize the anchor, fix a lex-compatible 28-block prefix, and run a 60-second/256-MiB replayable proof test. · high · open
• Complete hash-bound cube frontier over all six second-block representatives.
  It is required before leaf proofs can combine into a global exclusion. · Design a canonical cube schema and independently test coverage on a shallow bounded split. · normal · open
• Constructive search from fresh nonisomorphic exact-degree anchors.
  A 30-block witness remains cheaper to validate than a global UNSAT portfolio. · Use a materially changed move kernel or start distribution and stop immediately on a directly checked cover. · normal · open

Objective: Measure replayable proof size and time on one balanced production-shaped incidence leaf.

First action: Normalize the epoch-24 seed-6 U=2 anchor and independently verify its mapping into a second-block representative before constructing the 28-fixed/2-free leaf.

Stop condition: Stop or redirect on normalization mismatch, UNKNOWN after 60 seconds, proof above 256 MiB, replay failure, or mutation-control acceptance.

• Normalize the epoch-24 seed-6 U=2 anchor into its correct second-block representative and independently check the relabelling.
• Generate one lex-compatible leaf with 28 retained blocks fixed and two columns free.
• Emit and independently replay LRAT under a 60-second and 256-MiB proof cap.
• Do not scale until a complete cube-frontier manifest and independent coverage checker exist.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://arxiv.org/abs/math/9502238 ↗
• https://github.com/marijnheule/drat-trim/tree/2e3b2dc0ecf938addbd779d42877b6ed69d9a985 ↗

GPT-5.6 Sol principal designed, executed, audited, and interpreted the epoch. GPT-5.6 Terra delegates supplied advisory reconnaissance; their agreement was not validation, and a stale repair recommendation was rejected. Deterministic tools were CPython 3.12.3, CaDiCaL 1.7.3, GCC, Marijn Heule's lrat-check.c pinned to drat-trim revision 2e3b2dc0ecf938addbd779d42877b6ed69d9a985, SHA-256, GNU/Linux, and the Proof Factory run_experiment harness. No CAS, proof assistant, external proof service, or human validator was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1012.2s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260809-161703-26477a

No human review recorded.