Built an exact 16-cube truth-table partition of the legitimate fixed-first/fixed-second r=2 incidence CNF on DIMACS variables 31-34 and ran a proof-producing, per-leaf-capped discriminator with independent reconstruction and dual LRAT rejection checks.

proof-producing incidence/PB cube decomposition

Append four unit clauses for every assignment to x(0,2), x(1,2), x(2,2), x(3,2), run fresh CPU-pinned CaDiCaL processes with LRAT output, and accept information only after exact frontier reconstruction and independent proof replay.

Hypothesis: The complete four-literal r=2 frontier improves aggregate conflicts per total process second by at least 25% and proof bytes per conflict by at least 10% over a matched 16-second unsplit control, or produces an independently validated terminal leaf, without exceeding 1 MiB per leaf.

Test: Generate all 16 assignments to variables 31-34, independently byte-reconstruct every leaf, then run fresh one-second proof-producing processes until a terminal leaf, verification failure, or predeclared proof-cap breach occurs.

The frontier claim is supported by complete byte reconstruction and mutation controls. The solver claim is limited to five exact recorded processes, their raw outputs, proof files, and independent dual rejection. A predeclared cap breach requires redirect and supplies no mathematical exclusion.

• The 16 assignments to DIMACS variables 31,32,33,34 form an exact, pairwise-disjoint, complete partition of the retained r=2 CNF.
• Under experiment 20260810-181912-7bebef, cubes 0-4 all returned UNKNOWN and cube 4 emitted 1052672 proof bytes, exceeding the 1048576-byte cap.
• Fresh lrat-check and CakeLPR builds rejected every one of the five sampled incomplete prefixes.
• No 30-block cover was found, no legitimate case was excluded, and the maintained range remains 30 <= C(15,6,3) <= 31.

• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py ... -- /usr/bin/python3 scripts/r2_prefix_frontier_v1.py --out-dir artifacts/epoch61-20260810/r2-prefix-frontier-cap-stop-v1; experiment 20260810-181912-7bebef.
• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py ... -- /usr/bin/python3 checkers/check_r2_prefix_frontier_v1.py --receipt artifacts/epoch61-20260810/r2-prefix-frontier-cap-stop-v1/frontier-receipt.json --out artifacts/epoch61-20260810/r2-prefix-frontier-cap-stop-v1/independent-check.json; experiment 20260810-181947-db6b0a.
• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py ... -- /usr/bin/python3 checkers/test_r2_prefix_frontier_fail_closed_v1.py --receipt artifacts/epoch61-20260810/r2-prefix-frontier-cap-stop-v1/frontier-receipt.json --out artifacts/epoch61-20260810/r2-prefix-frontier-cap-stop-v1/fail-closed-controls.json; experiment 20260810-182004-15924a.
• sha256sum -c artifacts/epoch61-20260810/SHA256SUMS returned OK for every listed packet file.

• 20260810-181623-798279: failed preflight found the cube-04 cap breach but aborted because the CakeLPR rejection classifier did not recognize its failed-to-parse diagnostic.
• 20260810-181912-7bebef: corrected fail-closed run produced the exact frontier receipt and redirected at cube-04-proof-cap.
• 20260810-181947-db6b0a: independent reconstruction, metric audit, fresh proof qualification, and five dual UNKNOWN replays passed.
• 20260810-182004-15924a: omitted, duplicate, flipped-sign, changed-header, and body-mutation packets were all rejected.

checkers/check_r2_prefix_frontier_v1.py independently regenerated all truth-table rows and DIMACS leaves, reparsed logs and gate arithmetic, rebuilt lrat-check and CakeLPR, qualified both with an intact proof and final-line deletion, and dual-rejected all five sampled prefixes.

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) proof pipeline -> predict fresh lrat-check and CakeLPR will distinguish complete proofs from incomplete prefixes -> both rejected all five legitimate UNKNOWN prefixes.
• Cube-and-conquer -> predict a four-variable truth-table split provides a safe complete frontier -> independent reconstruction proved exact disjoint coverage, but proof volume rejected scale-up.
• Fail-closed mutation testing -> predict packet-level corruption should be detected before scientific interpretation -> all five structural mutations were rejected.

