1% Section: Exact computation and certification framework2\section{Exact computation and certification framework}\label{sec:framework}34\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.56\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}$.78\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.910\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.1112\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$.1314\begin{table}[t]15\centering\footnotesize16\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.}17\label{tab:paths}18\input{tables/tab_paths.tex}19\end{table}20