% Section: Robustness and falsification
\section{Robustness and falsification}\label{sec:robustness}

The 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.

\begin{table}[t]
\centering\footnotesize
\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}.}
\label{tab:conjectures}
\input{tables/tab_conjectures.tex}
\end{table}

After the first complete proof, every ingredient was attacked (Table~\ref{tab:verification}).

\begin{enumerate}[label=(\alph*)]
\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.
\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.
\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.
\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$.
\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.
\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.
\end{enumerate}

\begin{table}[t]
\centering\footnotesize
\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).}
\label{tab:verification}
\input{tables/tab_verification.tex}
\end{table}

Nothing was overturned or weakened. The qualifications that remain are stated in Section~\ref{sec:limitations}.