Calibrated raw CNF/LRAT proof production across all six fixed-second intersection representatives using intentional degree-13 contradictions, followed by clean-room reconstruction and dual replay.

proof-producing incidence/CNF cube decomposition

Fix the first block, represent the second block by one of six S6 x S9 orbit representatives, append exact unit suffixes contradicting point degree 12, and test proof emission and independent replay on every syntax.

Hypothesis: All six retained fixed-second representative syntaxes emit a complete LRAT for an intentional degree-13 contradiction within five solver seconds and one MiB, with fresh lrat-check and CakeLPR builds accepting each proof and rejecting its final-line deletion.

Test: Append 12 point-0 units to r=0 and 11 to r=1,...,5, run six fresh CPU-pinned CaDiCaL processes, and require dual replay acceptance plus dual final-line-deletion rejection for every leaf.

Every positive infrastructure claim is supported by raw hashed CNFs, complete LRATs, two materially different fresh replayers, exact deletion controls, clean-room DIMACS reconstruction, and an independently rerun orbit audit. Those facts validate the pipeline but not the covering target.

• For each r=0,...,5, the retained raw representative incidence formula plus the declared point-0 unit suffix forcing degree at least 13 has a complete LRAT accepted by fresh lrat-check and CakeLPR builds.
• Both proof checkers reject the exact final-line deletion of every one of the six proofs.
• The six second-block representatives cover all 5004 possible second blocks after fixing the first block, although complete-solution branches can overlap.
• No covering bound changed; 30 <= C(15,6,3) <= 31 remains the maintained range.

• python3 scripts/six_rep_lrat_calibration_v1.py --out-dir artifacts/epoch60-20260810/six-rep-lrat-calibration-v1, captured as experiment 20260810-173313-c3f4fa.
• python3 checkers/check_six_rep_lrat_calibration_v1.py --receipt artifacts/epoch60-20260810/six-rep-lrat-calibration-v1/calibration-receipt.json --out artifacts/epoch60-20260810/six-rep-lrat-calibration-v1/independent-check.json, captured as experiment 20260810-173433-ce6db2.
• python3 checkers/test_six_rep_lrat_calibration_fail_closed_v1.py, captured as experiment 20260810-173614-ea346b.
• sha256sum -c artifacts/epoch60-20260810/SHA256SUMS verified all 85 listed packet files.

• 20260810-173103-a7978a: failed closed before leaf solving because CakeLPR requested more memory than the harness allowed.
• 20260810-173300-faed6d: CakeLPR 64-MiB heap control passed under the 256-MiB harness.
• 20260810-173313-c3f4fa: all six proof-emission and replay calibrations passed.
• 20260810-173354-e9b11e: independent checker failed closed on an out-of-project temporary output path.
• 20260810-173433-ce6db2: corrected clean-room independent checker passed.
• 20260810-173614-ea346b: three additional fail-closed receipt mutations were rejected.

checkers/check_six_rep_lrat_calibration_v1.py uses a separately written DIMACS and fixed-clause reconstruction, reruns the orbit/no-comparator audit, freshly compiles lrat-check and CakeLPR, and independently replays all six proofs and deletions.

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 -> fresh lrat-check plus CakeLPR should catch incomplete proof traces -> all six intact traces were accepted and all deletions rejected.
• Group-action normalization -> second blocks should reduce to six intersection representatives under the fixed-block stabilizer -> exhaustive enumeration mapped all 5004 choices to the declared representatives.
• Bounded verifier resource tuning -> a smaller CakeML heap should preserve semantic replay while respecting the process-tree cap -> the retained complete proof passed with a 64-MiB heap under the 256-MiB harness.

• Every putative 30-block cover has point degree exactly 12.
  The prior slack-zero counting receipt and incidence cancellation: total incidences are 30*6=180=15*12. · Any 30-block (15,6,3) cover. · proved
• The six fixed-second representatives cover all 5004 possible second blocks after fixing F.
  The structural checker enumerated all blocks and constructed an explicit stabilizer image for each. · The fixed-first second-block coordinate; branches may overlap for complete solutions. · computed
