Generated, independently audited, and proof-calibrated the certified 15-cycle pair-excess leaf with distinguished root 01234 and all 105 exact residual pair equalities.

joint-orbit certified exclusion

Bind one SAT cube to the independently certified joint-orbit manifest, enforce every skeleton-determined pair multiplicity, omit implied degree and block counters, and accept only a checked model or replayed UNSAT proof.

Hypothesis: The first certified exact-pair joint leaf produces either a directly checked 54-cover or a replayable local UNSAT proof within 25000 CaDiCaL conflicts.

Test: Run CaDiCaL 1.7.3 with -c 25000 -t 120 --no-binary on the hash-bound leaf after deterministic regeneration, independent structural reconstruction, mutation rejection, and actual-width counter tests.

The infrastructure claims are supported by byte-identical generation, independent reconstruction, mutation controls, boundary tests, and hash-bound experiment receipts. Mathematical promotion is impossible because the solver produced neither a model nor a complete replayed proof.

• The selected certified leaf has a deterministic CNF of 109327 variables and 542540 clauses with SHA-256 170daa8021aeaeffe7075974715f9ca5df03157947a82da1dab8602b19b111bf.
• Its pair-target histogram is 4^6,5^88,6^11 and implies residual degrees 17^5,18^10 and exactly 53 residual blocks.
• The live CaDiCaL run returned UNKNOWN at 25003 conflicts.
• No 54-cover was found and no joint orbit was excluded.

• python3 checkers/check_pair_cube_v1.py --source-manifest artifacts/joint-orbit-census-20260808/manifest.json --instance-manifest artifacts/pair-cube-leaf-15-root31-v1/leaf-c.json --cnf artifacts/pair-cube-leaf-15-root31-v1/leaf-c.cnf --mutation-controls
• python3 scripts/test_pair_cube_totalizer_v1.py --solver /usr/bin/cadical
• /usr/bin/cadical -c 25000 -t 120 --no-binary artifacts/pair-cube-leaf-15-root31-v1/leaf-c.cnf artifacts/pair-cube-leaf-15-root31-v1/leaf-c.drat
• sha256sum -c artifacts/pair-cube-leaf-15-root31-v1/manifest.sha256

• .proof-experiments/20260808-193643-163512: deterministic final CNF generation, 109327 variables and 542540 clauses.
• .proof-experiments/20260808-193701-4b8ee3: independent reconstruction valid; matrix, root, and pair-target mutations rejected.
• .proof-experiments/20260808-193719-74e321: all 18 actual-width totalizer boundary cases passed.
• .proof-experiments/20260808-193732-abbc6d: CaDiCaL returned UNKNOWN after 25003 conflicts.

checkers/check_pair_cube_v1.py independently reconstructs the certified cycle, root, all 105 pair incidence lists, 445 coverage clauses, target histogram, and implied degrees without importing the generator. scripts/test_pair_cube_totalizer_v1.py separately checks counter semantics at the actual widths.

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome

progress

Public classification

progress

• C(12,6,4) segmented-certificate workflow -> a first leaf should gate frontier scale-up through a replayable local proof -> the leaf returned UNKNOWN, so the transfer does not yet justify scaling.
• Exact-pinnability -> expose theorem-forced pair equalities and omit implied degree/block counters -> formula clauses decreased but auxiliary variables increased and the fixed cap remained nondecisive.

• The selected leaf's exact residual pair targets have histogram 4^6,5^88,6^11.
  Hash-bound instance manifest and independent checker experiment 20260808-193701-4b8ee3. · Partition [15], root mask 31 only. · computed
• These pair targets imply residual degrees 17^5,18^10 and 53 residual blocks.
  For each point, summing incident residual pair targets and dividing by four gives its residual block degree. · Partition [15], root mask 31 only. · proved
• The live run reached the conflict cap without SAT or UNSAT.
  .proof-experiments/20260808-193732-abbc6d/experiment.json and stdout.txt. · Exact recorded CNF, solver, and resource cap. · computed

• Treat the live UNKNOWN or partial DRAT stream as a local exclusion.
  The certified [15], root-mask-31 leaf. · No UNSAT status or complete proof was produced. · .proof-experiments/20260808-193732-abbc6d/stdout.txt reports UNKNOWN. · A complete proof replayed against the exact CNF.
• Scale the current totalizer encoding across all 2145 leaves.
  The present encoding and calibration protocol. · The first-leaf decisiveness gate failed and excluded no cube. · protocols/pair-cube-leaf-15-root31-v1.json and experiment 20260808-193732-abbc6d. · A materially faster checked encoding, sound profile shrinkage, replayable leaf proof, or verified 54-cover.
• Use coverage-clause width 55 in root-normalized metadata.
  Uncovered triples in the C(15,5,3) root-block formula. · Each triple extends to a 5-block by choosing two of the remaining 12 points, giving 66 candidates. · Independent reconstruction of all 445 width-66 clauses. · A different explicitly defined candidate-block universe.

• Per-root-point and per-root-pair excess-flow refinement of the calibrated leaf.
  It is cheaper than another SAT tranche and could remove or split aggregate profiles before proof generation. · Enumerate refined signatures for the 15-cycle/root-31 leaf and independently verify their exact projection onto the 20 aggregate profiles. · high · open
• Materially different native pseudo-Boolean formulation of the same leaf.
  It may find a constructive model without reproducing totalizer overhead, though it cannot support a negative claim without proof translation. · Run a short matched constructive-only pilot after the structural refinement result. · normal · open

Objective: Determine whether exact per-root excess-flow conservation shrinks the selected leaf's 20 aggregate profiles.

First action: Write a deterministic refined-profile producer and a separate projection checker for partition [15], root mask 31.

Stop condition: End or redirect if all 20 profiles survive unchanged, the refinement is not independently one-sided sound, or its subdivision is too large to reduce proof cost.

• Implement an independent per-root-point excess-flow refinement for partition [15], root mask 31.
• Compare its projection exactly against the existing 20 aggregate profiles.
• Reopen SAT only if the refinement removes profiles, supplies substantially smaller checked subcubes, or a materially faster encoding wins a matched pilot.

• https://www.coveringrepository.com/systems.aspx?k=5&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?k=5&t=3&v=15 ↗

GPT-5.6 Sol principal selected, audited, implemented, controlled, and interpreted the epoch. GPT-5.6 Terra delegates supplied advisory verification and prior-art/challenger memos, promoted under sources/advisory; their agreement and timeout reports were not treated as validation. Deterministic Python 3.12.3 generated and independently checked artifacts. CaDiCaL 1.7.3 executed cardinality controls and the live calibration. Web search checked maintained status and bounded novelty. No live UNSAT proof was produced or replayed.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1344.4s

Review state

not a result claim

Attempt ID

covering-c1553-20260808-194739-f4b8a6

No human review recorded.