1\documentclass{autoscholar}2\usepackage{tikz}3\usepackage{pgfplots}4\pgfplotsset{compat=1.18}5\usetikzlibrary{arrows.meta,calc,backgrounds,positioning}6\graphicspath{{../results/figures/}}7\makeatletter\g@addto@macro{\UrlBreaks}{\UrlOrds}\makeatother % allow line breaks inside file paths89\theoremstyle{plain}10\newtheorem{conjecture}[theorem]{Conjecture}11\theoremstyle{definition}12\newtheorem{observation}[theorem]{Observation}13\newtheorem{compresult}[theorem]{Computational Result}14\newtheorem{question}[theorem]{Question}1516\newcommand{\Z}{\operatorname{Z}}17\newcommand{\cl}{\operatorname{cl}}18\newcommand{\Aut}{\operatorname{Aut}}19\newcommand{\PP}[2]{P(#1,#2)}20\newcommand{\bd}{\partial}21\newcommand{\Fcnf}{\mathcal F}22\newcommand{\Gcnf}{\mathcal G}23\newcommand{\Nmax}{N_{\max}}24\newcommand{\cmax}{c_{\max}}25\newcommand{\code}[1]{\texttt{#1}}2627\title{Sharp Zero-Forcing Bounds for Generalized Petersen Graphs:\\ Computational Discovery and Certified Proofs for $P(n,5)$}28\aswpnumber{AS-WP-2026-0001}29\aswpversion{1}30\aswpdate{2026-10-30}31\keywords{zero forcing; generalized Petersen graphs; minimum rank; forts; SAT certificates; DRAT; computer-assisted proof}32\msccodes{05C50; 05C69; 05C85; 68V15}33\asdiscipline{Mathematics --- combinatorics and algebraic graph theory}3435\begin{document}36\maketitle3738\begin{abstract}39The zero forcing number $\Z(G)$ of a graph is the minimum size of a set of initially black vertices from which the colour-change rule (a black vertex with exactly one white neighbour forces that neighbour black) eventually colours the whole graph; it bounds the maximum nullity of the matrices described by $G$. For the generalized Petersen graphs $\PP{n}{k}$ the sharp values were, to our knowledge, reported for $k=2$ (with independent confirmation only for $n\le 16$), proved for $k=3$ and $k=4$ (2026), and known for $k=5$ only at $n=11$ and at $n\equiv 0\pmod{24}$. We determine $\Z(\PP{n}{5})$ for every $n\ge 11$: the values are $6,8,9,8,8,8,10,10,10,10,10,11$ for $n=11,\dots,22$, and $\Z(\PP{n}{5})=12$ for all $n\ge 23$, so the stabilization threshold is exactly $n_0=23$. The upper bound $12$ is the published $2k+2$ construction. The lower bound for all $n\ge 26$ follows the first-force boundary method of Krishnan, Ma and Zhang, adapted to $k=5$: we prove that the minimum boundary of an $18$-vertex set in $\PP{n}{5}$ is at least $12$ for every $n\ge 26$ by a column-deletion lemma that reduces the statement to the finite window $26\le n\le 154$, which is settled by $129$ unsatisfiability certificates in DRAT format, each verified by the external checker \code{drat-trim} and rebuilt from the graph definition by an independent checker. The method provably fails at $n=25$ for every parameter $p\le 24$ (two inner pentagons give an obstruction), so $n=23,24,25$ and all $n\le 22$ are settled by exhaustive enumeration with dihedral orbit reduction, cross-validated by a second, independently written enumeration based on first-force normalization (through $n=40$) and, for $n\le 23$, by DRAT-certified fort-cover refutations. We also show that the $k=4$ parameter $p=16$ cannot work for $k=5$ at any $n\ge 22$, that the certified bound has zero slack, and that a pre-registered holdout of six values of $n$ confirmed the registered conjectures. All proofs are written out; all certificates, code and a reproduction script are released.40\end{abstract}4142\section{Introduction}\label{sec:intro}4344Zero forcing was introduced by the AIM Minimum Rank -- Special Graphs Work Group \citeyearpar{aim2008zeroforcing} as a combinatorial upper bound on the maximum nullity $M(G)$ of the real symmetric matrices whose off-diagonal pattern is prescribed by a graph $G$: every zero-forcing set $S$ satisfies $M(G)\le |S|$, hence $M(G)\le \Z(G)$, and the inequality is tight for many families \citep{barioli2010parameters,hogben2022book}. Computing $\Z$ is NP-hard in general, and exact values on structured infinite families are usually obtained by pairing an explicit forcing construction with a matching lower-bound argument. Such arguments are delicate: a figure-based case analysis for the generalized Petersen graphs $\PP{n}{3}$ \citep{rashidi2020petersen} was recently shown to fail at $n=12$ \citep{arxiv2607_19412}, and the sharp results for $\PP{n}{3}$ and $\PP{n}{4}$ were only established in 2026 with machine-checked finite cases \citep{arxiv2610_24059}.4546The generalized Petersen graph $\PP{n}{k}$ \citep{watkins1969tait}, for $n>2k$, has vertices $u_0,\dots,u_{n-1}$ (outer cycle) and $v_0,\dots,v_{n-1}$ (inner vertices) and edges $u_iu_{i+1}$, $u_iv_i$ and $v_iv_{i+k}$, indices modulo $n$ (Figure~\ref{fig:anatomy}). For $k=5$ the published information was, to our knowledge, the following: $\Z(\PP{n}{5})\le 12$ for all $n$ \citep{alameda2018families,rashidi2020petersen}; $\Z(\PP{11}{5})=6$ \citep{rashidi2020petersen,arxiv2607_19412}; $\Z(\PP{24r}{5})=12$ for $r\ge1$, attributed to \citet{alameda2018families}; a general lower bound of $6$ for $n\ge 15$ \citep{rashidi2020petersen}; and a handful of better upper bounds at $n=12,13,14,16$. The stabilization threshold and every exact value outside these cases were open, and the 2026 papers list exact values and lower bounds for $k\ge 5$ as open problems.4748\begin{theorem}[main theorem]\label{thm:main}49For $k=5$ and every $n\ge 11$,50\[51\Z(\PP{n}{5})=52\begin{cases}536 & n=11,\\548 & n=12,\\559 & n=13,\\568 & n=14,15,16,\\5710 & n=17,18,19,20,21,\\5811 & n=22,\\5912 & n\ge 23.60\end{cases}61\]62In particular the least $n_0$ with $\Z(\PP{n}{5})=12$ for all $n\ge n_0$ is $n_0=23$.63\end{theorem}6465\paragraph{Contributions.} Beyond the theorem itself, the paper offers the following.66\begin{enumerate}[label=(\roman*)]67\item A complete, self-contained adaptation of the first-force boundary method of \citet{arxiv2610_24059} to $k=5$ (Section~\ref{sec:lower}). The method needs a parameter $p$ (the number of first forces examined); for $k=5$ we prove that the parameter $p=16$ used for $k=4$ fails for every $n\ge 22$ (Proposition~\ref{prop:p16}), that $p=18$ is the smallest parameter that works on the tested range, and that no $p\le 24$ works at $n=25$ (Computational Result~\ref{cr:obstruction}). The finite window left by the deletion lemma, $26\le n\le 154$, is closed by externally checked DRAT certificates.68\item A certified table of exact values for $11\le n\le 48$ in which every entry has an upper-bound witness replayed by an independent program and a lower bound supported by at least one externally checkable or exhaustive argument, with the three-valued status \emph{fully certified / solver-supported / candidate} never collapsed (Section~\ref{sec:results}).69\item A systematic falsification campaign (Section~\ref{sec:robustness}): a pre-registered holdout, a second exhaustive enumeration by a different reduction principle and a different closure algorithm, exhaustive validation of the SAT encodings on small instances, negative controls for the proof checker, stress tests of the deletion lemma, and heuristic attacks on the theorem. Nothing was overturned.70\end{enumerate}7172\paragraph{What is new and what is not.} We state this carefully, because several entries of Theorem~\ref{thm:main} were known. The bound $\Z(\PP{n}{5})\le 12$ is Theorem~2.2 of \citet{alameda2018families} as reported by \citet{rashidi2020petersen}, who prove it as their Theorem~2.2. The value at $n=11$ is Theorem~2.6 of \citet{rashidi2020petersen}, independently confirmed by exhaustive search in \citet{arxiv2607_19412}. The values at $n=14,16$ ($8$) and $n=19,21$ ($10$) are \emph{implied} by the isomorphisms $\PP{14}{5}\cong\PP{14}{3}$, $\PP{16}{5}\cong\PP{16}{3}$, $\PP{19}{5}\cong\PP{19}{4}$, $\PP{21}{5}\cong\PP{21}{4}$ (Proposition~\ref{prop:iso}) together with Theorem~1.1 of \citet{arxiv2610_24059}; they do not appear to have been stated for $k=5$ but we do not claim them. The values at $24\mid n$ are attributed to \citet{alameda2018families}; we could not access that paper's full text in our environment and rely on the statement reported in \citet[Remark~2.4]{rashidi2020petersen}, which our computation confirms at $n=24$ and $n=48$. To our knowledge, the values at $n\in\{12,13,15,17,18,20,22,23\}$, the statement $\Z(\PP{n}{5})=12$ for all $n\ge 23$, and the sharpness of the threshold are new. The proof technique for the lower bound is borrowed from \citet{arxiv2610_24059}; our contribution there is the $k=5$ analysis (the parameter, the obstruction at $n=25$, the finite window and its certificates), not the method.7374\paragraph{Organization.} Section~\ref{sec:related} reviews prior work. Section~\ref{sec:prelim} fixes definitions and proves the foundational facts (order independence of the closure, the fort characterization, symmetry, graph facts, the isomorphism). Section~\ref{sec:upper} proves the upper bounds. Section~\ref{sec:lower} develops the boundary method and proves the correctness of the two SAT encodings used for certificates. Section~\ref{sec:framework} describes the exact-computation framework and its certification vocabulary. Section~\ref{sec:results} assembles the proof of Theorem~\ref{thm:main} and reports the certified table, the obstruction at $n=25$ and the negative results about the method. Section~\ref{sec:robustness} reports the falsification campaign, Section~\ref{sec:discussion} discusses competing explanations and open questions, Section~\ref{sec:limitations} states limitations, and Section~\ref{sec:conclusion} concludes. The appendices contain the remaining proofs, the computational protocol, the reproducibility notes and additional tables.7576\begin{figure}[t]77\centering78\begin{subfigure}[t]{0.47\textwidth}\centering79\includegraphics[width=\linewidth]{fig1_anatomy_P13_5.pdf}80\caption{$\PP{13}{5}$: $\gcd(13,5)=1$, the inner edges form one $13$-cycle.}81\end{subfigure}\hfill82\begin{subfigure}[t]{0.47\textwidth}\centering83\includegraphics[width=\linewidth]{fig1_anatomy_P15_5.pdf}84\caption{$\PP{15}{5}$: $\gcd(15,5)=5$, the inner edges form five triangles.}85\end{subfigure}86\caption{Anatomy of $\PP{n}{5}$: outer cycle $u_iu_{i+1}$ (dark grey), spokes $u_iv_i$ (light grey) and inner chords $v_iv_{i+5}$ (dark grey). The inner subgraph is a union of $\gcd(n,5)$ cycles of length $n/\gcd(n,5)$ (Proposition~\ref{prop:graph}).}87\label{fig:anatomy}88\end{figure}8990\section{Related work}\label{sec:related}9192\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$.9394\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.9596\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}).9798\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.99100\section{Preliminaries}\label{sec:prelim}101102\subsection{Definitions}103104Throughout, graphs are finite, simple and undirected; $N(w)$ is the open neighbourhood of $w$ and, for $X\subseteq V$, $\bd X=\{w\notin X: N(w)\cap X\neq\emptyset\}$ is the (vertex) boundary and $N[X]=X\cup\bd X$.105106\begin{definition}[generalized Petersen graph]\label{def:gp}107For integers $k\ge 1$ and $n>2k$, $\PP{n}{k}$ has vertex set $\{u_i,v_i: i\in\mathbb Z_n\}$ and edge set $\{u_iu_{i+1},\ u_iv_i,\ v_iv_{i+k}: i\in\mathbb Z_n\}$. The pair $\{u_i,v_i\}$ is \emph{column} $i$; $u_i$ lies in the \emph{outer layer} and $v_i$ in the \emph{inner layer}. The rotation $\rho\colon u_i\mapsto u_{i+1},\ v_i\mapsto v_{i+1}$ and the reflection $\sigma\colon u_i\mapsto u_{-i},\ v_i\mapsto v_{-i}$ generate a dihedral group $D_n$ of order $2n$ acting on $V$.108\end{definition}109110\begin{definition}[zero forcing]\label{def:zf}111Let $B\subseteq V$ be the set of black vertices. A black vertex $b$ with exactly one white neighbour $w$ may \emph{force} $w$, written $b\to w$, after which $w$ is black. A \emph{chronology} from $S$ is a sequence of forces, each legal at the colouring produced by its predecessors, starting from $B=S$; it is \emph{maximal} if it cannot be extended. $S$ is a \emph{zero-forcing set} if some maximal chronology from $S$ ends with $B=V$, and $\Z(G)$ is the minimum size of a zero-forcing set.112\end{definition}113114\begin{definition}[forts, boundary minimum]\label{def:fort}115A \emph{fort} of $G$ is a non-empty $F\subseteq V$ such that every $w\notin F$ has $|N(w)\cap F|\neq 1$. For $p\ge1$ let $\beta_p(n)=\min\{|\bd X|: X\subseteq V(\PP{n}{5}),\ |X|=p\}$.116\end{definition}117118\subsection{Order independence and the closure}119120The following standard fact makes Definition~\ref{def:zf} independent of the choice of chronology; we include the proof because the certificates of Section~\ref{sec:framework} depend on replaying one particular chronology.121122\begin{proposition}[order independence]\label{prop:order}123Let $S\subseteq V$. Every maximal chronology from $S$ ends in the same black set $\cl(S)$. Consequently $\cl$ is monotone and idempotent, and $\cl(\varphi S)=\varphi\,\cl(S)$ for every automorphism $\varphi$ of $G$.124\end{proposition}125126\begin{proof}127\emph{Step 1 (monotonicity of the rule).} Let $b\in B\subseteq B'$ and suppose $b$ can force $w$ at $B$, i.e.\ $N(b)\setminus B=\{w\}$. If $w\notin B'$ then $\emptyset\ne N(b)\setminus B'\subseteq N(b)\setminus B=\{w\}$, so $b$ can force $w$ at $B'$.128129\emph{Step 2.} Put $\Phi(B)=B\cup\{w\notin B:\exists b\in B,\ N(b)\setminus B=\{w\}\}$. By Step~1, $B\subseteq B'$ implies $\Phi(B)\subseteq\Phi(B')$. The final set $C$ of a maximal chronology satisfies $\Phi(C)=C$.130131\emph{Step 3.} Let $D\supseteq S$ with $\Phi(D)=D$ and let $S=B_0\subset B_1\subset\dots\subset B_m=C$ be any chronology, $B_{i+1}=B_i\cup\{w_i\}$ with $b_i\to w_i$. By induction $B_i\subseteq D$: if $B_i\subseteq D$ then either $w_i\in D$ or, by Step~1, $b_i\in D$ forces $w_i$ at $D$, contradicting $\Phi(D)=D$.132133\emph{Step 4.} If $C,C'$ are final sets of two maximal chronologies from $S$, both are fixed points of $\Phi$ containing $S$, so Step~3 gives $C\subseteq C'$ and $C'\subseteq C$. Thus $\cl(S)$ is the least fixed point of $\Phi$ above $S$. Monotonicity follows from Step~3, idempotence from $\Phi(\cl S)=\cl S$, and equivariance because an automorphism maps legal forces to legal forces and fixed points to fixed points.134\end{proof}135136\begin{proposition}[fort characterization, {\citealp[Thm.~8]{brimkov2019computational}}]\label{prop:fort}137$S$ is a zero-forcing set of $G$ if and only if $S\cap F\neq\emptyset$ for every fort $F$.138\end{proposition}139140\begin{proof}141($\Rightarrow$) Let $F$ be a fort disjoint from a zero-forcing set $S$ and consider, in a chronology from $S$ that colours $V$, the first force $b\to w$ with $w\in F$. Just before it no vertex of $F$ is black, so $b\notin F$ and all neighbours of $b$ other than $w$ are black, hence outside $F$; thus $|N(b)\cap F|=1$, contradicting the fort property.142($\Leftarrow$) If $\cl(S)\ne V$, let $W=V\setminus\cl(S)$. For $b\in\cl(S)$ the set $N(b)\cap W$ consists of the white neighbours of $b$ at a fixed point, so it has size $\ne1$. Hence $W$ is a fort disjoint from $S$.143\end{proof}144145\begin{proposition}[orbit reduction]\label{prop:orbit}146Let $H\le\Aut(G)$. There is a zero-forcing set of size $s$ if and only if some representative of each $H$-orbit on $s$-subsets is zero forcing. Nothing requires an optimal set to be $H$-invariant.147\end{proposition}148149\begin{proof}150By Proposition~\ref{prop:order}, $\cl(\psi S)=\psi\cl(S)$, so $S$ is zero forcing if and only if $\psi S$ is, and $|\psi S|=|S|$.151\end{proof}152153\subsection{Graph facts and the isomorphism \texorpdfstring{$P(n,k)\cong P(n,l)$}{P(n,k) = P(n,l)}}154155\begin{proposition}\label{prop:graph}156For $n\ge 11$, $\PP{n}{5}$ is simple and cubic with $2n$ vertices and $3n$ edges, connected, its inner subgraph is a disjoint union of $\gcd(n,5)$ cycles of length $n/\gcd(n,5)$, and $D_n$ acts by automorphisms.157\end{proposition}158159\begin{proof}160The three edge families are pairwise disjoint. The outer edges form an $n$-cycle. An inner edge $v_iv_{i+5}$ is a loop iff $5\equiv0$, and $v_iv_{i+5}=v_jv_{j+5}$ with $i\ne j$ iff $10\equiv0\pmod n$; both are excluded by $n\ge 11$. So there are $3n$ distinct edges, every $u_i$ has the three distinct neighbours $u_{i\pm1},v_i$ and every $v_i$ has $v_{i\pm5},u_i$. The outer cycle is connected and every $v_i$ is joined to it by a spoke. The inner subgraph is the Cayley graph of $\mathbb Z_n$ with connection set $\{\pm5\}$; the orbit of $i$ under $i\mapsto i+5$ has $n/\gcd(n,5)\ge 11/5>2$ elements, so each orbit induces a genuine cycle. $\rho$ and $\sigma$ map each edge family to itself.161\end{proof}162163\begin{proposition}[isomorphism]\label{prop:iso}164Let $\gcd(n,k)=1$ and $kl\equiv1\pmod n$. Then $\psi(v_{jk})=u_j$, $\psi(u_{jk})=v_j$ $(j\in\mathbb Z_n)$ is an isomorphism $\PP{n}{k}\to\PP{n}{l}$, and $\PP{n}{l}\cong\PP{n}{n-l}$. For $k=5$ and $n\ge 11$ the partner $l'=\min(l,n-l)$ satisfies $l'\le 4$ exactly when $n\in\{11,14,16,19,21\}$, giving $\PP{11}{5}\cong\PP{11}{2}$, $\PP{14}{5}\cong\PP{14}{3}$, $\PP{16}{5}\cong\PP{16}{3}$, $\PP{19}{5}\cong\PP{19}{4}$ and $\PP{21}{5}\cong\PP{21}{4}$.165\end{proposition}166167\begin{proof}168Since $\gcd(n,k)=1$, $j\mapsto jk$ is a bijection of $\mathbb Z_n$, so $\psi$ is a bijection of the vertex set (swapping layers). Inner edge $v_{jk}v_{(j+1)k}\mapsto u_ju_{j+1}$; spoke $u_{jk}v_{jk}\mapsto v_ju_j$; outer edge $u_{jk}u_{jk+1}$: since $lk\equiv1$, $jk+1=(j+l)k$, so $u_{jk}u_{(j+l)k}\mapsto v_jv_{j+l}$, an inner edge of $\PP{n}{l}$. Thus $\psi$ maps $E(\PP{n}{k})$ injectively into $E(\PP{n}{l})$, and both have $3n$ edges. The map $i\mapsto-i$ on both layers sends $v_iv_{i+l}$ to $v_{-i}v_{-i-l}$, an edge of $\PP{n}{n-l}$. For $k=5$: $5l'\equiv\pm1\pmod n$ with $1\le l'\le4$ means $n\mid 5l'\mp1\in\{4,6,9,11,14,16,19,21\}$, and $n\ge 11$ leaves exactly the listed cases.169\end{proof}170171The isomorphism of Proposition~\ref{prop:iso} is the well-known sufficiency direction of the classification of isomorphisms among generalized Petersen graphs; with \citet[Theorem~1.1]{arxiv2610_24059} ($\Z(\PP{n}{3})=8$ for $n\ge 13$, $\Z(\PP{n}{4})=10$ for $n\ge 18$) it yields $\Z(\PP{14}{5})=\Z(\PP{16}{5})=8$ and $\Z(\PP{19}{5})=\Z(\PP{21}{5})=10$, which we treat as known and use as reference tests.172173\section{Upper bounds}\label{sec:upper}174175\begin{proposition}[the uniform bound $12$]\label{prop:P7}176For every $n\ge 12$ the set $S=\{u_0,\dots,u_{11}\}$ is a zero-forcing set of $\PP{n}{5}$. Hence $\Z(\PP{n}{5})\le 12$ for all $n\ge 11$.177\end{proposition}178179\begin{proof}180For $n=12$, $S$ is the whole outer layer and each $u_i$ forces $v_i$ through its spoke. Let $n\ge 13$.181182\emph{Phase 1.} For $i=1,\dots,10$ perform $u_i\to v_i$: the other neighbours $u_{i-1},u_{i+1}$ of $u_i$ lie in $S$ because $0\le i-1$ and $i+1\le 11$. Then $v_5\to v_0$ ($N(v_5)=\{u_5,v_{10},v_0\}$, the first two black) and $v_6\to v_{11}$ ($N(v_6)=\{u_6,v_1,v_{11}\}$). Now columns $0,\dots,11$ are black and columns $12,\dots,n-1$ white (column $n-1\ne 11$ since $n\ge 13$).183184\emph{Phase 2.} For $j=12,\dots,n-1$ in increasing order perform $u_{j-1}\to u_j$ and then $v_{j-5}\to v_j$. Invariant before stage $j$: columns $<j$ black, columns $\ge j$ white. $N(u_{j-1})=\{u_{j-2},v_{j-1},u_j\}$ with the first two in columns $<j$, so the first force is legal; it leaves $v_j$ as the only white neighbour of $v_{j-5}$, because $N(v_{j-5})=\{u_{j-5},v_{j-10},v_j\}$ and $j-5\ge 7$, $j-10\ge 2$ are columns in $[0,j)$. After stage $n-1$ every vertex is black. For $n=11$ the value $6<12$ is part of Theorem~\ref{thm:main}.185\end{proof}186187This is the $2k+2$ bound of \citet{alameda2018families} and \citet[Theorem~2.2]{rashidi2020petersen}; the column-by-column proof is the $k=4$ argument of \citet{arxiv2610_24059} with the indices adjusted to $k=5$. Figure~\ref{fig:chronology}(a) shows the chronology on $\PP{14}{5}$; it was replayed by an independent program for every $12\le n\le 300$ (Section~\ref{sec:robustness}). For $11\le n\le 22$ the upper bounds in Theorem~\ref{thm:main} are given by explicit sets found by exhaustive search; Table~\ref{tab:witnesses} (Appendix~\ref{app:tables}) lists one minimum zero-forcing set for each $n$ and Figure~\ref{fig:chronology}(b) shows an $8$-vertex set for $\PP{15}{5}$ together with its full chronology. Every stored witness is accompanied by its chronology and was replayed force by force by a checker that shares no code with the solvers.188189\begin{figure}[t]190\centering191\begin{subfigure}[t]{0.48\textwidth}\centering192\includegraphics[width=\linewidth]{fig2a_chronology_P14_5_P7.pdf}193\caption{Proposition~\ref{prop:P7} on $\PP{14}{5}$: $S=\{u_0,\dots,u_{11}\}$, $16$ forces.}194\end{subfigure}\hfill195\begin{subfigure}[t]{0.48\textwidth}\centering196\includegraphics[width=\linewidth]{fig2b_chronology_P15_5_optimal.pdf}197\caption{A minimum zero-forcing set of $\PP{15}{5}$ ($|S|=8=\Z$), $22$ forces.}198\end{subfigure}199\caption{Two independently replayed forcing chronologies. Black vertices form the initial set; each other vertex carries the step at which it was forced; arrows point from the forcing vertex to the forced vertex. Both chronologies were re-validated force by force by the figure generator before drawing.}200\label{fig:chronology}201\end{figure}202203\section{Lower bounds: the first-force boundary method for $k=5$}\label{sec:lower}204205\subsection{The two lemmas}206207\begin{lemma}[first-force boundary lemma, {\citealp[Lemma~2.1]{arxiv2610_24059}}]\label{lem:P8}208If a zero-forcing set $S$ of a finite graph performs at least $p$ forces in some chronology, then the set $X$ of sources of the first $p$ forces satisfies $|X|=p$ and $|\bd X|\le |S|$.209\end{lemma}210211\begin{proof}212A vertex forces at most once: after $b\to w$ all neighbours of $b$ are black and stay black. So the first $p$ forces have $p$ distinct sources and $|X|=p$. Let $B$ be the black set after these forces, $|B|=|S|+p$. Each $b\in X$ had its whole neighbourhood black immediately after it forced, so $N[X]\subseteq B$ and $\bd X\subseteq B\setminus X$, whence $|\bd X|\le |B|-|X|=|S|$.213\end{proof}214215\begin{lemma}[column deletion for $k=5$, after {\citealp[Lemma~2.2]{arxiv2610_24059}}]\label{lem:P9}216Let $n\ge 13$ and $X\subseteq V(\PP{n}{5})$ with no vertex in columns $0,1,\dots,10$. Delete column $5$ and re-index the surviving columns by $f(i)=i$ for $i<5$ and $f(i)=i-1$ for $i>5$, preserving layers. The image $X'\subseteq V(\PP{n-1}{5})$ satisfies $|X'|=|X|$ and $|\bd X'|=|\bd X|$.217\end{lemma}218219\begin{proof}220$f$ is a bijection from the surviving columns onto $\{0,\dots,n-2\}$, hence (with layers) a bijection $V(\PP{n}{5})\setminus\{u_5,v_5\}\to V(\PP{n-1}{5})$; so $|X'|=|X|$. We show $f(N[X])=N[X']$; injectivity then gives $f(\bd X)=\bd X'$.221222Fix an occupied column $i$, so $11\le i\le n-1$, and an offset $d\in\{-5,-1,1,5\}$ (outer vertices use $\pm1$, inner vertices $\pm5$; spokes stay inside a column and are preserved trivially). Put $q=i+d\in[6,n+4]$. If $q<n$, the neighbour column is $q\ne 5$, it survives, and $f(q)=q-1=f(i)+d$ is the corresponding neighbour column in $\PP{n-1}{5}$ (no wrap-around, as $0\le q-1\le n-2$). If $q\ge n$, the neighbour column is $q-n\in\{0,\dots,4\}$, fixed by $f$, and in $\PP{n-1}{5}$ the neighbour of column $f(i)=i-1$ at offset $d$ is $(q-1)\bmod(n-1)=q-n$ because $n-1\le q-1\le n+3<2(n-1)$. Hence no neighbour of $X$ is deleted and $f(N[X])\subseteq N[X']$. Conversely, for an image column $j=f(i)\in[10,n-2]$ and offset $d$: if $j+d\le n-2$ then $j+d\ge 5$ and it lifts to column $j+d+1=i+d$, a neighbour of $i$; if $j+d\ge n-1$ then $(j+d)\bmod(n-1)=j+d-n+1\in\{0,\dots,4\}$ equals $(i+d)\bmod n$, again a neighbour of $i$. So $N[X']\subseteq f(N[X])$.223\end{proof}224225The hypothesis of eleven empty columns is necessary: with only ten, the deleted column can meet $N[X]$ and the boundary size can change (Section~\ref{sec:robustness}, item (d)).226227\subsection{From boundaries to zero forcing and the finite reduction}228229\begin{lemma}\label{lem:31}230Let $p\ge1$ and $n\ge\lceil(p+11)/2\rceil$. If $\beta_p(n)\ge 12$ then $\Z(\PP{n}{5})\ge 12$.231\end{lemma}232233\begin{proof}234Suppose $S$ is zero forcing with $|S|\le 11$. A chronology from $S$ ending at $V$ performs $2n-|S|\ge 2n-11\ge p$ forces. By Lemma~\ref{lem:P8} the sources $X$ of the first $p$ forces satisfy $|X|=p$ and $|\bd X|\le 11$, so $\beta_p(n)\le 11$.235\end{proof}236237\begin{lemma}[finite reduction]\label{lem:32}238Let $p\ge 1$, $\cmax=\lfloor(p+11)/2\rfloor$ and $\Nmax=11\cmax$. If $\beta_p(n)\le 11$ for some $n>\Nmax$, then $\beta_p(m)\le 11$ for every $m$ with $\Nmax\le m\le n$.239\end{lemma}240241\begin{proof}242Let $|X|=p$ and $|\bd X|\le 11$ in $\PP{n}{5}$, $n>\Nmax\ge 13$. Let $C$ be the set of occupied columns and $c=|C|$. A column containing exactly one vertex of $X$ contributes the other vertex of the column to $\bd X$ (through the spoke). Since each column holds at most two vertices of $X$, the number of singly occupied columns is exactly $2c-p$, hence $2c-p\le|\bd X|\le 11$ and $c\le\cmax$. The $c$ occupied columns cut the cyclic sequence of columns into $c$ gaps of empty columns with total length $n-c>11\cmax-c\ge 10c$, so some gap contains at least $11$ consecutive empty columns. Rotating by an automorphism (which preserves $|X|$ and $|\bd X|$) so that these are columns $0,\dots,10$, Lemma~\ref{lem:P9} yields $X'\subseteq V(\PP{n-1}{5})$ with $|X'|=p$ and $|\bd X'|\le 11$. Repeat while $n-1>\Nmax$.243\end{proof}244245\begin{lemma}[what a finite window proves]\label{lem:33}246Let $p\ge 1$ and $n_1\le\Nmax$. If $\beta_p(n)\ge 12$ for every $n_1\le n\le\Nmax$, then $\beta_p(n)\ge 12$ for every $n\ge n_1$, and therefore $\Z(\PP{n}{5})\ge 12$ for every $n\ge\max(n_1,\lceil(p+11)/2\rceil)$.247\end{lemma}248249\begin{proof}250A violation at some $n>\Nmax$ would propagate to $m=\Nmax\ge n_1$ by Lemma~\ref{lem:32}, contradicting the hypothesis. The second statement is Lemma~\ref{lem:31}.251\end{proof}252253For $p=18$ these constants are $\cmax=14$ and $\Nmax=154$, and Lemma~\ref{lem:31} applies for $n\ge 15$; the integer bookkeeping of Lemmas~\ref{lem:31}--\ref{lem:32} was also checked symbolically for $12\le p\le 30$.254255\subsection{Two SAT encodings and their correctness}\label{sec:encodings}256257The lower bounds that are not exhaustive rest on unsatisfiability certificates for the following two families of formulas. The correctness proofs are the link between a verified DRAT proof and a mathematical statement; nothing about the solver is trusted.258259\begin{lemma}[boundary formulas]\label{lem:34}260For fixed $n$ and $p$ let $\Fcnf(n,p)$ be the CNF over variables $x_w,z_w$ ($w\in V$) and auxiliary counter variables with the clauses $(x_w\vee\neg x_t\vee z_w)$ for every edge $tw$ in both orientations, $(\neg z_w\vee\neg x_w)$, a sequential-counter encoding of $\sum_w x_w=p$ and of $\sum_w z_w\le 11$, and the clause $(x_{u_0}\vee x_{v_0})$. Then $\Fcnf(n,p)$ is satisfiable if and only if $\beta_p(n)\le 11$.261\end{lemma}262263\begin{proof}264($\Leftarrow$) Given $X$ with $|X|=p$ and $|\bd X|\le 11$, rotate so that column $0$ is occupied, set $x_w=[w\in X]$, $z_w=[w\in\bd X]$ and extend to the counter variables as the sequential-counter encoding prescribes; the encoding is satisfiable exactly when the cardinality constraint holds \citep{sinz2005cardinality}. The edge clauses hold because $x_t\wedge\neg x_w$ means $w\in\bd X$. ($\Rightarrow$) From a model put $X=\{w:x_w\}$, so $|X|=p$. For $w\in\bd X$ pick $t\in N(w)\cap X$; the clause $(x_w\vee\neg x_t\vee z_w)$ forces $z_w$. Hence $\bd X\subseteq\{w:z_w\}$ and $|\bd X|\le 11$.265\end{proof}266267Thus a verified refutation of $\Fcnf(n,p)$ proves $\beta_p(n)\ge 12$, while a model exhibits a $p$-set of boundary at most $11$, which our driver re-checks by direct counting. We also used $\Fcnf(n,p,b)$ with the bound $11$ replaced by $b$ to compute $\beta_p(n)$ exactly.268269\begin{lemma}[fort-cover formulas]\label{lem:35}270For fixed $n$ and $b<2n$ let $\Gcnf(n,b)$ be the CNF over seed variables $s_w$ with: a sequential-counter encoding of $\sum_w s_w\le b$; four selector variables $c_1,\dots,c_4$ for the directed edges $u_0\to v_0$, $u_0\to u_1$, $v_0\to u_0$, $v_0\to v_5$, with clauses $c_j\to s_{\mathrm{src}}$, $c_j\to\neg s_{\mathrm{tgt}}$, $c_j\to s_{w'}$ for the two other neighbours $w'$ of the source, and $(c_1\vee c_2\vee c_3\vee c_4)$; and one clause $\bigvee_{w\in F}s_w$ for each fort $F$ in a stored list $\mathcal L$. If $\Z(\PP{n}{5})\le b$ then $\Gcnf(n,b)$ is satisfiable; hence a refutation proves $\Z(\PP{n}{5})\ge b+1$.271\end{lemma}272273\begin{proof}274Let $S$ be zero forcing with $|S|\le b<2n$. Since $S\ne V$ there is a first force $x\to y$; at that moment the black set is $S$, so $x\in S$, $y\notin S$ and the two other neighbours of $x$ lie in $S$. The directed edges of $\PP{n}{5}$ fall into four $D_n$-orbits (outer edges in either direction, outward spokes, inward spokes, inner edges in either direction; the reflection reverses the direction within each class), with the four listed representatives. Choose $\varphi\in D_n$ mapping $x\to y$ to a representative; $\varphi S$ is zero forcing of the same size (Proposition~\ref{prop:orbit}) and $\varphi x\to\varphi y$ is a legal first force. Set $s_w=[w\in\varphi S]$ and the matching selector. Every fort clause holds by Proposition~\ref{prop:fort}, and the counter encoding is satisfiable since $|\varphi S|\le b$.275\end{proof}276277The list $\mathcal L$ may contain any forts, in particular all dihedral images of each fort found (automorphisms preserve the fort condition). Our driver generates forts lazily as the white remainders of stalled closures (Proposition~\ref{prop:fort}, direction $\Leftarrow$), shrinks each greedily to a minimal sub-fort while re-verifying the fort property, adds its $D_n$-images, and iterates until the solver reports UNSAT or a model whose seed set is verified to be zero forcing by the closure oracle. The independent checker re-verifies the fort property of every stored set vertex by vertex before accepting a certificate.278279A third, round-based encoding of the forcing process (Appendix~\ref{app:round}) was used as an additional agreement test for small $n$ only.280281\section{Exact computation and certification framework}\label{sec:framework}282283\paragraph{Graph construction.} Two independent constructors (an edge-list formula and a block-circulant adjacency construction) produced identical canonical edge lists for $11\le n\le 48$ and for the Petersen graph $\PP{5}{2}$; each graph was checked for $2n$ vertices, $3n$ edges, all degrees $3$, connectivity, $\gcd(n,5)$ inner cycles, absence of loops and multiple edges, and the $2n$ dihedral maps were verified to be automorphisms. SHA-256 digests of the canonical edge lists are stored with every result record. The order-independence of the closure (Proposition~\ref{prop:order}) was additionally exercised empirically: for $n=11,\dots,16$, $200$ random seed sets each and $20$ random force orders per seed set, the final black set was identical in $1200$ of $1200$ cases.284285\paragraph{Exhaustive oracle (E).} A C program enumerates all $s$-subsets of $V(\PP{n}{5})$ in Gosper order, keeps those that are the lexicographically least bitmask of their $D_n$-orbit (one representative per orbit; sound by Proposition~\ref{prop:orbit}, also at $n=12,13,24,26$ where $D_n$ is a proper subgroup of $\Aut$, since the proposition holds for any subgroup), and computes the closure by bit operations with 16 threads. For each $n$ the sizes $s=1,2,\dots$ are exhausted until a forcing representative appears, so the program certifies both $\Z\le s$ (with a witness) and $\Z>s-1$ (no forcing set of size $s-1$, hence none smaller by monotonicity of $\cl$). The recorded numbers of enumerated subsets and tested representatives were audited afterwards against $\binom{2n}{s}$ and against the Burnside count of $D_n$-orbits on $s$-subsets in all $162$ $(n,s)$ rows, with no mismatch. The oracle was also validated against an unreduced Python enumeration on $\PP{5}{2}$ and $\PP{11}{5}$.286287\paragraph{Second exhaustive path (E$'$).} A second C program, written without reference to the first, uses a different reduction: any zero-forcing set $S$ with $|S|<2n$ has a first force $x\to y$ with $x\in S$, $y\notin S$, $N(x)\setminus\{y\}\subseteq S$, and by the orbit argument in the proof of Lemma~\ref{lem:35} the first force may be taken to be one of four representatives, so it suffices to enumerate the $4\binom{2n-4}{s-3}$ sets containing a fixed closed neighbourhood minus one vertex. It uses a counter/worklist closure instead of pass-based bitmask scanning.288289\paragraph{Certificate paths.} (F) fort-cover refutations of $\Gcnf(n,Z-1)$ with CaDiCaL proof logging, checked by \code{drat-trim}; (B) boundary refutations of $\Fcnf(n,18)$, likewise; (R) the round-based encoding with Glucose, UNSAT without an external certificate. For every DRAT certificate an independent checker rebuilds the CNF from the graph definition, compares the sorted clause multiset byte for byte with the stored DIMACS file, checks the SHA-256 digests of the CNF and of the proof, re-verifies every stored fort, and re-runs \code{drat-trim}, recording the exit code.290291\paragraph{Certification vocabulary.} Fixed before any computation: \emph{fully certified} means the upper witness replays and the lower bound is exhaustive enumeration, an externally checked proof combined with a proved lemma, or a handwritten proof; \emph{solver-supported} means two agreeing solver paths without an external certificate; \emph{candidate} means an upper bound only; \emph{unknown} means a timeout. Timeouts are never interpreted as UNSAT. Table~\ref{tab:paths} shows which paths completed for each $n\le 40$.292293\begin{table}[t]294\centering\footnotesize295\caption{Independent lower-bound paths per $n$. E: exhaustive $D_n$-orbit enumeration; E$'$: exhaustive first-force enumeration (second program); F: fort-cover refutation with a \code{drat-trim}-verified DRAT proof; R: round-based SAT encoding (Glucose, no external proof); B: boundary refutation $\Fcnf(n,18)$ with a verified DRAT proof, which gives $\Z\ge 12$ through Lemma~\ref{lem:31}. ``(s)'': UNSAT reported by the solver without a proof log (solver-supported only); ``t/o'': timed out ($600$\,s); ``$\times$'': the method provably fails at this $n$ (Computational Result~\ref{cr:obstruction}); ``--'': not run. No two completed paths ever disagreed.}296\label{tab:paths}297\input{../results/tables/tab_paths.tex}298\end{table}299300\section{Results}\label{sec:results}301302\subsection{Exhaustive values for $11\le n\le 27$}303304\begin{compresult}\label{cr:exhaustive}305For $11\le n\le 27$ the exhaustive oracle found no zero-forcing set of size $Z-1$ and a zero-forcing set of size $Z$, with $Z$ as in Theorem~\ref{thm:main} (for $n\ge 23$ the witness is Proposition~\ref{prop:P7}). In total 432,226,268,255 subsets were enumerated in 4,125.7\,s of wall-clock time; the largest single instance was $n=27$, $s=11$, with $95{,}722{,}852{,}680$ subsets and $1{,}772{,}711{,}200$ orbit representatives. The second program reproduced all twelve values for $11\le n\le 22$ (no forcing set at $Z-1$, forcing sets at $Z$) and re-established $\Z\ge 12$ for every $23\le n\le 40$, testing 344,080,112,924 sets in 2,345.7\,s.306\end{compresult}307308Table~\ref{tab:bruteforce} lists the enumeration at size $Z-1$ for every $n$, Figure~\ref{fig:scaling}(b) shows its cost, and Table~\ref{tab:witnesses} in Appendix~\ref{app:tables} gives a minimum witness for each $n\le 22$. Three features of the small-$n$ values deserve comment. The sequence is not monotone: $\Z(\PP{13}{5})=9>8=\Z(\PP{14}{5})$ and $\Z(\PP{16}{5})=8<10=\Z(\PP{17}{5})$. The values at $n=14,16$ and $n=19,21$ coincide with $2\cdot3+2$ and $2\cdot4+2$, exactly as Proposition~\ref{prop:iso} predicts, and the intermediate values at $n=15$ ($8$) and $n=20$ ($10$) fit the same plateaus although no isomorphism to a smaller $k$ is available there ($\gcd(n,5)=5$). Finally, the bounds $r(s+2)$ of \citet[Theorem~2.1]{rashidi2020petersen} are attained only at $n=12$ ($8$); at $n=13$ the true value $9$ is below the bound $10$, and at $n=14,16$ the bounds $11$ and $9$ are not sharp.309310\begin{table}[t]311\centering\footnotesize312\caption{Exhaustive enumeration at the critical size $s=Z-1$ (no zero-forcing set exists) for $11\le n\le 27$: number of $s$-subsets, number of $D_n$-orbit representatives actually tested, wall-clock time (16 threads), the number of sets tested by the second program (first-force normalization, $4\binom{2n-4}{s-3}$), and the number of forcing orbit representatives found at size $Z$ (for $n\ge 25$ the size-$Z$ pass was not run because Proposition~\ref{prop:P7} supplies the witness). For $n=27$ sizes $s\le 3$ were not run separately; this is immaterial since a smaller forcing set would extend to one of size $Z-1$.}313\label{tab:bruteforce}314\input{../results/tables/tab_brute_force.tex}315\end{table}316317\subsection{Choosing the parameter: the boundary table and the obstruction at $n=25$}318319\begin{compresult}\label{cr:boundary}320For $12\le p\le 24$ and $13\le n\le 30$ the exact value of $\beta_p(n)$ was computed whenever it is at most $11$, and the formula $\Fcnf(n,p)$ was refuted (certificate kept) otherwise ($234$ cells; Figure~\ref{fig:heatmap}, Table~\ref{tab:boundarytable}). The smallest $p$ with $\beta_p(n)\ge 12$ for all $n\in\{24\}\cup\{26,\dots,30\}$ is $p=18$; $p=24$ still fails at $n=26$. Every $p\le 24$ fails at $n=25$.321\end{compresult}322323\begin{compresult}[obstruction at $n=25$]\label{cr:obstruction}324In $\PP{25}{5}$ the $18$-set $X=\{v_i: i\equiv 0,1\pmod 5\}\cup\{u_i: i\equiv 0,1\pmod 5,\ i\ne 0,21\}$ (two complete inner pentagons and eight outer vertices) has boundary $\{u_0,u_2,u_4,u_7,u_9,u_{12},u_{14},u_{17},u_{19},u_{21}\}$ of size $10$ (Figure~\ref{fig:obstruction}); for $p=20$ the three inner pentagons $\{v_i:i\equiv0,1,2\pmod 5\}$ together with $u_1,u_6,u_{11},u_{16},u_{21}$ have boundary $10$ as well. Hence $\beta_p(25)\le 10$ for $p=18,20$, and the archived obstructions show $\beta_p(25)\le 11$ for every $12\le p\le 24$.325\end{compresult}326327The obstruction is specific to $k=5$: the inner subgraph of $\PP{n}{5}$ contains pentagons only when $n=25$ (for $n\ge 26$ the inner cycles have length $n/\gcd(n,5)\ge 6$ by Proposition~\ref{prop:graph}), and a full inner pentagon has no inner boundary at all, so two pentagons plus well-chosen outer vertices spend only $10$ boundary vertices. Whether some $p>24$ certifies $n=25$ was not tested; it is irrelevant to Theorem~\ref{thm:main}, because $n=25$ is settled by enumeration, but it shows that a purely boundary-based proof of the full theorem would need either a larger $p$ or a different lemma. In contrast, for $k=4$ the parameter $p=16$ certified every $n$ from the threshold on \citep{arxiv2610_24059}. That parameter is useless for $k=5$:328329\begin{proposition}\label{prop:p16}330$\beta_{16}(n)\le 11$ for every $n\ge 22$. Consequently the first-force method with $p=16$ cannot prove $\Z(\PP{n}{5})\ge 12$ for any $n\ge 22$.331\end{proposition}332333\begin{proof}334There is a $16$-set $X_{22}\subseteq V(\PP{22}{5})$ with $|\bd X_{22}|=11$ whose columns $0,\dots,9$ are empty; it was found as a model of $\Fcnf(22,16)$ augmented by the ten emptiness clauses and its boundary was recounted directly (Section~\ref{sec:robustness}, item (d)). Insert a new empty column at position $5$: this produces a $16$-set $X_{23}\subseteq V(\PP{23}{5})$ whose columns $0,\dots,10$ are empty, and Lemma~\ref{lem:P9} applied to $X_{23}$ returns exactly $X_{22}$ with the same boundary size; therefore $|\bd X_{23}|=|\bd X_{22}|=11$. Repeating the insertion gives, for every $n\ge 22$, a $16$-set of boundary $11$ in $\PP{n}{5}$. The second statement follows from Lemma~\ref{lem:31}: with $p=16$ the premise $\beta_{16}(n)\ge 12$ is never available.335\end{proof}336337The same insertion argument explains why the certified row $p=18$ is self-consistent: if some $18$-set of boundary at most $11$ with ten consecutive empty columns existed at $n=22,23$ or $25$, it would propagate to all larger $n$ and contradict the certificates; such sets were searched for and do not exist (Section~\ref{sec:robustness}).338339\begin{figure}[t]340\centering341\includegraphics[width=\textwidth]{fig6_boundary_heatmap.pdf}342\caption{The boundary table $\beta_p(n)$ for $12\le p\le 24$, $13\le n\le 30$ (Computational Result~\ref{cr:boundary}). Cells marked $\ge 12$ carry a \code{drat-trim}-verified refutation of $\Fcnf(n,p)$; all other cells are exact values realised by an explicitly recounted $p$-set. The column $n=25$ (gold frame) defeats every $p\le 24$; the row $p=18$ from $n=26$ on (dashed) is the one used in the proof of Theorem~\ref{thm:main}.}343\label{fig:heatmap}344\end{figure}345346\begin{figure}[t]347\centering348\includegraphics[width=0.6\textwidth]{fig4_obstruction_P25_5.pdf}349\caption{The obstruction of Computational Result~\ref{cr:obstruction} in $\PP{25}{5}$: an $18$-set $X$ (rust) with $|\bd X|=10$ (grey). The two inner pentagons have no inner boundary, so the first-force method with $p=18$ cannot certify $\Z(\PP{25}{5})\ge 12$; the value is instead settled by exhaustive enumeration of all $37{,}353{,}738{,}800$ subsets of size $11$.}350\label{fig:obstruction}351\end{figure}352353\subsection{The certified window $26\le n\le 154$}354355\begin{compresult}\label{cr:window}356For every $n\in\{24\}\cup\{26,27,\dots,154\}$ the formula $\Fcnf(n,18)$ was refuted by CaDiCaL~1.9.5 with DRAT proof logging, and each proof was verified by \code{drat-trim} (output \code{s VERIFIED}, exit code $0$): $129$ certificates in the window plus one at $n=24$. Per-instance solve times range from $17.4$ to $266.8$\,s (mean $100.6$\,s, total 12,972.1\,s for the window), verification times from $13.3$ to $231.3$\,s (mean $90.7$\,s, total 11,700.7\,s), and proof lengths from 1,214,641 to 4,923,281 lines ($346{,}502{,}796$ lines, $39.0$\,GB in total). The largest CNF, $\Fcnf(154,18)$, has $14{,}323$ variables and $28{,}933$ clauses. The independent checker accepted all $130$ certificates (and five additional $p=20$ cross-checks at $n=26,\dots,30$, which are not used in the proof).357\end{compresult}358359Figure~\ref{fig:scaling}(a) and Table~\ref{tab:window} (Appendix~\ref{app:tables}) show the growth with $n$; the cost grows roughly quadratically and never approached the configured limits, so the window could be extended if a larger $p$ were ever needed.360361\begin{figure}[t]362\centering363\begin{subfigure}[t]{\textwidth}\centering364\includegraphics[width=0.9\linewidth]{fig5a_window_scaling.pdf}365\caption{Boundary certificates $\Fcnf(n,18)$, $26\le n\le 154$: CaDiCaL solve time, \code{drat-trim} verification time (left axis) and DRAT proof length (right axis).}366\end{subfigure}\\[6pt]367\begin{subfigure}[t]{\textwidth}\centering368\includegraphics[width=0.9\linewidth]{fig5b_enumeration_scaling.pdf}369\caption{Exhaustive enumeration at size $Z-1$: wall-clock time with 16 threads (left axis, log scale) and the number of subsets $\binom{2n}{Z-1}$ (right axis); the jump at $n=22$--$23$ reflects the increase of $Z-1$ from $9$ to $11$.}370\end{subfigure}371\caption{Cost of the two certified lower-bound engines (Computational Results~\ref{cr:exhaustive} and~\ref{cr:window}). All points are measured; no instance timed out.}372\label{fig:scaling}373\end{figure}374375\subsection{Proof of Theorem~\ref{thm:main}}376377\begin{proof}378\emph{Upper bounds.} For $n\ge 12$, $\Z\le 12$ by Proposition~\ref{prop:P7}. For $11\le n\le 22$ the witnesses of Table~\ref{tab:witnesses}, stored with their chronologies and replayed by the independent checker, give $\Z\le$ the stated value.379380\emph{Lower bounds for $11\le n\le 27$.} By Computational Result~\ref{cr:exhaustive} no zero-forcing set of size $Z-1$ exists (one representative per $D_n$-orbit, sound by Proposition~\ref{prop:orbit}; a smaller zero-forcing set would extend to one of size $Z-1$ by monotonicity of $\cl$), so $\Z\ge$ the stated value for $11\le n\le 27$. For $11\le n\le 22$ the same lower bounds follow independently from the verified refutations of $\Gcnf(n,Z-1)$ through Lemma~\ref{lem:35} and Proposition~\ref{prop:fort}, and for $23\le n\le 40$ from the second exhaustive program.381382\emph{Lower bound $12$ for $n\ge 26$.} By Computational Result~\ref{cr:window} and Lemma~\ref{lem:34}, $\beta_{18}(n)\ge 12$ for all $26\le n\le 154$. With $p=18$ we have $\cmax=14$ and $\Nmax=154$, so Lemma~\ref{lem:33} gives $\beta_{18}(n)\ge 12$ for every $n\ge 26$, and since $26\ge\lceil 29/2\rceil=15$, Lemma~\ref{lem:31} gives $\Z(\PP{n}{5})\ge 12$ for every $n\ge 26$.383384\emph{The cases $n=23,24,25$} are covered by the exhaustive lower bound $12$ ($n=24$ also by the boundary certificate at $n=24$ and $n=23,25$ also by the second exhaustive program). Together with the upper bound this gives $\Z=12$ for all $n\ge 23$.385386\emph{Sharpness.} $\Z(\PP{22}{5})=11<12$, so $n_0=23$.387\end{proof}388389No step of the proof infers anything about large $n$ from the shape of the table: for $n>154$ the argument is Lemma~\ref{lem:32} alone, and for $26\le n\le 154$ it is one certificate per $n$.390391\subsection{The certified table}392393Table~\ref{tab:exact} lists the exact values for $11\le n\le 48$ with the evidence behind each one and its relation to the literature; Figure~\ref{fig:values} plots them against the published bounds. Every value in the table is fully certified in the sense of Section~\ref{sec:framework}; the solver-supported round-encoding results and the heuristic searches add nothing to the status and are listed only as agreement tests.394395\begin{table}[t]396\centering\footnotesize397\caption{Certified exact values $\Z(\PP{n}{5})$, $11\le n\le 48$. ``bound'': best published upper bound before this work ($r(s+2)$ of Rashidi et al.\ where it beats $12$). ``literature'': published exact value and source --- R20 = \citet{rashidi2020petersen}, K26 = \citet{arxiv2607_19412}, KMZ = \citet{arxiv2610_24059} through the isomorphism of Proposition~\ref{prop:iso}, A18$^\dagger$ = \citet{alameda2018families} as reported second-hand in R20 (primary text not read). ``lower'': lower-bound evidence, codes as in Table~\ref{tab:paths}. ``class'': \emph{new} if, to our knowledge, no exact value was published; $^{h}$ marks the pre-registered holdout. All $38$ entries are fully certified.}398\label{tab:exact}399\input{../results/tables/tab_exact_values.tex}400\end{table}401402\begin{figure}[t]403\centering404\includegraphics[width=\textwidth]{fig3_exact_values.pdf}405\caption{Exact values of $\Z(\PP{n}{5})$ for $11\le n\le 48$ (Table~\ref{tab:exact}) against the published bounds. Squares: values known before (directly or through Proposition~\ref{prop:iso}); discs: values certified here; rings: the pre-registered holdout. For $n>48$ the value $12$ is proved by Theorem~\ref{thm:main} but no per-$n$ computation is tabulated.}406\label{fig:values}407\end{figure}408409\subsection{Negative results about the method and zero slack}410411\begin{observation}[zero slack]\label{obs:slack}412$\beta_{18}(n)=12$ exactly for every $26\le n\le 40$: at each of these $n$ an $18$-set of boundary $12$ exists (found as a model of $\Fcnf(n,18,12)$ and recounted). The certified lower bound $12$ is therefore the best the first-force method with $p=18$ can give, and the certificates have no margin: any under-constrained error in the encoding would have been fatal, which is why the encoding was validated exhaustively on small instances (Section~\ref{sec:robustness}).413\end{observation}414415\begin{observation}\label{obs:engines}416The round-based encoding (Appendix~\ref{app:round}) is impractical as a lower-bound engine beyond $n\approx 17$ (UNSAT at $s=Z-1$ for $11\le n\le 16$ within $26$\,s each; at $n=17$ one run timed out at $600$\,s and a second completed after 3295\,s; timeouts at $n=18,\dots,21$). The fort-cover engine with lazy minimal forts and dihedral images produced verified certificates up to $n=22$ (the $n=22$ certificate has $37{,}521$ fort clauses and $12{,}952{,}380$ proof lines) and returned UNSAT at $n=23$ ($837$\,s) and $n=25$ (1796\,s) in runs without proof logging. The stored formula for $n=23$ was afterwards re-solved under proof logging; the resulting DRAT proof (59,527,561 lines, 4.0\,GB) was verified by \code{drat-trim} (output \code{s VERIFIED}, exit code $0$, 2486\,s), is listed in Table~\ref{tab:fortcover}, and extends column~F of Table~\ref{tab:paths} to $n=23$. For $n=25$ a proof-logging re-solve of the stored formula produced a 103,621,714-line (7.7\,GB) proof whose \code{drat-trim} check could not be completed within the time limits of this run; the file and its digest are recorded but its status is unknown and it is not counted, so $\Z(\PP{25}{5})\ge 12$ continues to rest on the two exhaustive enumerations and is marked ``(s)'' in Table~\ref{tab:paths}. At the holdout values the fort-cover engine timed out at $600$\,s with up to 5,500,920 forts generated. The boundary engine scales to $n=154$ with proofs of a few million lines because it never reasons about the forcing process itself.417\end{observation}418419\section{Robustness and falsification}\label{sec:robustness}420421The study was pre-registered in the following sense. Before any $\PP{n}{5}$ computation, the conjecture-fitting range was fixed to $11\le n\le 30$ and the holdout set $H=\{32,35,37,41,44,48\}$ was frozen. Conjectures C1--C4 (Table~\ref{tab:conjectures}) were registered with timestamps from the data for $n\le 30$ before any value with $n>30$ was computed; the holdout was then computed once. All six holdout values are $12$, as predicted, and each is fully certified (boundary certificate plus Proposition~\ref{prop:P7}); a $600$\,s fort-cover search for an $11$-vertex zero-forcing set at each holdout $n$ found none. Competing residue hypotheses ($\gcd(n,5)$, $n\bmod 24$ and the moduli $2,3,4,6,8,10,12$) show no effect on $11\le n\le 30$ and are refuted for $n\ge 23$ by the theorem.422423\begin{table}[t]424\centering\footnotesize425\caption{The conjecture registry (\code{plan/conjectures.jsonl}). Statements were registered from data with $n\le 30$ at the time shown (2026-10-30, UTC) and tested on the frozen holdout afterwards; statuses are the final ones. C5 was registered during the robustness stage and is Proposition~\ref{prop:p16}.}426\label{tab:conjectures}427\input{../results/tables/tab_conjectures.tex}428\end{table}429430After the first complete proof, every ingredient was attacked (Table~\ref{tab:verification}).431432\begin{enumerate}[label=(\alph*)]433\item \emph{Re-derivation.} Every proposition and lemma was re-derived by hand; one presentational issue was found and corrected (a mis-description of the archived $n=25$ obstruction, now stated correctly in Computational Result~\ref{cr:obstruction}). No statement changed.434\item \emph{Second exhaustive path.} The first-force program (E$'$) reproduced all values for $11\le n\le 22$ and re-proved $\Z\ge 12$ for $23\le n\le 40$; in particular $\Z(\PP{23}{5})=\Z(\PP{25}{5})=12$, which in the first pass rested on a single program, now have two exhaustive proofs by different reduction principles, and the holdout values $32,35,37$ have a second certified path. As a positive control, at $n=23$, $s=12$ the program found 16,179,916 forcing sets.435\item \emph{Soundness of the boundary encoding.} An exhaustive enumeration (no SAT, no symmetry) tabulated the full distribution of $|\bd X|$ over all $p$-subsets for $n=13,14,15$ (all $p$) and $n=16$ ($10\le p\le 22$), $94$ $(n,p)$ pairs. For each pair $\Fcnf(n,p,\beta-1)$ was UNSAT and $\Fcnf(n,p,\beta)$ was SAT with a recounted model; all $50$ cells shared with the boundary table agree. Because the UNSAT side is exercised at $b=\beta-1$ on every instance, an over-constrained encoding, the one failure mode that could produce a false certificate, would have been detected.436\item \emph{Deletion lemma under stress.} D1: for $13\le n\le 30$ and every $X$ with $|X|\le 2$ ($\le 3$ for $n\le 20$) supported on columns $11,\dots,n-1$, the strong form $f(N[X])=N[X']$ holds in all $7{,}287$ cases. D2 (negative control): if $X$ may meet column $10$, the deleted column lies in $N[X]$ in $414$ of $810$ cases and the boundary size changes in $18$ of them, so the hypothesis of eleven empty columns is necessary and the test can detect violations. D3: on boundary-$11$ sets with a ten-column gap the insertion map and Lemma~\ref{lem:P9} were applied $25$ times each; the boundary stayed equal at every step and the original set was recovered, for $p=16$ at $n_0=22,26,30$; for $p=18$ at $n_0=22,23,25$ and $p=20$ at $n_0=24$ no such set exists (UNSAT), consistent with $\beta_{18}(n)\ge 12$ for $n\ge 26$.437\item \emph{Trust in the checker.} \code{drat-trim} rejected (exit code $1$, \code{s NOT VERIFIED}) the $\PP{26}{5}$ proof truncated to its first half, the same proof run against the CNF for $n=27$, and the same proof run against the satisfiable weakening $\Fcnf(26,18,12)$; the original pair still verifies. The independent checker was re-run on all $135$ boundary and $14$ fort-cover certificates, all accepted.438\item \emph{Direct attacks.} Simulated annealing over $11$-subsets maximising $|\cl(S)|$ for $23\le n\le 60$ and $n\in\{70,80,96,120,154,155,200\}$ ($45$ instances, seed $20261030$) found the planted positive controls at $(n,s)=(11,6),(13,9),(21,10),(22,11)$ but no $11$-set forcing any $\PP{n}{5}$ with $n\ge 23$; the best closures were $30$ of $46$ vertices at $n=23$, $34$ of $50$ at $n=25$ and $28$ for every $n\ge 26$. Annealing over $18$-subsets minimising $|\bd X|$ ($43$ instances, including $n=155,160,200$ beyond the certified window) reached the known table values at the controls and never found boundary $11$ for $n\ge 26$. This is heuristic evidence only; the proof does not depend on it.439\end{enumerate}440441\begin{table}[t]442\centering\footnotesize443\caption{Independent verification and falsification checks. Each row is an independently written implementation; ``failures'' counts outcomes that would have contradicted a claim (the $18$ changed boundaries of the negative control D2 are the expected behaviour when the hypothesis of Lemma~\ref{lem:P9} is violated).}444\label{tab:verification}445\input{../results/tables/tab_verification.tex}446\end{table}447448Nothing was overturned or weakened. The qualifications that remain are stated in Section~\ref{sec:limitations}.449450\section{Discussion}\label{sec:discussion}451452\paragraph{Competing explanations considered.} (1) \emph{A small-$n$ artifact.} A pattern seen for $n\le 30$ could fail later. This is excluded for $n\ge 26$ by proof (Lemma~\ref{lem:33} with the certified window), and the frozen holdout gave an honest out-of-sample test before the proof was complete; we note, however, that by the time the holdout values were computed the window $26\le n\le 154$ had been certified, so Lemma~\ref{lem:33} already guaranteed the prediction $12$ at every holdout $n$, and the holdout therefore tested the pipeline (witness replay, certificate generation and checking at new $n$) rather than the conjecture itself. (2) \emph{An artifact of the construction.} The constant $12$ could be a property of the $12$-outer-vertex construction while the true values are lower. The certified lower bounds exclude this, and the zero slack of Observation~\ref{obs:slack} shows that $12$ is the natural value of the boundary invariant. (3) \emph{A shared bug.} Agreement between solver paths could hide a common error (wrong adjacency, too short a round horizon, an over-constrained cardinality encoding). The two graph constructors, the three exhaustive and certificate paths with no shared code, the exhaustive validation of the encodings at small $n$, and the negative controls on the checker address this; the one bug that the campaign did find was a textual mis-description, not a computational error. (4) \emph{Residue dependence.} The inner structure depends on $\gcd(n,5)$, and $24\mid n$ was the only published family; neither affects the value for $n\ge 23$, and for $n\le 22$ the irregularity is explained by the isomorphisms to $k=3,4$ rather than by residues. (5) \emph{Prior containment.} The strongest risk is that \citet{alameda2018families} prove more than $\Z(\PP{24r}{5})=12$; we could not read the paper and claim nothing for $24\mid n$. The threshold statement and the values for $24\nmid n$ are not in the reported result.453454\paragraph{Thresholds across $k$.} The sharp thresholds now known are $n_0=13$ for $k=3$ and $n_0=18$ for $k=4$ \citep{arxiv2610_24059}, and $n_0=23$ for $k=5$ (Theorem~\ref{thm:main}), with the value $2k+2$ in each case. The three thresholds are consistent with $n_0(k)=5k-2$, but three data points do not justify a conjecture, and the mechanisms differ: for $k=5$ the boundary method itself fails at $n=25=k^2$ because of the inner pentagons, and the pre-threshold values are governed by isomorphisms to smaller $k$. We record the question rather than a conjecture.455456\begin{question}\label{q:threshold}457Is $\Z(\PP{n}{k})=2k+2$ for all $n\ge 5k-2$ and $k\ge 3$, with $\Z(\PP{5k-3}{k})<2k+2$? Does the first-force boundary method certify the lower bound for all $k$ with a parameter $p(k)$ and, for each $k$, which finitely many $n$ (such as $n=25$ for $k=5$) require a different argument?458\end{question}459460\paragraph{Maximum nullity.} Theorem~\ref{thm:main} gives $M(\PP{n}{5})\le 12$ for $n\ge 23$; \citet{alameda2018families} are reported to show equality for $24\mid n$ (as stated in \citealp[Remark~2.4]{rashidi2020petersen}; we could not read the primary text, see Table~\ref{tab:exact}). Whether $M(\PP{n}{5})=12$ for all $n\ge 23$ is open; we did not compute $M$.461462\paragraph{Methodological note.} The lower-bound method is borrowed; what the $k=5$ case adds is a clear view of its limits (Proposition~\ref{prop:p16}, Computational Result~\ref{cr:obstruction}, Observation~\ref{obs:slack}) and a certification discipline in which each machine-checked input is a DRAT proof for a formula whose relation to the theorem is a proved lemma, re-verified by a second program, with negative controls on the checker. We regard the explicit account of what is machine-checked and what is not (Appendix~\ref{sec:scope}) as part of the result.463464\section{Limitations}\label{sec:limitations}465466\begin{itemize}467\item For $n>40$ the lower bound rests on one certified path (the boundary certificates plus Lemmas~\ref{lem:31}--\ref{lem:34}); the fort-cover second path exists only for $n\le 23$ and the exhaustive paths only for $n\le 27$ and $n\le 40$. For $n>154$ no certificate exists at all and the proof is Lemma~\ref{lem:32}, which we have proved but not formalized.468\item No Lean~4 formalization was attempted (toolchain unavailable in the execution environment), so no statement in this paper is formally verified in the proof-assistant sense; the machine-checked parts are the DRAT proofs and the exhaustive enumerations (Appendix~\ref{sec:scope}).469\item The DRAT proofs occupy $39.0$\,GB and are not shipped with the archive; their SHA-256 digests are recorded in the result records and they can be regenerated from the released generator (about $100$\,s per instance). Readers who want to verify the window without regenerating proofs must trust the digests.470\item The value $\Z(\PP{24r}{5})=12$ is cited second-hand; the primary statement and its hypotheses were not read.471\item The exhaustive oracle relies on the correctness of two C programs; they are cross-validated against each other, against an unreduced Python enumeration on two graphs, against the Burnside orbit counts, and against DRAT-certified refutations for $n\le 22$, but no formal proof of the programs exists.472\item The heuristic searches of Section~\ref{sec:robustness}(f) are evidence of absence only in the heuristic sense.473\item The search for the smallest working parameter $p$ was restricted to $p\le 24$ and $n\le 30$; we did not determine whether any $p$ certifies $n=25$.474\item The literature search covered Crossref, OpenAlex, arXiv and Semantic Scholar with verified identifiers for all $20$ sources; three sources were read in full, eight at abstract level and nine at metadata level. An unindexed thesis or report containing some of the small-$n$ values could have been missed.475\end{itemize}476477\section{Conclusion}\label{sec:conclusion}478479We have determined $\Z(\PP{n}{5})$ for all $n\ge 11$ and proved that the stabilization threshold is $n_0=23$, closing the $k=5$ case of a problem left open by the 2026 results for $k=3,4$. The proof combines the known $2k+2$ construction, the first-force boundary method with the parameter $p=18$ (the smallest that can work, since $p=16$ provably fails for all $n\ge 22$), a column-deletion reduction to the finite window $26\le n\le 154$ settled by $129$ externally checked DRAT certificates, and exhaustive enumeration for $n\le 27$, which is unavoidable at $n=25$ where inner pentagons defeat the boundary method for every $p\le 24$. All values for $11\le n\le 48$ are fully certified with independently replayed witnesses and independently re-verified lower-bound evidence, a pre-registered holdout confirmed the registered conjectures, and a falsification campaign found no error. Code, certificates (with digests), the conjecture registry and a one-command reproduction script are released with this paper.480481\appendix482483\section{The round-based SAT encoding}\label{app:round}484485Fix $s$ and $T=2n-s$. The CNF has variables $x_w$ (seed), $b_{w,t}$ for $0\le t\le T$ (black after round $t$) and $f_{b,w,t}$ for $bw\in E$, $1\le t\le T$ (force $b\to w$ in round $t$), with clauses: (i) $b_{w,0}\leftrightarrow x_w$; (ii) $b_{w,t}\to b_{w,t-1}\vee\bigvee_{b\in N(w)}f_{b,w,t}$; (iii) $f_{b,w,t}\to b_{b,t-1}\wedge\bigwedge_{w'\in N(b)\setminus\{w\}}b_{w',t-1}$; (iv) $b_{w,T}$ for all $w$; (v) a sequential-counter encoding of $\sum_w x_w\le s$.486487\begin{proposition}\label{prop:P4}488The CNF is satisfiable if and only if $\Z(G)\le s$.489\end{proposition}490491\begin{proof}492\emph{Soundness.} From a model let $S=\{w:x_w\}$, so $|S|\le s$ by (v). We show by induction on $t$ that $\{w:b_{w,t}\}\subseteq\cl(S)$. For $t=0$ this is (i). If $b_{w,t}$ holds then by (ii) either $b_{w,t-1}$ holds (induction) or some $f_{b,w,t}$ holds; by (iii) $b$ and all of $N(b)\setminus\{w\}$ are black at round $t-1$, hence in $\cl(S)$ by induction. If $w\notin\cl(S)$ then $b\in\cl(S)$ would have $N(b)\setminus\cl(S)=\{w\}$ and could force at the fixed point $\cl(S)$, which is impossible; so $w\in\cl(S)$. By (iv), $V\subseteq\cl(S)$.493\emph{Completeness.} Let $S$ be zero forcing with $|S|\le s$ and run the synchronous process $B_0=S$, $B_t=\Phi(B_{t-1})$ with $\Phi$ as in the proof of Proposition~\ref{prop:order}. Set $b_{w,t}=[w\in B_t]$ and $f_{b,w,t}=[b\in B_{t-1},\ N(b)\setminus B_{t-1}=\{w\}]$; (i)--(iii) hold by construction and (v) by $|S|\le s$. Each $B_t$ is reachable by a chronology (perform the available forces one at a time; by Step~1 of Proposition~\ref{prop:order} each remains legal), so $B_t\subseteq\cl(S)=V$, and while $B_{t-1}\ne V$ some force is available (otherwise $B_{t-1}$ would be a fixed point $\ne V$ above $S$), so $|B_t|\ge|B_{t-1}|+1$. Hence $B_t=V$ for $t\ge 2n-|S|$, and $2n-|S|\le 2n-s=T$ gives (iv).494\end{proof}495496The horizon $T=2n-s$ is exact in the sense that every forcing process from a set of size $s$ terminates within $T$ rounds; the propagation time of \citet{hogben2012propagation} is typically far smaller, but the exact horizon keeps the encoding complete without further argument.497498\section{Computational protocol}\label{app:protocol}499500\paragraph{Hardware and software.} All computations ran on a single MacLustr worker node (identifier \code{M4M64c}; Apple Silicon, 16 CPU cores, macOS~26.4). Python~3.14.7; PySAT~1.9.dev17 with CaDiCaL~1.9.5 (boundary and fort-cover formulas, DRAT logging) and Glucose~4.1 (round encoding); \code{drat-trim} built from the GitHub source fetched on 2026-10-30 (source SHA-256 \code{d834b649\dots a0c2ee}, full digest in the result records); SymPy~1.14.0 for the symbolic identities; C programs compiled with \code{gcc -O2}. No GPU, no cluster scheduler and no external service were used; all reported timings are wall-clock times measured on this node, and CPU times where stated.501502\paragraph{Job structure and limits.} One process per graph order $n$ with a bounded pool of workers (6 for the boundary table, 5--12 for the certified window, 16 threads inside each C enumeration). Limits: exhaustive oracle $3{,}600$\,s per $n$; fort-cover $600$\,s (holdout searches) to $1{,}200$\,s (exact runs); round encoding $600$\,s (one rerun at $n=17$ without limit). A timed-out solver is recorded as \emph{unknown}. No boundary-window instance approached its limit (maximum $266.8$\,s).503504\paragraph{Randomness.} The only random inputs are the seed sets and force orders of the order-independence test (seed $20261030\cdot 1000+n$), the random instances of the lemma checks, and the simulated-annealing attacks (seed $20261030$); all are inputs to deterministic checks and are recorded. Nothing in this study is simulated or synthetic data in the statistical sense: all objects are generated from Definition~\ref{def:gp}.505506\begin{sloppypar}\paragraph{Records.} Every solver run is a JSON record with UTC start time, $n$, $k$, graph digest, method, bound, solver name and version, wall time, timeout flag, witness or certificate paths and their SHA-256 digests (\path{results/solver_runs.jsonl}, \path{results/boundary_certificates.jsonl}, \path{results/lower_bound_certificates.jsonl}, \path{results/brute_force_runs.jsonl}); the independent checker's verdicts are in \path{results/lower_bound_verification.json} and \path{results/upper_bound_verification.json}.\end{sloppypar}507508\section{Reproducibility and artifact layout}\label{app:repro}509510\begin{sloppypar}The released directory contains \path{code/} (graph constructors, closure oracle, both C enumerators, the SAT drivers, the independent checkers, the figure and table generators, \code{reproduce.sh} and pinned \code{requirements.txt}), \path{code/proofs/handwritten/} (the step-numbered proofs), \path{code/proofs/certificates/} (DIMACS files, fort lists and, where shipped, DRAT proofs), \path{results/} (all tables, records, the counterexample archive, \code{derivations.md}, \code{robustness.md} and \path{metrics.json}), and \path{plan/} (the pre-registered plan with the frozen holdout, the prior-art audit and \path{conjectures.jsonl}). Running \path{sh code/reproduce.sh} from the root makes a working copy of the code and of the small result files under \path{results/reproduction/work/}, rebuilds the tools there, re-runs the invariant and lemma checks, replays every witness, re-verifies shipped certificates whose proof files are present, regenerates a bounded part of the computation with fresh proofs, and finally compares the working copy with the shipped files (\path{results/reproduction/summary.json}); the shipped artifacts are never modified. Every step is logged with its command, start and end time and exit code. The three modes regenerate different parts of the tables, and we state them precisely because the DRAT proofs of the boundary window ($39.0$\,GB) and the two large fort-cover proofs ($4.0$\,GB at $n=23$, $7.7$\,GB at $n=25$) may be absent from distributed copies of the archive (their digests are in the result records and in Tables~\ref{tab:fortcover} and~\ref{tab:window}; a proof that is not on disk is reported as \emph{skipped}, never as verified):511\begin{itemize}512\item \code{QUICK=1} (about ten minutes): steps 0--3, 9 and 10. It re-verifies with \code{drat-trim} the shipped fort-cover proofs for $n\le 21$ and a fixed sample of the boundary proofs ($n=24$, $26,\dots,40$, $60$) when they are present, and re-runs the robustness checks that need no enumeration.513\item default (about 25 minutes on 16 cores; bounded so that it stays well inside the platform's one-hour limit): adds the exhaustive oracle for $11\le n\le 22$ (rows $11$--$22$ of Table~\ref{tab:bruteforce}), the boundary table for $16\le p\le 20$, the certified window for $26\le n\le 40$ regenerated with fresh DRAT proofs (each checked; the regenerated CNF must have the digest of the shipped one), the fort-cover certificates for $n\le 21$ (the round encoding only for $n\le 17$, with a $60$\,s limit), and a re-check of the regenerated certificates.514\item \code{FULL=1} (about six further hours): adds the exhaustive oracle at $23\le n\le 27$ (the last five rows of Table~\ref{tab:bruteforce}), the complete boundary table, the complete window $26\le n\le 154$ (about $35$ minutes on 12 cores), the fort-cover certificate at $n=22$ (about eleven minutes), a \code{drat-trim} re-check of \emph{every} shipped proof present on disk including the two large fort-cover proofs (about three hours), the proof-logging re-solves of the stored fort-cover formulas for $n=23$ and $n=25$ (column~F of Table~\ref{tab:paths} at these $n$; two to three hours), the round encoding for $18\le n\le 22$ with its original $600$\,s limit, the second enumerator E$'$ through $n=40$ (column E$'$ of Tables~\ref{tab:paths} and~\ref{tab:bruteforce} for $n\ge 23$) and the exhaustive boundary-encoding checks of Section~\ref{sec:robustness}(c).515\end{itemize}516An interrupted step leaves the corresponding result rows unchanged; a killed or timed-out solver is never recorded as UNSAT. The outcome of our own runs of the default and \code{QUICK} modes, and of the platform's earlier clean re-execution, is described in \path{manuscript/reproducibility.md}.\end{sloppypar}517518\section{Scope of machine checking}\label{sec:scope}519520Table~\ref{tab:scope} states, for each component of the proof, what is proved by hand for all $n$, what is a machine-checked finite input and with which checker, and whether any formal (proof-assistant) verification exists. There is none; the claim ``verified'' in this paper always means ``verified by \code{drat-trim} and re-verified by an independent re-implementation'', never ``formally verified''.521522\begin{table}[h]523\centering\footnotesize524\caption{Human proof, machine-checked input and formal verification for each component.}525\label{tab:scope}526\input{../results/tables/tab_scope.tex}527\end{table}528529\section{Additional tables}\label{app:tables}530531\begin{table}[h]532\centering\footnotesize533\caption{One minimum zero-forcing set for each $11\le n\le 22$ (the first $D_n$-orbit representative found by the exhaustive oracle) and the number of forcing orbit representatives at size $Z$. Each set is stored with a complete chronology and was replayed by the independent checker. Only $n=15$ needs inner vertices in the listed representative; for $n\ge 17$ ten or eleven consecutive outer vertices (with one gap for $n=17,18$) suffice, and for $n=11$ two triples of consecutive outer vertices do.}534\label{tab:witnesses}535\input{../results/tables/tab_witnesses.tex}536\end{table}537538\begin{table}[h]539\centering\footnotesize540\caption{The boundary table $\beta_p(n)$ for $20\le n\le 30$ (the full range $13\le n\le 30$ is in Figure~\ref{fig:heatmap} and \code{results/tables/boundary\_table.csv}). Bold entries are certified refutations of $\Fcnf(n,p)$; all other entries are exact values with a recounted witness.}541\label{tab:boundarytable}542\input{../results/tables/tab_boundary_table.tex}543\end{table}544545\begin{table}[h]546\centering\footnotesize547\caption{Fort-cover certificates $\Gcnf(n,Z-1)$ for $11\le n\le 23$ (path F): size of the fort list at termination, CNF size, DRAT proof length and CaDiCaL time of the proof-logging re-solve. Every certificate was verified by \code{drat-trim}; those for $n\le 22$ were also re-verified by the independent checker, which re-validates every listed fort (the $n=23$ certificate was checked by \code{drat-trim} through a plain subprocess, Observation~\ref{obs:engines}). $^{*}$n/r: the proof-logging re-solve at $n=23$ ran as a separate process that ended before its record was written, so no solve time is recorded.}548\label{tab:fortcover}549\input{../results/tables/tab_fortcover.tex}550\end{table}551552\begin{table}[h]553\centering\scriptsize554\caption{Boundary certificates $\Fcnf(n,18)$ at selected $n$ in the certified window (all $129$ rows: \code{results/tables/boundary\_window\_p18.csv}). Digests are the first 16 hex characters of the SHA-256 of the DIMACS file and of the DRAT proof.}555\label{tab:window}556\input{../results/tables/tab_window_scaling.tex}557\end{table}558559\section{Note on the autonomous research process}\label{app:process}560561This working paper was produced by an autonomous research pipeline under a fixed brief. The scientific content (definitions, proofs, encodings, programs and the interpretation of results) was generated and checked within that pipeline; the pre-registration of the fitting range and holdout, the three-valued certification vocabulary, the independent re-implementation of every checker, and the requirement that every reported number be traceable to a stored artifact were imposed as process rules before computation began. The literature audit verified the identifiers of all $20$ cited sources and recorded the reading depth of each. The MacLustr compute infrastructure is credited for computation only. Nothing in this appendix is a mathematical claim.562563\bibliographystyle{autoscholar}564\bibliography{references}565566\end{document}567