Correct the impossible seed-6 r=5 production leaf to r=4, canonically normalize all intersection-four anchor pairs, enumerate two-open residual lex-slot leaves, and generate one independently checked LRAT UNSAT certificate.

proof-producing incidence/PB cube decomposition

Normalize an r=4 anchor pair to two fixed incidence columns, propagate exact degree 12 through 26 fixed residual columns, enumerate the two remaining columns, and certify one resulting local leaf by LRAT.

Hypothesis: The canonical seed-6 r=4 two-open-slot leaf is UNSAT and emits at most 64 MiB of replayable LRAT within 60 seconds and 256 MiB.

Test: Reconstruct all 12 r=4 normalizations and 378 slot placements, select the placement with the most lex-compatible exact-degree assignments, then require enumerative zero-cover confirmation, CaDiCaL UNSAT, successful LRAT replay, and rejection after deleting the proof's final line.

The positive claims are supported by deterministic enumeration, a byte-level CNF reconstruction, replayed LRAT, a proof mutation control, three semantic artifact mutations, and a fresh structural audit of the base incidence formulas. The represented family is explicitly local and does not justify a global bound.

• The seed-6 anchor has exactly 12 unordered block pairs of intersection four and no pair of intersection five.
• For the chosen canonical r=4 normalization, the 378 fixed-slot placements contain 4,956 ordered lex-compatible exact-degree assignments and zero covers.
• The columns-2-and-4 leaf is UNSAT; its 15,858,333-byte LRAT proof has SHA-256 9712c8540bae08c2f5bd138f0dec19f148c8dee11e8a6558c520d5ac8d63b343 and replays successfully.
• No claim about all two-block replacements or the global nonexistence of a 30-cover follows.

• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py ... python3 scripts/r4_two_open_leaf_v1.py --out-dir artifacts/epoch29-20260809/r4-two-open-leaf-v1
• python3 checkers/check_r4_two_open_leaf_v1.py --artifact-dir artifacts/epoch29-20260809/r4-two-open-leaf-v1 --receipt artifacts/epoch29-20260809/r4_two_open_leaf_checker_receipt.json
• python3 checkers/test_r4_two_open_leaf_fail_closed_v1.py --artifact-dir artifacts/epoch29-20260809/r4-two-open-leaf-v1 --checker checkers/check_r4_two_open_leaf_v1.py --receipt artifacts/epoch29-20260809/r4_two_open_leaf_fail_closed_receipt.json
• python3 checkers/check_incidence_orbit_pilot_v1.py --inputs artifacts/epoch9-20260808/incidence_orbit_inputs_v1.json --manifest artifacts/epoch9-20260808/incidence-orbit-pilot-v1/run-manifest.json --receipt artifacts/epoch29-20260809/incidence_orbit_structural_recheck_receipt.json --structural-only
• artifacts/epoch29-20260809/hash_manifest.json validated 25 recorded hashes

• .proof-experiments/20260809-172953-adab0a: generator and proof run; UNSAT in 8.10 seconds, 15,858,333-byte LRAT.
• .proof-experiments/20260809-173233-45578b: revised independent checker; 12 normalizations, 378 placements, 4,956 assignments, zero covers.
• .proof-experiments/20260809-173250-095494: three semantic corruption controls rejected.
• .proof-experiments/20260809-173451-170d19: fresh structural audit of all six second-block incidence formulas passed.

checkers/check_r4_two_open_leaf_v1.py is a separate integer-bitmask reconstruction that enumerates the local mathematical family and checks the CNF suffix. It independently establishes the local zero-cover result. LRAT was freshly replayed from the pinned lrat-check.c source, but this is not checker diversity; CakeLPR remains required before global promotion.

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

• C(12,6,4) dual-checker exhaustive certificates -> predict that a normalized incidence leaf can provide a tractable proof-pipeline calibration -> the r=4 leaf emitted and replayed LRAT, but its 15.9 MB size and missing CakeLPR replay block global scale.

• Every point of a hypothetical 30-block cover occurs in exactly 12 blocks.
  The slack-zero identity 6*30 = 15*12 together with the sourced minimum point degree. · Any 30-block (15,6,3) cover. · proved
• The seed-6 anchor has pair-intersection histogram {1:66,2:195,3:162,4:12}.
  Independent integer-bitmask scan of all 435 block pairs. · The hash-bound seed-6 anchor. · computed
