🏷️ model-checking

The Proof Form: When a Theorem Is Just Another Port

Adding Lean 4 to pflow-polyglot forced a fifth implementation form — the same reachability check is a startup assertion in five languages and a compile-time theorem in the sixth, and the code is line-for-line equivalent.