\begin{tabular}{@{}L{4.6cm}L{4.2cm}L{4.6cm}c@{}}
\toprule
statement & human proof & machine-checked input & Lean 4\\
\midrule
P1--P5 (closure, forts, symmetry, SAT encoding, graph facts) & complete, all $n$ & empirical companions only & no\\
P6--P9 (isomorphism, 12-vertex bound, first-force lemma, column deletion) & complete, all $n$ & symbolic identity (sympy); replays $12\le n\le 300$ & no\\
Lemmas 3.1--3.5 (boundary machinery, CNF correctness) & complete, all $n$, $p$ & integer bookkeeping $12\le p\le 30$ & no\\
$Z\ge 12$ for $26\le n\le 154$ & via Lemma 3.4 & 130 DRAT proofs, drat-trim exit 0 & no\\
$Z\ge 12$ for $n>154$ & Lemmas 3.2--3.3 (no computation) & --- & no\\
$Z(P(n,5))$, $11\le n\le 27$ & P3 (orbit reduction) & exhaustive enumeration, two independent programs & no\\
$Z(P(n,5))\ge$ table, $11\le n\le 22$ & Lemma 3.5, P2 & 12 fort-cover DRAT proofs & no\\
upper bounds, all $n$ & P7 & replayed chronologies & no\\
\bottomrule
\end{tabular}