Matched, CPU-pinned CaDiCaL 1.7.3 -P0 versus -P1 proof-compression qualification on the already certified rank-1 profile CNF, followed by independent CNF reconstruction and dual LRAT replay controls.

proof-producing incidence/PB cube decomposition

Use one initial preprocessing round to try to reduce independently replayable LRAT size before applying the encoding to an unresolved profile.

Hypothesis: On the retained certified rank-1 profile CNF, -P1 emits a complete dual-replayable LRAT at least 20% smaller than the retained 12,289,324-byte proof, with no process-time regression relative to fresh -P0.

Test: Run fresh seed-0 -P0 and -P1 processes on one pinned CPU with 75-second solver, 90-second wall, and 16 MiB proof caps; require complete dual replay, at most 9,831,459 bytes for -P1, and -P1 process time no greater than -P0.

The passing threshold was 9,831,459 bytes and no more than 50.47 process seconds. The -P1 prefix had already reached 16,801,792 bytes and 62.38 seconds. Because proof files append and terminal continuation consumes more time, neither gate can recover. Independent replayers rejected the incomplete prefix.

• Fresh -P0 reproduced the retained 12,289,324-byte LRAT byte-for-byte and the proof passed two independent replay implementations.
• Under the frozen protocol, -P1 cannot meet either the proof-size or process-time gate on this exact CNF.
• No covering-number bound changed; 30 <= C(15,6,3) <= 31 remains the maintained range.

• python3 scripts/run_r1_preprocess_proof_gate_v1.py --design artifacts/epoch67-20260810/proof-preprocess-efficiency-design.json --output-dir artifacts/epoch67-20260810/proof-preprocess-gate-v1 --result artifacts/epoch67-20260810/proof-preprocess-gate-primary.json
• python3 checkers/check_r1_preprocess_proof_gate_v1.py --design artifacts/epoch67-20260810/proof-preprocess-efficiency-design.json --result artifacts/epoch67-20260810/proof-preprocess-gate-primary.json --receipt artifacts/epoch67-20260810/proof-preprocess-gate-checker-v3.json
• sha256sum -c artifacts/epoch67-20260810/SHA256SUMS

• .proof-experiments/20260810-221217-fcfcbd: fresh -P0 completed; -P1 crossed the 16 MiB cap and was terminated.
• .proof-experiments/20260810-221434-46d545: preserved infrastructure negative control showing oversized CakeLPR memory settings fail under the harness cap.
• .proof-experiments/20260810-221546-5c34ab: corrected replay settings validated retained and -P0 controls and fail-closed the cap-hit arm.
• .proof-experiments/20260810-221702-9d8a52: final audit additionally dual-rejected the incomplete -P1 prefix and evaluated both gates as irreversibly failed.

checkers/check_r1_preprocess_proof_gate_v1.py independently parses dimensions and logs, reruns the retained profile-CNF reconstruction, freshly builds lrat-check and CakeLPR, checks exact command settings and hashes, validates intact/final-line-deletion controls, and rejects the incomplete -P1 prefix.

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

• Proof-complexity engineering -> initial simplification can enlarge externally checkable derivation traces even when it reduces the active SAT formula -> observed -P1 prefix exceeded the complete -P0 proof by 36.72% before termination.

• Fresh -P0 generated exactly the retained rank-1 LRAT.
  Both files have 12,289,324 bytes and SHA-256 793a68d3827c8ac664b2a1d79c313e849f7e379bb980e2fc9dc3e451180a7c1f; both fresh replayers accepted it. · The hash-bound rank-1 profile CNF and recorded CaDiCaL 1.7.3 options. · computed
• The -P1 arm failed both frozen method gates before termination.
  16,801,792-byte incomplete prefix versus 9,831,459-byte maximum; 62.38 process seconds versus terminal -P0 at 50.47. · The matched seed-0, CPU-0, ASCII external-LRAT protocol. · computed
• The -P1 prefix is not an UNSAT certificate.
  Fresh lrat-check returned NOT VERIFIED and CakeLPR reported a parse failure at line 219,592. · The exact 16,801,792-byte prefix with SHA-256 3fb176be7dc3dcf1312dfdae05089b8c932008afd591526029ddebec4d2bb537. · computed

• Scale the exact CaDiCaL 1.7.3 -P1 preprocessing mechanism to an unresolved profile under the frozen proof-compression gate.
  Current incidence/profile encoding, seed 0, external ASCII LRAT, and the recorded common solver options. · Both proof-size and process-time gates became irreversibly false before termination. · artifacts/epoch67-20260810/proof-preprocess-gate-checker-v3.json · A changed proof emitter or format, independently validated proof-prefix reuse, or a matched test meeting both the <=0.8 size ratio and no-process-regression requirements.
• Treat the cut -P1 trace as an UNSAT certificate.
  The exact recorded prefix. · It ends mid-line and both independent replayers reject it. · artifacts/epoch67-20260810/proof-preprocess-gate-checker-v3.json · A complete proof trace accepted by both independently built replayers.

• Binary-LRAT proof-format qualification
  It targets certificate storage without changing the proven CNF semantics or solver search, but is acceptable only with two independent validation paths. · Audit pinned binary-LRAT support and run a tiny intentional-contradiction intact/truncation control if an independent verifier or deterministic translator exists. · high · open
• Canonical root-link catalogue with a hash-bound completeness frontier
  Fixing a 12-block root link materially reduces completion variables, but previous bounded pilots lacked a complete orbit frontier. · Audit the retained root-link frontier and identify the first uncovered canonical orbit without repeating the closed 10,000-node cutoff. · normal · open

Objective: Qualify or kill binary LRAT as a compact, independently checkable proof-storage route.

First action: Inspect the pinned CaDiCaL and CakeLPR sources and project-scoped tools for binary-LRAT emission, an independent verifier, or a deterministic binary-to-ASCII translator.

Stop condition: Stop on a missing second validation path, source/hash mismatch, format disagreement, accepted truncation, or no measured storage reduction.

• Audit binary-LRAT support in the pinned CaDiCaL and CakeLPR sources.
• Require a second independent binary verifier or deterministic binary-to-ASCII translator before running any binary proof comparison.
• If the tiny format control passes, run one matched rank-1 binary-size calibration; otherwise redirect away from proof-format compression.
• Do not rerun exact -P1 with a larger cap.

• https://ljcr.dmgordon.org/cover/show_cover.php?v=15&k=6&t=3 ↗
• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://arxiv.org/abs/math/9502238 ↗
• https://github.com/arminbiere/cadical/blob/master/src/cadical.cpp ↗
• https://github.com/marijnheule/coch-demo ↗

GPT-5.6 Sol served as principal investigator and audited, designed, implemented, executed, and interpreted the epoch. GPT-5.6 Terra delegates supplied advisory challenger and verification memos; their statements were not treated as evidence, and the duplicate r=2 selector suggestion was rejected. Deterministic tools were CPython 3.12.3, CaDiCaL 1.7.3, GCC 13.3.0, lrat-check, CakeLPR, GNU taskset, SHA-256, and the Proof Factory experiment harness. Web access checked the maintained covering table, historical construction source, and primary solver documentation. No CAS, proof assistant beyond CakeLPR's verified checker, cloud lab, external proof service, human validator, or external publication was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1411.9s

Review state

not a result claim

Attempt ID

covering-c1563-20260810-222357-342f3c

No human review recorded.