• All 4,956 assignments in the 378 fixed-slot leaves of the selected normalization fail to cover at least one triple.
  Independent exhaustive direct scans of all 455 triples. · Exactly the fixed-slot placement family recorded in the normalization manifest. · computed
• The selected columns-2-and-4 leaf is UNSAT.
  Exhaustive local enumeration plus LRAT SHA-256 9712c8540bae08c2f5bd138f0dec19f148c8dee11e8a6558c520d5ac8d63b343 replayed to the empty clause. · The 33,162-variable, 156,782-clause CNF SHA-256 b5292c8d982c0afea8cde13a4d8a99d812665119ca33c11f39afae5f72e02ceb. · computed

• Normalize the seed-6 anchor using an r=5 block pair.
  All 435 block pairs of the fixed seed-6 anchor. · The maximum observed intersection is four. · Independent histogram {1:66,2:195,3:162,4:12}. · A defect in the hash-bound anchor source or pair-intersection checker.
• A cover exists in any of the 378 recorded fixed-slot leaves.
  All 4,956 ordered lex-compatible assignments represented by those leaves. · Direct exhaustive coverage evaluation found zero covers. · normalization-manifest.json and r4_two_open_leaf_checker_receipt.json. · A concrete checker defect or a represented assignment omitted from the manifest.
• Treat recompilation of lrat-check.c as independent checker diversity.
  Global certificate promotion. · Both replays share the same checker implementation and common-mode risk. · Tool provenance and comparison with the C(12,6,4) dual-checker methodology. · None; use a materially independent verified checker such as CakeLPR.

• CakeLPR certificate-integrity gate.
  It is constant-cost and removes the largest common-mode verification risk before expensive proof production. · Pin the official verified release and replay the two retained CNF/LRAT pairs with intact and truncated proofs. · high · open
• Complete assumption-literal cube frontier.
  A checked disjoint frontier is required to turn local UNSAT leaves into a global exclusion. · Specify a frontier manifest format and test completeness on a tiny synthetic branch set before touching the global formula. · normal · open
• Materially changed constructive search.
  A 30-cover remains cheaper to validate than a global UNSAT proof and deserves symmetric consideration. · Compare a new non-anchor exact-degree start mechanism against the existing U=2 result under a fixed proposal budget and direct cover checker. · normal · open
• C5 rarest-uncovered-triple exact DFS.
  The validated C5 quotient remains unresolved, but generic MILP supplied no telemetry. · Run a node-limited incremental bitset DFS throughput pilot with exact profile bounds. · low · open

Objective: Qualify checker diversity before deciding whether global incidence certificate production has acceptable expected value.

First action: Retrieve the official cake_lpr source from https://github.com/tanyongkiam/cake_lpr at the recorded revision into a project-scoped tool directory, verify source/release hashes, then replay artifacts/epoch27-20260809/r5-lrat-calibration-v2 and artifacts/epoch29-20260809/r4-two-open-leaf-v1.

Stop condition: Stop or redirect on acquisition/hash failure, format incompatibility, intact-proof rejection, mutation acceptance, or a breadth-sample aggregate projection exceeding the declared certificate budget.

• Pin the official verified CakeLPR release at its recorded upstream revision and bind its source and executable hashes.
• Replay the epoch-27 calibration and epoch-29 leaf with CakeLPR; require intact acceptance and final-line-deletion rejection.
• Only after dual-checker qualification, design a disjoint assumption-literal cube-frontier manifest and independently check its completeness.
• Run a small breadth sample and project aggregate proof bytes and replay time before authorizing global scale.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?k=6&t=3&v=15 ↗
• https://arxiv.org/abs/math/9502238 ↗
• https://doi.org/10.1002/jcd.3180030404 ↗
• https://arxiv.org/abs/2607.23766 ↗
• https://github.com/tanyongkiam/cake_lpr ↗

GPT-5.6 Sol acted as principal investigator and independently implemented, executed, audited, and reported the work. GPT-5.6 Terra delegates supplied advisory prior-art and experiment-verification memos; their agreement was not treated as validation, and relied-on advice was promoted with provenance. Python 3.12.3 performed exact enumeration, hashing, and artifact checking. CaDiCaL 1.7.3 emitted the LRAT proof. GCC compiled the pinned drat-trim lrat-check.c source for replay. Web search/retrieval checked current and primary sources. No CAS or proof assistant was used. CakeLPR was absent and remains a required gate.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1102.6s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260809-173913-8f03d3

No human review recorded.