pub fn hall_refutation(e: &ProofExpr) -> Option<HallWitness>Expand description
The full Hall certificate — the matching symmetry invariant in its complete form. A bipartite
cover is infeasible the moment some subset S of items reaches fewer than |S| slots, even when
the totals balance and the crude items > slots bound sees nothing. Returns the violating subset
(re-checked by is_hall_witness), strictly stronger than counting_certificate. This is the
witness behind decide_pigeonhole_unsat’s verdict, surfaced.