1% Appendices (A--G) of the AutoScholar manuscript, retypeset for the UQO series2\newpage3\begin{appendices}45\renewcommand{\thetable}{A\arabic{table}}6\renewcommand{\thefigure}{A\arabic{figure}}7\setcounter{table}{0}8\setcounter{figure}{0}91011\section{The round-based SAT encoding}\label{app:round}1213Fix $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$.1415\begin{proposition}\label{prop:P4}16The CNF is satisfiable if and only if $\Z(G)\le s$.17\end{proposition}1819\begin{proof}20\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)$.21\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).22\end{proof}2324The 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.2526\section{Computational protocol}\label{app:protocol}2728\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.2930\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).3132\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}.3334\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}3536\section{Reproducibility and artifact layout}\label{app:repro}3738\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):39\begin{itemize}40\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.41\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.42\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).43\end{itemize}44An 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}4546\section{Scope of machine checking}\label{sec:scope}4748Table~\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''.4950\begin{table}[h]51\centering\footnotesize52\caption{Human proof, machine-checked input and formal verification for each component.}53\label{tab:scope}54\input{tables/tab_scope.tex}55\end{table}5657\section{Additional tables}\label{app:tables}5859\begin{table}[h]60\centering\footnotesize61\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.}62\label{tab:witnesses}63\input{tables/tab_witnesses.tex}64\end{table}6566\begin{table}[h]67\centering\footnotesize68\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.}69\label{tab:boundarytable}70\input{tables/tab_boundary_table.tex}71\end{table}7273\begin{table}[h]74\centering\footnotesize75\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.}76\label{tab:fortcover}77\input{tables/tab_fortcover.tex}78\end{table}7980\begin{table}[h]81\centering\scriptsize82\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.}83\label{tab:window}84\input{tables/tab_window_scaling.tex}85\end{table}8687\section{Note on the autonomous research process}\label{app:process}8889This 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.9091\paragraph{UQO working paper edition.} This paper first appeared as AutoScholar Working Paper AS-WP-2026-0001 (version~1, 30~October 2026, \url{https://www.autoscholar.ai}), produced by the AutoScholar.ai autonomous research pipeline (Claude Fable~5.1 agents executing on the MacLustr worker node \code{M4M64c}) under a research brief written by the author, who designed and operates the platform. It is reissued as UQO Working Paper No.~32 with the scientific content, proofs, programs, result records and certificates of the original release; only the typesetting (UQO working paper template), the numbering of the appendix tables and this note differ. The complete artifact (code, results, pre-registered plan, QA report, provenance records and the original AutoScholar manuscript) accompanies this working paper.9293\end{appendices}94