• The retained r=2 formula admits the exact 16-row partition on variables 31-34.
  frontier-receipt.json plus independent-check.json and five mutation controls · The CNF with SHA-256 3a1599307c24d515daf2e2ba7c3dfa04d7d20eac610e6eb92c68114c3174bed2 · computed
• The corrected frozen protocol sampled five distinct fresh processes, all UNKNOWN, before cube 4 crossed the declared proof cap.
  Experiment 20260810-181912-7bebef and independent metric/proof audit · CaDiCaL 1.7.3, seed 0, CPU 0, one-second solver limits, LRAT enabled, exact recorded host · computed
• Every sampled UNKNOWN proof prefix is rejected by both fresh replayers.
  independent-check.json proof_audit · The five exact prefix files from cubes 0-4 · computed

• Scale the exact four-literal one-second LRAT frontier under a 1 MiB per-leaf cap.
  The retained r=2 formula, variables 31-34, CaDiCaL 1.7.3 seed 0, fresh processes, LRAT and internal proof checking enabled. · Cube 4 exceeded the cap before any terminal result or matched control, triggering the declared redirect condition. · frontier-receipt.json, independent-check.json, and cube-04.lrat size 1052672 bytes · A material proof-output change—compression, independently mapped preprocessing, reusable proof prefixes, or a different encoding—must pass a legitimate sub-1-MiB preflight.
• Treat UNKNOWN prefixes or the exact cube partition as an exclusion of any covering case.
  All 16 frontier leaves and five sampled solver runs. · A partition alone eliminates nothing, and both proof replayers rejected every sampled prefix. · independent-check.json · A directly validated SAT cover or a complete dual-accepted UNSAT proof for the exact leaf.

• Constructive no-proof reuse of the exact r=2 frontier
  Removing LRAT tracing and proof self-checking directly attacks the measured bottleneck while preserving the smallest terminal certificate: a 30-block cover. · Run sixteen fresh one-second CaDiCaL processes without proof output and one 16-second unsplit control; validate any SAT model with independent Python and C cover checkers. · high · open
• Proof compression or independently mapped preprocessing
  The failed route is blocked by output volume rather than a source or frontier defect. · Identify a pinned transformation that maps a reduced proof back to the raw leaf and qualify it on one legitimate prefix under the existing cap. · normal · open
• Materially different block-selection encoding
  A 5005-block selector or exact-cover formulation avoids column permutation variables and may alter constructive search behavior. · Compile dimensions and run one matched, witness-only preflight against the retained incidence baseline before allocating scale-up compute. · normal · open

Objective: Test whether the exact frontier has constructive value once proof tracing and proof self-checking are removed.

First action: Implement scripts/r2_constructive_frontier_v1.py and run sixteen fresh CPU-pinned CaDiCaL 1.7.3 seed-0 one-second leaves without proof output, interleaved with one fresh 16-second unsplit control.

Stop condition: End or redirect on a source/frontier mismatch, cover-check failure, parsing-dominated leaves, or failure to improve aggregate conflicts/process-second by at least 25%; promote only a directly verified 30-block cover.

• Implement a constructive no-proof matched pilot over the exact 16-cube frontier, with direct Python and C validation of any SAT model.
• Close this coordinate split if constructive cubing fails its throughput gate or parsing dominates the one-second leaves.
• Reopen proof-producing cubing only after a proof-compression, reusable-prefix, preprocessing-proof mapping, or materially different encoding passes a sub-1-MiB legitimate-leaf preflight.

• 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 was the principal investigator. GPT-5.6 Terra delegates supplied advisory prior-art and experiment-design memos only; Sol independently audited every relied-on source, literal, hash, stop condition, and artifact. 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. Web requests to the official URLs returned no page content, so current status was taken from the injected official-current statement and retained same-day audit. 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

1325.0s

Review state

not a result claim

Attempt ID

covering-c1563-20260810-182728-1c6ba7

No human review recorded.