Exact covering number C(12,6,4)

Validate the closed 47/47 exclusion with a materially different cardinality encoding and re-derive frontier completeness, rather than search further.

First action: Re-encode a predeclared sample of the closed nodes (including s-r0-2, the hardest) with a totalizer or generalized-totalizer cardinality encoding instead of the sequential counter, solve to UNSAT, and replay every proof with drat-trim.

Stop or redirect when: Stop on any SAT result, any replay failure, or any node whose two encodings disagree; that would falsify the closure and must be reported before anything else runs. Otherwise stop after the declared sample and hand the frontier-completeness re-derivation to a separate pass.

• Bind the committed fifth-level split to the independently validated fourth-level base.
  Run the fifth-level auditor with a fail-closed 384-parent ID/hash cross-check against the new receipt.
• Retain constructive 40-block witness search only for a materially different basin or formulation.
  Semantic-gate an exact optimization or independently sourced new basin before allocating a multi-seed tranche.

• fourth-level receipt plus descendant deficit certification
  Use the certified 384-parent inventory as the domain certificate for the newer fifth-level orbit split, then use deficit partitions only inside descendants whose parent binding is independently verified.
• direct exact optimization witness search
  Use the forced matching and exact pair multiplicities in an independently audited CP-SAT or pseudo-Boolean formulation, returning only directly checked 40-block models.
• descendant certificate-chain audit
  Cross-bind fifth-level and deficit partitions to the immutable 790-row fourth-level receipt, then replay aggregate certificates from leaves upward.
• ordinary C(11,5,3) canonical classification
  Regenerate the normalized covering CNF from triples and exact cardinality, independently reconstruct stabilizers through point-membership cells, bind frozen protocols to unique branch IDs, and replay every claimed UNSAT proof with pinned DRAT-trim.
  Reopen only if: Retry or extend fourth-level solving only after the newer descendant receipts are audited and the exact surviving parent set is recomputed.
• temporary-degree-slack ejection chain
  A targeted one-point exchange covers a missing quadruple, then a degree token traverses a directed four-cycle; only indecomposable endpoints returning to all point degrees 20 are scored.
  Reopen only if: Retry this slack sampler only with a different basin, a materially more informative endpoint selector, or an exhaustive structural result.
• slack-constrained three-block repair
  Combine the audited targeted three-block generator with bounded constraint-violation penalties and mandatory exact-degree endpoint projection.
• exhaustive local-neighborhood classification
  Enumerate all degree-compatible indecomposable three-block trades from the fixed warm start through complete signature buckets and canonicalize resulting families.
• degree-preserving positive local search
  Each proposal targets an uncovered quadruple, removes three selected blocks, and adds three previously unselected blocks with identical aggregate point incidence. Pair-signature buckets derive the final two additions, and moves decomposable into a legal two-block trade are rejected.
  Reopen only if: Retry the blocked exact-degree three-block strategy only after demonstrating a new proposal distribution, basin, exhaustive neighborhood result, or checked temporary-slack projection.
• unspecified
  Headless research pass
• canonical-link plus alternative-cardinality synthesis
  Keep the perfect-matching and C2 wr S5 canonical link decomposition, catalog blockers, and residual checker, but substitute a structurally audited kmtotalizer only for exact link degrees.
• cardinality-encoding portfolio
  Replace only the 11 link-degree sequential counters with kmtotalizer while byte-comparing every other clause and replaying cold CaDiCaL proofs.
• baseline invariant and symmetry audit
  Source verification, incidence double counting, exact matching enumeration, fixed-matching block classification, and a separately implemented bitmask replay
  Reopen only if: Reopen this completed baseline only if the maintained status changes, a cited source contradicts an invariant, or the independent checker disagrees after an environment change.

• A 40-block C(12,6,4) cover, and therefore the lower half of the maintained 40 <= C <= 41 range.
  All 47 nodes are UNSAT with drat-trim-replayed DRAT proofs, byte-identical CNF regeneration, and independent encoding audits; no solve in the campaign ever returned SAT.
  Reopen only if: A defect in the inherited frontier-completeness argument, a defect in the sequential cardinality encoding found by the pending second-encoding route, or any node CNF that fails to regenerate to its pinned hash.
• Use intersection-3-third-00-fourth-031 as an altered-unit rejection control.
  The proof still verifies, establishing a stronger prefix contradiction.
  Reopen only if: A different weakening shown to invalidate that proof
• The legacy fourth-level layer has 416 open branches.
  406 replayed closures leave 384 open; the open set partitions into 32 timeouts and 352 unmeasured branches.
  Reopen only if: A protocol-binding or branch-ID error demonstrated against the receipt
• Scale the unchanged four-exchange temporary-degree-slack token-cycle sampler from the fixed warm start.
  No audited endpoint improved six defects, failing the declared continuation signal.
  Reopen only if: A different basin, materially different endpoint selector, or exhaustive neighborhood classification producing a structural result
• Repeat or scale the unchanged exact-point-degree targeted indecomposable three-block annealer from the six-defect warm start.
  Every seed retained six uncovered quadruples, failing the predeclared continuation signal.
  Reopen only if: A materially different state generator, such as bounded temporary point-degree slack, or an exhaustive direct-neighborhood classification producing a structural result
• Scale the prior Glucose4 incremental-assumption wrapper unchanged.
  Both cold and incremental modes closed 0/10, resource work was not matched, and the wrapper could overshoot limits; this is not evidence against incremental solving in general.
  Reopen only if: A reliably interruptible backend and resource-matched cold/incremental protocol with exact parent-plus-assumption equivalence.
• Scale shallow depth-7 direct cubing unchanged under the prior 10-second leaf policy.
  Only 10/128 leaves closed provisionally, 7.8125%, below the declared continuation threshold, and no leaf proofs were preserved/replayed in that sample.
  Reopen only if: A materially stronger branching/encoding mechanism with a predeclared matched sample and replayed proofs.