1% Section: Results2\section{Results}\label{sec:results}34\subsection{Exhaustive values for $11\le n\le 27$}56\begin{compresult}\label{cr:exhaustive}7For $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.8\end{compresult}910Table~\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.1112\begin{table}[t]13\centering\footnotesize14\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$.}15\label{tab:bruteforce}16\input{tables/tab_brute_force.tex}17\end{table}1819\subsection{Choosing the parameter: the boundary table and the obstruction at $n=25$}2021\begin{compresult}\label{cr:boundary}22For $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$.23\end{compresult}2425\begin{compresult}[obstruction at $n=25$]\label{cr:obstruction}26In $\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$.27\end{compresult}2829The 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$:3031\begin{proposition}\label{prop:p16}32$\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$.33\end{proposition}3435\begin{proof}36There 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.37\end{proof}3839The 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}).4041\begin{figure}[t]42\centering43\includegraphics[width=\textwidth]{fig6_boundary_heatmap.pdf}44\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}.}45\label{fig:heatmap}46\end{figure}4748\begin{figure}[t]49\centering50\includegraphics[width=0.6\textwidth]{fig4_obstruction_P25_5.pdf}51\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$.}52\label{fig:obstruction}53\end{figure}5455\subsection{The certified window $26\le n\le 154$}5657\begin{compresult}\label{cr:window}58For 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).59\end{compresult}6061Figure~\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.6263\begin{figure}[t]64\centering65\begin{subfigure}[t]{\textwidth}\centering66\includegraphics[width=0.9\linewidth]{fig5a_window_scaling.pdf}67\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).}68\end{subfigure}\\[6pt]69\begin{subfigure}[t]{\textwidth}\centering70\includegraphics[width=0.9\linewidth]{fig5b_enumeration_scaling.pdf}71\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$.}72\end{subfigure}73\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.}74\label{fig:scaling}75\end{figure}7677\subsection{Proof of Theorem~\ref{thm:main}}7879\begin{proof}80\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.8182\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.8384\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$.8586\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$.8788\emph{Sharpness.} $\Z(\PP{22}{5})=11<12$, so $n_0=23$.89\end{proof}9091No 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$.9293\subsection{The certified table}9495Table~\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.9697\begin{table}[t]98\centering\footnotesize99\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.}100\label{tab:exact}101\input{tables/tab_exact_values.tex}102\end{table}103104\begin{figure}[t]105\centering106\includegraphics[width=\textwidth]{fig3_exact_values.pdf}107\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.}108\label{fig:values}109\end{figure}110111\subsection{Negative results about the method and zero slack}112113\begin{observation}[zero slack]\label{obs:slack}114$\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}).115\end{observation}116117\begin{observation}\label{obs:engines}118The 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.119\end{observation}120