pub fn pigeonhole_abstract_refutation(n: usize) -> Option<AbstractRefutation>Expand description
Symmetry-break pigeonhole to its abstract certificate. The rules collapse (via clause_orbits) to
exactly two types regardless of n; the abstract invariant on those types is Hall’s condition,
witnessed by the O(1) counting certificate pigeons > holes. The whole certificate is constant in
size and identical in shape at every scale — the auto-collapse of pigeonhole, lifted to the type
level where it actually scales. None only in the degenerate hole-free case.