1% Section: Lower bounds: the first-force boundary method for $k=5$2\section{Lower bounds: the first-force boundary method for $k=5$}\label{sec:lower}34\subsection{The two lemmas}56\begin{lemma}[first-force boundary lemma, {\citealp[Lemma~2.1]{arxiv2610_24059}}]\label{lem:P8}7If 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|$.8\end{lemma}910\begin{proof}11A 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|$.12\end{proof}1314\begin{lemma}[column deletion for $k=5$, after {\citealp[Lemma~2.2]{arxiv2610_24059}}]\label{lem:P9}15Let $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|$.16\end{lemma}1718\begin{proof}19$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'$.2021Fix 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])$.22\end{proof}2324The 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)).2526\subsection{From boundaries to zero forcing and the finite reduction}2728\begin{lemma}\label{lem:31}29Let $p\ge1$ and $n\ge\lceil(p+11)/2\rceil$. If $\beta_p(n)\ge 12$ then $\Z(\PP{n}{5})\ge 12$.30\end{lemma}3132\begin{proof}33Suppose $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$.34\end{proof}3536\begin{lemma}[finite reduction]\label{lem:32}37Let $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$.38\end{lemma}3940\begin{proof}41Let $|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$.42\end{proof}4344\begin{lemma}[what a finite window proves]\label{lem:33}45Let $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)$.46\end{lemma}4748\begin{proof}49A 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}.50\end{proof}5152For $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$.5354\subsection{Two SAT encodings and their correctness}\label{sec:encodings}5556The 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.5758\begin{lemma}[boundary formulas]\label{lem:34}59For 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$.60\end{lemma}6162\begin{proof}63($\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$.64\end{proof}6566Thus 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.6768\begin{lemma}[fort-cover formulas]\label{lem:35}69For 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$.70\end{lemma}7172\begin{proof}73Let $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$.74\end{proof}7576The 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.7778A third, round-based encoding of the forcing process (Appendix~\ref{app:round}) was used as an additional agreement test for small $n$ only.79