• All six intentional degree-13 calibration formulas have complete dual-replayed LRAT proofs below one MiB.
  Calibration receipt bc0be4aecf14c43163fb7de597edb5293ba794bdd9888b80e05e412eb9ae0984 and independent check 5863e65e4842263b963477bcaf029e967632b8307481320c645ff7157c7e71e7. · Only the six deliberately contradictory calibration formulas. · computed

• Treat the six calibration UNSAT proofs as exclusions of legitimate 30-block covers.
  All six epoch-60 leaves. · Each leaf intentionally adds units demanding point degree 13 against exact degree 12. · Independent byte reconstruction and degree arithmetic in independent-check.json. · Never for these leaves; only proofs of legitimate, non-contradictory cubes can support exclusion.
• Run CakeLPR with a 1024-MiB heap under the 256-MiB harness.
  This project harness and current checker binary. · Allocation failed before leaf solving. · Experiment 20260810-173103-a7978a. · A deliberately raised and justified outer memory limit, or a verifier build whose allocation semantics differ.
• Use PB output as a certificate route now.
  Current project-scoped toolchain. · No pinned independent PB proof emitter and replayer were identified. · Epoch-60 toolchain audit and delegate advisory, independently confirmed by the absence of a declared PB certificate pipeline. · A pinned PB proof format, emitter, and independent replay checker passing positive and mutation controls.
• Scale the unchanged global incidence search based on calibration proof sizes.
  The current six representative formulas. · Trivial propagation contradictions do not project proof size or solve time for legitimate hard cubes. · The calibration claim scope and prior UNKNOWN legitimate searches. · A legitimate prefix-frontier pilot passing exact coverage and matched proof-search efficiency gates.

• Legitimate prefix-free incidence frontier inside one representative formula.
  It is the cheapest test of whether cubing changes proof-producing search rather than merely validating syntax. · Generate at most 16 r=2 cubes from a frozen variable order, independently check exact assignment coverage, and run matched one-second LRAT searches. · high · open
• Constructive 30-block witness search after a material encoding or neighborhood change.
  A witness remains the smallest terminal certificate and should receive symmetric consideration. · Identify one encoding change not already rejected by the route ledger, then run a bounded matched witness-search discriminator with direct cover checking. · normal · open
• Pinned PB certificate pipeline.
  Native cardinality reasoning could reduce CNF proof growth if an independently replayable format is available. · Audit official VeriPB-compatible emitter and checker sources and run one retained positive proof plus a mutation. · low · open

Objective: Test whether deterministic cubing materially improves proof-producing search on one legitimate representative formula.

First action: Implement scripts/build_incidence_prefix_frontier_v1.py for r=2 with at most 16 prefix-free cubes and a separate exact-coverage checker.

Stop condition: Stop or redirect on reconstruction failure, frontier size above 16, aggregate proof-cap breach, no 25% conflicts-per-second gain, no 10% proof-bytes-per-conflict gain, or a better verified route.

• Construct an at-most-16-cube prefix-free r=2 frontier from a frozen residual-incidence variable order.
• Write a separate checker proving exact Boolean coverage, raw-CNF suffix construction, and mutation rejection before solving.
• Compare matched one-second LRAT-enabled cube runs against a 16-second unsplit r=2 control.
• Stop unless cubing improves both conflicts per second by at least 25% and proof bytes per conflict by at least 10%, or yields a legitimate dual-replayed UNSAT leaf.

• 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 ↗
• https://github.com/tanyongkiam/cake_lpr ↗

GPT-5.6 Sol served as principal investigator. GPT-5.6 Terra delegates supplied advisory reconnaissance only; Sol independently audited every relied-on claim. Deterministic tools were Python 3.12.3, CaDiCaL 1.7.3, GCC, drat-trim lrat-check.c, CakeLPR, exact DIMACS parsers, SHA-256, and the project experiment harness. No CAS, proof assistant, PB solver/replayer, cloud lab, external proof service, or human validator produced evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1305.3s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260810-174240-1c121b

No human review recorded.