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

Manual backfill of a multi-day campaign run in a separate canonical worktree (c1264-canonical-import-v2), not through this box's automated gpt-5.6-sol/terra epoch pipeline. Completed the independent ordinary C(11,5,3) exhaustive classification and the direct-20 residual-family closure, then cross-referenced both against the 47-node frontier ledger.

Progress

The independent ordinary C(11,5,3) exhaustive classification closed: 384/384 fourth-level parents, all 43,319 fifth-level branches, all 42 third-level nodes, and all 5 root leaves reached terminal UNSAT with zero SAT witnesses. A real CNF-reproducibility gap was found during closure and fixed with a new regeneration-plus-replay audit pair. It rests on 3 named, unaudited premises (the blocker argument, encoding faithfulness, and partition exhaustiveness). The direct-20 residual family (the perfect-matching-orbit decomposition of the classified C(11,5,3) cover) also fully closed, 20/20 UNSAT. Cross-referencing three independently audited artifacts confirmed the direct-20 closure's 20 classes align exactly with the prior 9-catalogued / 11-uncatalogued matching-orbit split: 9 of the 20 were already inside the active frontier blocker catalogue, and 0 of the remaining 11 reach either of the two checked hard frontier nodes (s-r0-1, s-r1-15). No frontier ledger node closes yet from this route; reachability against the other 12 open frontier nodes is unchecked. The global ledger remains 33/47 and the maintained bound remains 40 <= C(12,6,4) <= 41.

Strategy and discriminator

Legacy attempt

Manual backfill of a multi-day campaign run in a separate canonical worktree (c1264-canonical-import-v2), not through this box's automated gpt-5.6-sol/terra epoch pipeline. Completed the independent ordinary C(11,5,3) exhaustive classification and the direct-20 residual-family closure, then cross-referenced both against the 47-node frontier ledger.

Hypothesis: Not recorded.

Test: Not recorded.

Rationale

Both closures replay independently (fresh regeneration plus DRAT-trim replay for the classification; independent audit for the direct-20 family) and the class-index alignment against the matching-orbit split was verified artifact-to-artifact rather than assumed. This is a negative finding (no new frontier closure) reached through positive, verified work, not a guess.

Claims requiring scrutiny
  • The independent ordinary C(11,5,3) exhaustive classification is closed under 3 named premises.
  • The direct-20 residual family is fully closed (20/20 UNSAT).
  • The direct-20 closure's classes align exactly with the existing 9-catalogued/11-new matching-orbit split; 0 of the 11 new classes reach the 2 checked hard frontier nodes.
  • 12 of the 47 frontier ledger nodes remain unchecked against the 11 new classes; no exact-value claim follows from this entry.
Evidence and scope
  • Independent artifact cross-reference across three audited files in the canonical worktree: the literature/matching-split file, its independent audit, and the direct-20 full-closure summary (class_index-to-tranche alignment matches the catalogued/missing partition exactly).
  • Full detail and hashes are recorded in the wiki (projects/covering-c1264.md, 2026-07-24 headline entries) rather than in this box's evidence/ tree, since the closure ran in the separate c1264-canonical-import-v2 worktree, not this host's research/covering-c1264/workspace.
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
progress
Public classification
progress
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
  • Extend the direct-20-to-frontier reachability check to the other 12 open frontier nodes.
  • Merge the canonical worktree's classification-closure and direct-20 artifacts into research/covering-c1264/workspace so future automated epochs can build on them directly.
  • Resume active exclusion/constructive discriminator work on the remaining open frontier nodes.
Tool disclosure

Duration
s
Review state
Attempt ID
covering-c1264-20260724-manual-backfill-classification-closure
Human review ledger

No human review recorded.