1% Section: Related work2\section{Related work}\label{sec:related}34\paragraph{Zero forcing and minimum rank.} The parameter was introduced by the AIM Minimum Rank -- Special Graphs Work Group \citeyearpar{aim2008zeroforcing} with the inequality $M(G)\le\Z(G)$ and the values for many standard graphs (including $\Z=5$ for the Petersen graph $\PP{5}{2}$). \citet{barioli2010parameters} relate zero forcing to other minimum-rank parameters; the monograph of \citet{hogben2022book} is the standard reference. Propagation time, the number of synchronous rounds needed by a zero-forcing set, is studied by \citet{hogben2012propagation}; we use the trivial bound $2n-|S|$ on the number of rounds to fix the horizon of a round-based SAT encoding. \citet{davila2015girth} give $\Z(G)\ge 2\delta-2$ for graphs of girth at least $5$, which yields only $\Z(\PP{n}{5})\ge 4$.56\paragraph{Generalized Petersen graphs.} The family was named by \citet{watkins1969tait}; its automorphism groups were determined by \citet{frucht1971groups}: for $k^2\not\equiv\pm1\pmod n$ the group is the dihedral group $D_n$ of order $2n$ generated by the rotation $i\mapsto i+1$ and the reflection $i\mapsto -i$, with larger groups when $k^2\equiv\pm1\pmod n$ and in seven sporadic small cases (for $k=5$ and $n\ge 11$ the exceptional orders are $n\in\{12,13,24,26\}$: $5^2\equiv1$ modulo $12$ and $24$, and $5^2\equiv-1$ modulo $13$ and $26$; we confirmed computationally that the layer-swapping map of Proposition~\ref{prop:iso} with $l=\pm5$ is an automorphism exactly for these four $n\le 60$). We only use the dihedral subgroup, which acts for every $n$. \citet{alameda2018families} prove $\Z(\PP{n}{k})\le 2k+2$ and identify generalized Petersen graphs with $M=\Z$; \citet{rashidi2020petersen} give the bound $r(s+2)$ for $n=rk+s$, the value $6$ for $\PP{2k+1}{k}$ with $k\ge 5$, the lower bound $\min\{k,\lfloor n/k\rfloor\}+1$ through a $K_{k,\lfloor n/k\rfloor}$ minor and the Colin de Verdi\`ere parameter, the value $\Z(\PP{n}{2})=6$ for $n\ge 10$ (Theorem~2.5 there, proved by the same figure-based case analysis; \citet{arxiv2607_19412} confirms it by exhaustive search for $10\le n\le 16$ only, so we call it reported rather than established), and a claimed formula for $\PP{n}{3}$ that \citet{arxiv2607_19412} corrected at $n=12$ by exhaustive search. \citet{arxiv2610_24059} prove $\Z(\PP{n}{3})=8$ for $n\ge 13$ and $\Z(\PP{n}{4})=10$ for $n\ge 18$ with a two-lemma method (a bound on the boundary of the sources of the first $p$ forces, and a column-deletion lemma) whose finite residue is discharged by SAT or fort checks, with a Lean~4 formalization for $k=3$; both lemmas are stated for general $k$ but applied only to $k=3,4$. \citet{bjorkman2025leaky} study a fault-tolerant variant and record a $2k+2$ forcing set of a different shape.78\paragraph{Forts and computation.} A \emph{fort} \citep{fast2018degrees} is a non-empty vertex set $F$ such that no vertex outside $F$ has exactly one neighbour in $F$; \citet[Theorem~8]{brimkov2019computational} show that $S$ is a zero-forcing set if and only if $S$ meets every fort, which turns zero forcing into a hitting-set problem; \citet{brimkov2021improved} improve the resulting integer programs and give a SAT-style formulation, and \citet{cameron2023forts} develop fort numbers and fractional zero forcing. We use the fort characterization for one family of certificates (Section~\ref{sec:encodings}).910\paragraph{Certificates and tooling.} Our SAT solving uses PySAT \citep{ignatiev2018pysat} with CaDiCaL~1.9.5 and Glucose~4.1; cardinality constraints are encoded by sequential counters \citep{sinz2005cardinality}; unsatisfiability proofs are logged in DRAT format and verified by \code{drat-trim} \citep{wetzler2014drattrim}, built from source. We attempted no Lean~4 \citep{demoura2021lean4} formalization because the toolchain could not be installed in our execution environment; Appendix~\ref{sec:scope} states the resulting boundary of what is machine-checked.11