Module counting_principle 

Fast refuter for the modular counting principle Count_q(n): partition an n-element set into blocks of size q. Encoded as: one Boolean per q-subset (block); a coverage clause per element (the incident blocks, at least one chosen); and a disjointness clause for every pair of overlapping blocks. It is unsatisfiable exactly when q ∤ n.

The refutation is a one-line counting argument: coverage + disjointness force each element into EXACTLY one chosen block, and every block covers exactly q elements, so summing over the elements gives n = q · (#chosen blocks) — impossible when q ∤ n. Recognizing the structure and checking n mod q ≠ 0 is O(clauses); the certificate is the triple (n, q, n mod q).

Soundness: the detector fires only when the clauses faithfully form Count_q(n) — every coverage clause’s incident blocks are pairwise disjoint (a full at-most-one clique, so each element is covered at most once), every block covers exactly q elements, and q ∤ n. Then the counting argument makes the formula unsatisfiable. Any deviation returns None; never a false refutation.

Structs

CountingCert

A modular-counting refutation: an n-element set cannot split into blocks of size q because q ∤ n (the remainder is non-zero). Re-checkable in O(1): n % q == remainder != 0.

Functions

counting_certificate

Recover a Count_q(n) core from clauses and refute it by the q ∤ n counting argument, or None if there is no such core. Conservative / fail-closed — see the module docs.

refute_counting

Refute a Count_q(n) core (q ∤ n). true iff a certificate is recovered. Never a false refutation.