Function solve 

pub fn solve(spec: &PigeonSpec) -> Verdict

Solve PHP(spec.pigeons) with our prover, live: the matching Hall witness (always), the certified Heule symmetry-breaking proof (small/medium n), and a baseline CDCL conflict count for contrast (small n). Every field is a re-verified artifact, never a trusted verdict.