Module pigeonhole_viz 

Studio easter egg — the pigeonhole principle, solved live in the browser by our prover.

Pure data → SVG (no Z3, no JS): n pigeons fly toward n-1 holes. One pigeon is always left with nowhere to land — and that is the whole point. Encoded as boolean SAT, PHP(n) needs an exponentially long resolution refutation (Haken 1985), so every resolution-class solver — Kissat, CaDiCaL, Glucose, Z3 — hits a 2^Ω(n) wall. Our prover does not:

• Maximum bipartite matching (logicaffeine_proof::matching) decides infeasibility in polynomial time and returns a re-verified Hall witness — the n pigeons collectively reach only n-1 holes, so no assignment exists. The certificate the animation draws.
• Certified symmetry breaking (logicaffeine_proof::sym_certify::heule_php_refutation) produces a polynomial PR proof (Heule–Kiesl–Biere 2017) that escapes the resolution lower bound and re-checks against the original formula — machine-checked, in the browser, no Z3.

Both run live here. For contrast we also run a plain CDCL solve (the Kissat-class algorithm family) on the small instances and report its conflict count — the search work our certified proof avoids entirely.

Structs

PigeonSpec

A parsed pigeonhole spec: pigeons pigeons into pigeons - 1 holes — the canonical resolution-hard PHP instance, always unsatisfiable.

Verdict

The certified refutation result for one instance, all re-checkable and computed live in WASM.

Functions

is_pigeonhole_spec

Whether spec is a pigeonhole spec — the single source of truth the Studio uses to route Hardware-mode input to this easter egg, so the wiring can never drift from the parser.

parse_pigeonhole_spec

Parse a spec of the form (a single pigeons: N line; comments and blanks ignored):

render

Render PHP(spec.pigeons) as (svg, verdict). The SVG is an animated flight: n pigeons glide into n-1 holes while the one left over flutters and flashes “NO ROOM”. The verdict is the plain-language, certified summary.

report

A textual summary for the Studio output panel, paired with the render animation — the same certified result, in words.

solve

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.