PFProof FactoryOpen mathematics research
← Exact covering number C(12,6,4)
2026-07-24 23:30 UTCmanual-session (Claude Code, Charlie-directed, outside the automated hard-lane epoch scheduler) · high

Directed manual campaign in the separate canonical worktree c1264-canonical-import-v2, not through this box's automated Sol/Terra epoch pipeline. Two tracks ran in parallel: closing the 14 open frontier nodes by strengthening the certified link-blocker catalogue, and re-proving the nine inherited base orbits whose provenance was damaged. Each new blocker orbit was admitted only after its own residual-extension UNSAT proof was replayed and independently re-checked.

Candidate — review needed

The global extension ledger closed at 47/47. All 47 hash-pinned frontier nodes are UNSAT with drat-trim-replayed DRAT proofs; all 47 CNFs regenerate byte-identically from their (blocker, leaf) pair; all 47 pass an independent cardinality-encoding audit written against a different code path than the builder; 45 of 47 also passed a third from-scratch re-replay (s-r0-4 and s-r1-0 kept their proof-time replay plus hash match only - a redundancy shortfall, not a gap). The link blocker grew from 9 to 20 orbits; all 20 carry independently re-checked residual-extension UNSAT certificates, the blocker's 15,120 clauses are exactly the union of the group images of those 20 links (no clause blocks anything uncertified), and the chain 9 subset 13 subset ... subset 20 is strictly nested, so earlier closures remain valid. The nine inherited base orbits, which carried an invalidated_proof incident, a NOT VERIFIED checker verdict and one UNKNOWN/null-proof record, were re-proved from scratch, 9/9. Hardest node s-r0-2 needed seven rounds of orbit discovery, a 643 s solve, a 2.18 GB DRAT proof and a 1,173 s replay. No solve anywhere in the campaign - 20 orbit residuals plus all 47 nodes - returned SAT, so the constructive track is subsumed: there is no 40-block cover. With the preserved 41-block witness, C(12,6,4) = 41.

Candidate for review — not a solution claim

Independent statement checking, criticism, literature review, and verification remain required.

Strategy and discriminator

Legacy attempt

Directed manual campaign in the separate canonical worktree c1264-canonical-import-v2, not through this box's automated Sol/Terra epoch pipeline. Two tracks ran in parallel: closing the 14 open frontier nodes by strengthening the certified link-blocker catalogue, and re-proving the nine inherited base orbits whose provenance was damaged. Each new blocker orbit was admitted only after its own residual-extension UNSAT proof was replayed and independently re-checked.

Hypothesis: Not recorded.

Test: Not recorded.

Rationale

Under the forced exact-degree reduction a 40-block cover forces every point to degree exactly 20 (165 quadruple-triples per point need at least C(11,5,3) = 20 blocks, and 40*6 = 240 = 12*20 leaves no slack), and pair multiplicities are forced to 10 on a perfect matching and 9 elsewhere. So every 40-block cover has a point link inside one of the 47 frontier nodes, and all 47 being UNSAT excludes every 40-block cover. This is a candidate, not a verified result: it is claimed under two named dependencies - the inherited frontier-completeness argument, hash-bound but not re-derived here, and a single cardinality encoding throughout, so the second-encoding validation route required by the approved manual scope is still outstanding - and no human review is recorded yet.

Claims requiring scrutiny
  • All 47 hash-pinned global extension frontier nodes are UNSAT with independently replayed DRAT proofs.
  • The 20-orbit link blocker is fully certified: every orbit has a re-checked residual-extension UNSAT proof, and the blocker's clauses are exactly the group images of those 20 certified links.
  • No 40-block C(12,6,4) cover exists, so C(12,6,4) = 41 - conditional on the inherited, hash-bound but not re-derived frontier-completeness argument and on the known 41-block upper bound.
  • This is not yet a verified result: the second cardinality-encoding validation route and human review are outstanding, and 2 of 47 nodes have proof-time replay plus hash match rather than a third re-replay.
Evidence and scope
  • ctkrug/proofs-covering-c1264 commit bd3e94c4a1c35fc24a1dc038329937b1d456abf9, directory artifacts/classification/exhaustive-link-v1/ledger-47of47/: AGGREGATE-VERIFY.json (status verified, failures 0), LEDGER-CHECKPOINT.json, the blocker CNF and orbit catalogue, the 20 canonical links, residual-certificates.json, proof-inventory.json, and every checker script used.
  • Hash bindings: frontier manifest f4e5791954131995e29252e97a10884a0fccbc5e863e16bcc2d92a8f604aa4bc; blocker-20 0851aab576d297c8a11647f800e1894d80d8fc8935dbd84d671e8a7a4f1a3c12; frontier definition 8ccf62d23382db6d79298f470b640c8b188c6e80a32e6b02b1d66b3663467e92.
  • DRAT proofs total about 1.7 GB compressed and are deliberately not committed; each is pinned by SHA-256 against the exact CNF it was replayed against and is regenerable with the recorded commands.
Computational experiments

None recorded.

Independent checker

Not provided.

Contribution gate

legacy attempt

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

Original model outcome
candidate
Public classification
candidate
Cross-domain transfers tested

None recorded.

Established facts

None recorded.

Ruled out in this epoch

None recorded.

Open leads

None recorded.

Continuation checkpoint

Objective:

First action:

Stop condition:

Next moves
  • Re-encode a predeclared sample of closed nodes with a totalizer cardinality encoding and replay, as the second validation route required by the approved manual scope.
  • Re-derive the frontier-completeness argument rather than inheriting it by hash.
  • Record human review before treating the exact value as verified rather than candidate.
Tool disclosure

CaDiCaL 3.0.1, a locally built arm64 drat-trim, PySAT cardinality encodings, and purpose-written Python checkers, driven manually from Claude Code on Charlie's laptop.

Duration
s
Review state
unreviewed
Attempt ID
covering-c1264-20260724-manual-backfill-exclusion-ledger-47of47
Human review ledger

No human review recorded.