# Derivations and proofs — zero forcing in P(n,5)

Run 951263fc · Stage 4 (execution) · 2026-10-30. Every statement below is proved in full here or is explicitly marked as a computational result with the artifact that supports it. Numbered steps are meant to be attacked one at a time by the referee context. Notation follows plan/formal-setup.md (D1–D7). Throughout, $k=5$ unless stated otherwise, $V=V(P(n,k))$, indices are modulo $n$, $N(w)$ is the open neighbourhood, $\partial X={w\notin X: N(w)\cap X\neq\emptyset}$, $N[X]=X\cup\partial X$.

Reading guide. §1 foundations (P1–P5), §2 structural lemmas (P6–P9), §3 the lower-bound machinery (Lemmas 3.1–3.4), §4 the computational results with their certificates, §5 the main theorem, §6 what was checked numerically or symbolically (code/verify_lemmas.py, results/lemma_checks.json), §7 negative results and the exact boundary of what is proved.

# 1. Foundations

# P1. Order independence of the closure

Statement. Let $G=(V,E)$ be a finite graph and $S\subseteq V$. Every maximal chronology from $S$ (a sequence of legal forces that cannot be extended) ends in the same black set, denoted $\mathrm{cl}(S)$. Consequently "$S$ is a zero-forcing set" ($\mathrm{cl}(S)=V$) is well defined, $\mathrm{cl}$ is monotone and idempotent, and $\mathrm{cl}(\varphi S)=\varphi,\mathrm{cl}(S)$ for every automorphism $\varphi$.

Proof.

1. Monotonicity of the rule. Suppose $b\in B\subseteq B'$ and $b$ can force $w$ at colouring $B$, i.e. $N(b)\setminus B={w}$. If $w\notin B'$ then $N(b)\setminus B'\subseteq N(b)\setminus B={w}$ and $w\in N(b)\setminus B'$, hence $N(b)\setminus B'={w}$: $b$ can still force $w$ at $B'$. If $w\in B'$ the force has become vacuous.

2. The closure as a least fixed point. Define $\Phi(B)=B\cup{w\notin B:\exists b\in B,\ N(b)\setminus B={w}}$. By step 1, $B\subseteq B'$ implies $\Phi(B)\subseteq\Phi(B')$ (each $w\in\Phi(B)\setminus B$ either lies in $B'$ or is forced by the same $b$ at $B'$). Let $C$ be the final set of a maximal chronology $B_0=S\subset B_1\subset\dots\subset B_m=C$ where $B_{i+1}=B_i\cup{w_i}$. Maximality means $\Phi(C)=C$.

3. Every chronology is contained in every fixed point above $S$. Let $D\supseteq S$ with $\Phi(D)=D$. By induction $B_i\subseteq D$: if $B_i\subseteq D$ and $b_i\in B_i$ forces $w_i$ at $B_i$, then by step 1 either $w_i\in D$ or $b_i$ forces $w_i$ at $D$, which contradicts $\Phi(D)=D$. So $w_i\in D$ and $B_{i+1}\subseteq D$.

4. Conclusion. If $C$ and $C'$ are the final sets of two maximal chronologies from $S$, then both are fixed points of $\Phi$ containing $S$, so by step 3 applied twice, $C\subseteq C'$ and $C'\subseteq C$. Hence $\mathrm{cl}(S)$ is the least fixed point of $\Phi$ above $S$; monotonicity of $\mathrm{cl}$ follows from step 3 ($\mathrm{cl}(S')$ is a fixed point above $S$ when $S\subseteq S'$), idempotence from $\Phi(\mathrm{cl}(S))=\mathrm{cl}(S)$, and equivariance from the fact that $\varphi$ maps legal forces to legal forces and fixed points to fixed points. $\square$

Empirical companion. Test T2 (code/closure_oracle.py; results/t2_order_independence.json): for $n=11,\dots,16$, 200 random seed sets each, 20 random force orders each, the final black set was identical across orders in 1200/1200 cases.

# P2. Fort characterization

Statement. $S$ is a zero-forcing set of $G$ if and only if $S\cap F\neq\emptyset$ for every fort $F$ of $G$ (D4).

Proof. ($\Rightarrow$) Let $F$ be a fort with $F\cap S=\emptyset$ and let $S$ be zero forcing. Some chronology from $S$ colours all of $V$, in particular $F$; consider the first force $b\to w$ with $w\in F$. Just before it, no vertex of $F$ is black, so $b\notin F$, and $N(b)$ contains exactly one white vertex, namely $w$. Every other neighbour of $b$ is black and hence outside $F$, so $|N(b)\cap F|=1$, contradicting the fort property at $b\notin F$. ($\Leftarrow$) If $\mathrm{cl}(S)\neq V$, put $W=V\setminus\mathrm{cl}(S)\neq\emptyset$. For $b\in\mathrm{cl}(S)=V\setminus W$, the set $N(b)\cap W$ is the set of white neighbours of $b$ at the final colouring; it has size $\neq1$ because no force is available at a fixed point. Hence $W$ is a fort, and $W\cap S=\emptyset$. $\square$

This is Theorem 8 of Brimkov–Fast–Hicks (2019) [brimkov2019computational], reproved here because the fort-cover certificates rely on it.

# P3. Symmetry and orbit reduction

Statement. If $\varphi\in\mathrm{Aut}(G)$ then $\mathrm{cl}(\varphi S)=\varphi,\mathrm{cl}(S)$; thus $S$ is zero forcing iff $\varphi S$ is, and $|\varphi S|=|S|$. Consequently, in an exhaustive search over $s$-subsets it suffices to test one representative per orbit of any subgroup $H\le\mathrm{Aut}(G)$: there is a zero-forcing $s$-set iff some orbit representative is zero forcing.

Proof. Equivariance is P1 step 4. If $S$ is a zero-forcing $s$-set then its orbit representative $S_0=\psi S$ ($\psi\in H$) is zero forcing of size $s$; conversely a zero-forcing representative is itself a zero-forcing $s$-set. $\square$

The C oracle (code/brute_force.c) uses $H=D_n$ (D6) and the representative "lexicographically least bitmask in the orbit"; it tests exactly the subsets equal to the minimum of their own orbit, which is one representative per orbit. Nothing requires the optimal set to be symmetric. The reduction is sound for $n=12,24$ as well, where $D_n$ is a proper subgroup of the full automorphism group (Frucht–Graver–Watkins).

# P4. Soundness and completeness of the round-based SAT encoding

Statement. Fix $s$ and $T=2n-s$. The CNF with variables $x_w$, $b_{w,t}$ $(0\le t\le T)$, $f_{b,w,t}$ $(bw\in E, 1\le t\le T)$ and clauses (i)–(v) of plan/formal-setup.md P4 is satisfiable iff $Z(G)\le s$.

Proof. Soundness. Take a model and $S={w:x_w}$, so $|S|\le s$ by (v) and $S={w:b_{w,0}}$ by (i). Claim: for every $t$, ${w:b_{w,t}}\subseteq\mathrm{cl}(S)$. Induction on $t$: if $b_{w,t}$ holds then by (ii) either $b_{w,t-1}$ (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 lie in $\mathrm{cl}(S)$ by induction; then either $w\in\mathrm{cl}(S)$ already, or $b\in\mathrm{cl}(S)$ has $N(b)\setminus\mathrm{cl}(S)={w}$ and can force $w$ at the fixed point $\mathrm{cl}(S)$, which is impossible — so $w\in\mathrm{cl}(S)$. By (iv), $V\subseteq\mathrm{cl}(S)$. Completeness. Let $S$ be zero forcing with $|S|\le s$. Run the synchronous process: $B_0=S$, $B_{t}=\Phi(B_{t-1})$. 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}]$. Clauses (i)–(iii) hold by construction. $B_t$ is a chronology-reachable set (perform the available forces one at a time; by P1 step 1 each stays legal), so $B_t\subseteq\mathrm{cl}(S)=V$, and while $B_{t-1}\neq V$ at least one force is available (otherwise $B_{t-1}$ would be a fixed point $\neq V$ above $S$, contradicting P1 step 4), so $|B_t|\ge|B_{t-1}|+1$. Therefore $B_t=V$ for $t\ge 2n-|S|$, and $2n-|S|\le 2n-s=T$ gives (iv). $\square$

# P5. Graph facts

Statement. For $n\ge 11$: $P(n,5)$ is simple and cubic with $2n$ vertices and $3n$ edges, connected, with inner subgraph a disjoint union of $\gcd(n,5)$ cycles of length $n/\gcd(n,5)$, and $D_n$ acts by automorphisms.

Proof. The three edge families are pairwise disjoint (outer–outer, outer–inner, inner–inner). Outer edges $u_iu_{i+1}$ are the $n$ edges of a cycle. Inner edges $v_iv_{i+5}$: $v_i v_{i+5}=v_jv_{j+5}$ iff $i=j$ or $i=j+5,\ j=i+5$, i.e. $10\equiv0\pmod n$, excluded by $n\ge11$; and $v_iv_{i+5}$ is a loop iff $5\equiv0\pmod n$, excluded. So there are exactly $3n$ distinct edges, no loops, each $u_i$ has neighbours $u_{i\pm1},v_i$ and each $v_i$ has $v_{i\pm5},u_i$, all distinct (for $v_i$: $v_{i+5}\neq v_{i-5}$ since $10\not\equiv0$). Connectivity: the outer cycle is connected and every $v_i$ is joined to it by a spoke. The inner subgraph is the Cayley graph of $\mathbb Z_n$ with connection set ${\pm5}$; the orbit of $i$ under $+5$ has size $n/\gcd(n,5)$ and there are $\gcd(n,5)$ orbits, each inducing a cycle (length $\ge 11/5>2$, so a genuine cycle). Rotation $\rho$ and reflection $\sigma$ (D6) map each edge family to itself. $\square$

Computational companion (T1). code/graph_constructor.py, output results/t1_graph_invariants.json: for $n=11,\dots,48$ the edge-formula constructor and the block-circulant-matrix constructor produce identical edge lists; $2n$ vertices, $3n$ edges, all degrees 3, connected, $\gcd(n,5)$ inner cycles, all $2n$ dihedral maps are automorphisms; SHA-256 of each canonical edge list recorded. Also P(5,2).

# 2. Structural lemmas

# P6. Isomorphism $P(n,k)\cong P(n,l)$ for $kl\equiv1\pmod n$

Statement. Let $\gcd(n,k)=1$, $kl\equiv1\pmod n$. Then $\psi(v_{jk})=u_j$, $\psi(u_{jk})=v_j$ ($j\in\mathbb Z_n$) is an isomorphism $P(n,k)\to P(n,l)$; also $P(n,l)\cong P(n,n-l)$ by $i\mapsto-i$ on both layers.

Proof. Since $\gcd(n,k)=1$, $j\mapsto jk$ is a bijection of $\mathbb Z_n$, so $\psi$ is a bijection $V\to V$ (it swaps layers). Images of the three edge families of $P(n,k)$: inner edge $v_{jk}v_{jk+k}=v_{jk}v_{(j+1)k}\mapsto u_ju_{j+1}$ (outer edge); spoke $u_{jk}v_{jk}\mapsto v_ju_j$ (spoke); outer edge $u_{jk}u_{jk+1}$: write $jk+1=(j+l)k$, valid because $lk\equiv1$; so $u_{jk}u_{(j+l)k}\mapsto v_jv_{j+l}$ (inner edge of $P(n,l)$). Thus $\psi$ maps $E(P(n,k))$ into $E(P(n,l))$, injectively, and both have $3n$ edges, so $\psi$ is an isomorphism. The map $i\mapsto -i$ sends $v_iv_{i+l}$ to $v_{-i}v_{-i-l}$, an edge of $P(n,n-l)$. $\square$

Checked: the identity $(j+l)k-(jk+1)=lk-1$ symbolically (sympy) and the full edge check for $11\le n\le 60$, $\gcd(n,5)=1$ (results/t1_graph_invariants.json, column P6_isomorphism_ok; results/lemma_checks.json).

Consequence for $k=5$. The partner $l'=\min(l,n-l)\le4$ exactly for $n\in{11,14,16,19,21}$ ($5l'\equiv\pm1\pmod n$ with $l'\le4$ means $n\mid 5l'\mp1\in{4,6,9,11,14,16,19,21}$). Hence $P(11,5)\cong P(11,2)$, $P(14,5)\cong P(14,3)$, $P(16,5)\cong P(16,3)$, $P(19,5)\cong P(19,4)$, $P(21,5)\cong P(21,4)$. With Krishnan–Ma–Zhang Theorem 1.1 this gives $Z(P(14,5))=Z(P(16,5))=8$ and $Z(P(19,5))=Z(P(21,5))=10$ — values implied by published work, not new (and reproduced by brute force below).

# P7. The uniform upper bound 12

Statement. For every $n\ge12$, $S={u_0,\dots,u_{11}}$ is a zero-forcing set of $P(n,5)$; hence $Z(P(n,5))\le12$ for all $n\ge11$.

Proof. For $n=12$, $S$ is the whole outer layer; each $u_i$ then has the single white neighbour $v_i$ and the spokes finish. Let $n\ge13$. Phase 1: $u_i\to v_i$ for $i=1,\dots,10$ in order (other neighbours $u_{i\pm1}\in S$ since $0\le i-1$ and $i+1\le11$). Then $v_5\to v_0$ (neighbours of $v_5$: $u_5$, $v_{10}$, $v_0$; the first two are black) and $v_6\to v_{11}$ (neighbours $u_6,v_1,v_{11}$). Now columns $0,\dots,11$ are entirely black and columns $12,\dots,n-1$ entirely white (column $n-1\ne 11$ because $n\ge13$). Phase 2: for $j=12,\dots,n-1$ perform $u_{j-1}\to u_j$ and then $v_{j-5}\to v_j$. Invariant before stage $j$: columns $<j$ black, columns $\ge j$ white. The neighbours of $u_{j-1}$ are $u_{j-2},v_{j-1}$ (columns $<j$, black) and $u_j$ (white), so the first force is legal; it leaves $v_j$ white. The neighbours of $v_{j-5}$ are $u_{j-5}$ and $v_{j-10}$ (columns $j-5\ge7$ and $j-10\ge2$, both $<j$ and $\ge0$, black) and $v_j$, so the second force is legal and completes column $j$. After $j=n-1$ all vertices are black. For $n=11$, $Z=6<12$. $\square$

This bound is Alameda et al. (2018), Theorem 2.2, and Rashidi et al. (2020), Theorem 2.2; the column-by-column proof is the $k=4$ argument of Krishnan–Ma–Zhang adapted to $k=5$. Checked: the chronology replays by code/closure_oracle.py for $13\le n\le 48$ (code/verify_upper_bounds.py).

# P8. First-force boundary lemma (Krishnan–Ma–Zhang Lemma 2.1)

Statement. If 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 $|\partial X|\le|S|$.

Proof. A vertex forces at most once: after $b\to w$, all neighbours of $b$ are black and remain so. Hence the first $p$ forces have $p$ distinct sources, $|X|=p$. Let $B$ be the black set after these $p$ forces; $|B|=|S|+p$. Each $b\in X$ was black when it forced and its whole neighbourhood was black immediately after, so $N[X]\subseteq B$ and $\partial X\subseteq B\setminus X$, giving $|\partial X|\le|B|-|X|=|S|$. $\square$

# P9. Column deletion (Krishnan–Ma–Zhang Lemma 2.2, written out for $k=5$)

Statement. Let $n\ge13$ and $X\subseteq V(P(n,5))$ such that columns $0,1,\dots,10$ contain no vertex of $X$. Delete column $5$ and reindex the surviving columns in cyclic order by $f(i)=i$ for $i<5$, $f(i)=i-1$ for $i>5$, preserving layers. Then the image $X'\subseteq V(P(n-1,5))$ satisfies $|X'|=|X|$ and $|\partial X'|=|\partial X|$.

Proof. $f$ is a bijection from the surviving columns ${0,\dots,n-1}\setminus{5}$ onto ${0,\dots,n-2}$, hence (with layers preserved) a bijection $V(P(n,5))\setminus{u_5,v_5}\to V(P(n-1,5))$, so $|X'|=|X|$. Fix an occupied column $i$ (so $11\le i\le n-1$) and a neighbour offset $d\in{-5,-1,1,5}$ (outer vertices use $d=\pm1$, inner ones $d=\pm5$; spokes stay in the column). Put $q=i+d$, so $6\le q\le n+4$. Case $q<n$: the neighbour column is $q\ne5$ (as $q\ge6$), it survives, and $f(q)=q-1=f(i)+d$ is its neighbour column in $P(n-1,5)$ (no wrap-around is needed since $0\le q-1\le n-2$). Case $q\ge n$: the neighbour column is $q-n\in{0,\dots,4}$, which survives and is fixed by $f$; in $P(n-1,5)$ the neighbour of column $f(i)=i-1$ at offset $d$ is $(i-1+d)\bmod(n-1)=(q-1)\bmod(n-1)=q-n$ because $n-1\le q-1\le n+3<2(n-1)$. So no neighbour of $X$ is deleted and $f$ maps $N[X]$ onto $N[X']$ provided the converse also holds: for an image column $j=f(i)$ ($10\le j\le n-2$) and offset $d$, if $j+d\le n-2$ then $j+d\ge5$ lifts to $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}$, which equals $(i+d)\bmod n=i+d-n$, again a neighbour of $i$. Spokes are preserved. Hence $f(N[X])=N[X']$, and by injectivity $f(\partial X)=\partial X'$ and $|\partial X'|=|\partial X|$. $\square$

Checked (T8): 5600 random instances with $14\le n\le 40$ (results/lemma_checks.json): the map preserved $|X|$ and $|\partial X|$ in every case.

# 3. Lower-bound machinery for $k=5$

Write $\beta_p(n)=\min{|\partial X|: X\subseteq V(P(n,5)),\ |X|=p}$.

# Lemma 3.1 (from boundary to zero forcing).

Let $p\ge1$ and $n\ge\lceil (p+11)/2\rceil$. If $\beta_p(n)\ge12$ then $Z(P(n,5))\ge12$.

Proof. Suppose $S$ is zero forcing with $|S|\le11$. Every chronology from $S$ ending at $V$ performs $2n-|S|\ge2n-11\ge p$ forces (the last inequality is $n\ge(p+11)/2$). By P8 the sources $X$ of the first $p$ forces satisfy $|X|=p$ and $|\partial X|\le|S|\le11$, so $\beta_p(n)\le11$. $\square$

# Lemma 3.2 (finite reduction).

Let $p\ge1$, $c_{\max}=\lfloor(p+11)/2\rfloor$ and $N_{\max}=11c_{\max}$. If $\beta_p(n)\le11$ for some $n>N_{\max}$, then $\beta_p(m)\le11$ for every $m$ with $N_{\max}\le m\le n$; in particular for $m=N_{\max}$.

Proof. Let $|X|=p$, $|\partial X|\le11$ in $P(n,5)$, $n>N_{\max}\ge 13$. Let $C$ be the set of occupied columns, $c=|C|$. In an occupied column with exactly one vertex of $X$, the other vertex is in $\partial X$ (spoke). The number of such columns is at least $2c-p$ (each column holds at most two vertices of $X$, so $p\le 2c-(\text{number of singly occupied columns})$). Hence $2c-p\le|\partial X|\le11$ and $c\le c_{\max}$. The $c$ occupied columns cut the cycle of columns into $c$ cyclic gaps of empty columns, of total length $n-c>11c_{\max}-c\ge10c$, so some gap contains at least $11$ consecutive empty columns. Rotating ($\rho$ is an automorphism, boundaries are preserved) so that these are columns $0,\dots,10$, Lemma P9 produces $X'\subseteq V(P(n-1,5))$ with $|X'|=p$ and $|\partial X'|\le11$. Repeat while $n-1>N_{\max}$. $\square$

The sympy script verifies the integer arithmetic ($c\le c_{\max}\iff 2c-p\le11$; $2n-11\ge p\iff n\ge\lceil(p+11)/2\rceil$) for $12\le p\le30$ (results/lemma_checks.json, "L2_counting").

# Lemma 3.3 (what a finite window proves).

Let $p\ge1$ and $n_1\le N_{\max}$. If $\beta_p(n)\ge12$ for every $n$ with $n_1\le n\le N_{\max}$, then $\beta_p(n)\ge12$ for every $n\ge n_1$, and hence (Lemma 3.1) $Z(P(n,5))\ge12$ for every $n\ge\max(n_1,\lceil(p+11)/2\rceil)$.

Proof. For $n>N_{\max}$, a violation would propagate to $m=N_{\max}$ by Lemma 3.2, contradicting the hypothesis at $m=N_{\max}\ge n_1$. $\square$

# Lemma 3.4 (the boundary formulas and their correctness).

For fixed $n,p$ let $\mathcal F(n,p)$ be the CNF over variables $x_w,z_w$ ($w\in V$) and auxiliary counter variables with clauses: $(x_w\vee\neg x_t\vee z_w)$ for every edge $tw$ (both orientations), $(\neg z_w\vee\neg x_w)$, the sequential-counter encoding of $\sum_w x_w=p$ and of $\sum_w z_w\le11$, and the clause $(x_{u_0}\vee x_{v_0})$. Claim: $\mathcal F(n,p)$ is satisfiable iff $\beta_p(n)\le11$.

Proof. ($\Leftarrow$) Take $X$ with $|X|=p$, $|\partial X|\le11$; by rotation (an automorphism, preserving $|X|$ and $|\partial X|$) assume column $0$ is occupied. Set $x_w=[w\in X]$, $z_w=[w\in\partial X]$ and extend to the counter variables as Sinz's encoding prescribes (the encoding is satisfiable exactly when the cardinality constraint holds; sequential counters are complete in this sense [sinz2005cardinality]). The edge clauses hold: if $x_t$ and $\neg x_w$ then $w\in\partial X$. ($\Rightarrow$) From a model, put $X={w:x_w}$, so $|X|=p$. For $w\in\partial X$ pick $t\in N(w)\cap X$; the clause $(x_w\vee\neg x_t\vee z_w)$ forces $z_w$. Hence $\partial X\subseteq{w:z_w}$ and $|\partial X|\le\sum z_w\le11$. $\square$

Thus an UNSAT certificate for $\mathcal F(n,p)$ proves $\beta_p(n)\ge12$, and a model exhibits an explicit $p$-set of boundary $\le11$ (which the driver re-checks by direct counting).

# Lemma 3.5 (the fort-cover formulas).

For fixed $n$ and bound $b<2n$, let $\mathcal G(n,b)$ be the CNF over seed variables $s_w$ with: the 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$ (every listed set is verified to be a fort by the independent checker). Claim: if $Z(P(n,5))\le b$ then $\mathcal G(n,b)$ is satisfiable. Hence UNSAT proves $Z(P(n,5))\ge b+1$.

Proof. Let $S$ be zero forcing with $|S|\le b<2n$. $S\ne V$, so some first force $x\to y$ exists; at that moment the black set is exactly $S$, so $x\in S$, $y\notin S$ and the two other neighbours of $x$ are in $S$. The directed edges of $P(n,5)$ fall into four orbits under $D_n$ (outer edges in either direction: rotation and reflection; spokes outward; spokes inward; inner edges in either direction), with the four representatives listed. Choose $\varphi\in D_n$ with $\varphi(x\to y)$ equal to a representative; $\varphi S$ is zero forcing of the same size (P3) and its first force can be $\varphi x\to\varphi y$. Set $s_w=[w\in\varphi S]$ and the matching selector; every fort clause holds by P2 ($\varphi S$ meets every fort). The counter encoding is satisfiable since $|\varphi S|\le b$. $\square$

Note that the stored list $\mathcal L$ may contain any forts (in particular all dihedral images of each fort found, since automorphisms map forts to forts: the fort condition is a statement about neighbourhood counts, which are preserved). The lazy loop generates forts as white remainders of stalled closures (P2, $\Leftarrow$), shrunk greedily to a minimal sub-fort; the shrinking only ever keeps sets verified to be forts.

# 4. Computational results and certificates

All numbers below are read from the artifacts named in parentheses; nothing is extrapolated.

# 4.1 Exhaustive values (code/brute_force.c, results/brute_force_runs.jsonl, results/brute_force_values.json)

The C oracle enumerates every $s$-subset of $V(P(n,5))$ by Gosper's hack, keeps the subsets that are the minimum of their $D_n$-orbit (P3), and computes the closure by bit operations. For each $n$ it exhausts $s=1,2,3,\dots$ until a forcing representative appears (sizes $1,2,3$ were run in a separate pass for $11\le n\le26$; no forcing set exists, as also follows from the published bound $Z\ge\min{5,\lfloor n/5\rfloor}+1\ge4$ for $n\ge15$ and from the fort-cover certificates for $n\le22$).

(Exact counts for every $(n,s)$ are in results/tables/brute_force.csv.) The values at $n=11,14,16,19,21$ agree with the literature (Rashidi et al. Thm 2.6 and Krishnan 2026 for $n=11$; P6 plus Krishnan–Ma–Zhang Thm 1.1 for the others); $n=24$ agrees with the reported Alameda et al. value. Rashidi's bounds 8, 10, 11 at $n=12,13,14$ are attained only at $n=12$.

# 4.2 Boundary table (code/run_boundary_table.py, results/boundary_table.jsonl)

For $12\le p\le24$ and $13\le n\le30$ the exact $\beta_p(n)$ when $\le11$, else "$\ge12$" (results/tables/boundary_table.csv). The relevant rows:

Every $p\le24$ fails at $n=25$: with $p=18$, $X={v_i: i\equiv0,1,2\ (5)}\cup{u_i:i\equiv1\ (5)}$ minus two vertices, or (for $p=20$) the three inner pentagons ${v_i:i\equiv0,1,2\pmod5}$ together with $u_1,u_6,u_{11},u_{16},u_{21}$, has boundary ${u_0,u_2,u_5,u_7,u_{10},u_{12},u_{15},u_{17},u_{20},u_{22}}$ of size 10. The inner pentagons exist only for $n=25$ (inner cycles have length $n/\gcd(n,5)\ge6$ for $n\ge26$, $n\ne25$). The smallest $p$ with $\beta_p(n)\ge12$ on all of $24,26,\dots,30$ is $p=18$ (rule L4); $p=24$ fails at $n=26$. Decision: $p=18$, $n_1=26$, $c_{\max}=\lfloor29/2\rfloor=14$, $N_{\max}=154$.

# 4.3 Certified window (code/run_boundary_window.py, results/boundary_certificates.jsonl, code/proofs/certificates/boundary/)

For every $n\in{24}\cup{26,27,\dots,154}$ the formula $\mathcal F(n,18)$ (Lemma 3.4) was found unsatisfiable by CaDiCaL 1.9.5 (python-sat 1.9.dev17) with DRAT proof logging, and each proof was verified by drat-trim (source SHA-256 d834b649…a0c2ee, built from the GitHub revision fetched on 2026-10-30) with output s VERIFIED and exit code 0 — 130 certificates in total (129 in the window plus $n=24$). Sizes: the CNF for $n=154$ has the numbers of variables and clauses recorded in results/tables/boundary_window_p18.csv; per-instance solve times range from 17 s to 267 s (mean 101 s) and drat-trim times from 13 s to 231 s (total 11,701 s); proofs have between 1.2 and 4.9 million lines (346.5 million lines, 37 GB on disk in total; SHA-256 of every CNF and proof is in the record; they can be regenerated by code/run_boundary_window.py 18 26 154). The independent checker code/verify_lower_bounds.py rebuilds each CNF from the graph definition, compares the sorted clause multiset byte-for-byte with the stored DIMACS file, checks both hashes and re-runs drat-trim (results/lower_bound_verification.json). Five additional certificates with $p=20$ at $n=26..30$ were produced and verified as a cross-check and are not used in the proof.

# 4.4 Fort-cover and round-encoding SAT paths (code/run_exact.py, results/lower_bound_certificates.jsonl, results/solver_runs.jsonl)

Independently of the brute force, the fort-cover formulas $\mathcal G(n,Z-1)$ (Lemma 3.5) were refuted with DRAT certificates (CaDiCaL, checked by drat-trim and re-checked by verify_lower_bounds.py including the vertex-by-vertex fort validity of every stored fort) for $n=11,\dots,22$, and the round-based encoding (Glucose 4.1, P4) returned UNSAT at $s=Z-1$ for $n=11,\dots,16$ and timed out (600 s, recorded as unknown) for the larger $n$ where it was tried. The three paths agree wherever all finished; no disagreement occurred. (Status per $n$: results/exact_values.csv.)

# 4.5 Holdout (plan/conjectures.jsonl, results/holdout_results.jsonl)

Conjectures C1–C4 were registered at 2026-10-30T18:00:31Z from the data for $n\le30$, predicting $Z=12$ at every holdout $n\in{32,35,37,41,44,48}$. Afterwards: the certified window supplies $\beta_{18}(n)\ge12$ hence $Z\ge12$ at each holdout $n$; P7 gives $\le12$; and a time-limited fort-cover search for an 11-vertex forcing set (600 s per $n$) found none. All six predictions are correct.

# 5. Main theorem

Theorem 5.1. Let $k=5$. Then $$Z(P(n,5))=\begin{cases}6&n=11,\8&n=12,\9&n=13,\8&n=14,15,16,\10&n=17,18,19,20,21,\11&n=22,\12&n\ge23.\end{cases}$$ In particular the stabilization threshold is exactly $n_0=23$.

Proof.

1. Upper bounds. For $n\ge23$ (indeed $n\ge12$), $Z\le12$ by P7. For $11\le n\le22$ the explicit witnesses of §4.1 (stored with full chronologies in results/upper_bound_witnesses.jsonl, replayed by the independent checker code/verify_upper_bounds.py) give $Z\le$ the stated value.

2. Lower bounds for $11\le n\le 26$. By §4.1 the exhaustive enumeration found no zero-forcing set of size $Z-1$ (one representative per $D_n$-orbit; sound by P3), so $Z\ge$ the stated value for $n=11,\dots,27$. For $n=11,\dots,22$ the DRAT-certified fort-cover refutations of §4.4 give the same lower bounds by Lemma 3.5 and P2, independently of the enumeration.

3. Lower bound 12 for $n\ge26$. By §4.3, $\mathcal F(n,18)$ is unsatisfiable for all $26\le n\le154$, so by Lemma 3.4 $\beta_{18}(n)\ge12$ on that window. With $p=18$: $c_{\max}=14$, $N_{\max}=154$, so Lemma 3.3 gives $\beta_{18}(n)\ge12$ for every $n\ge26$, and since $26\ge\lceil(18+11)/2\rceil=15$, Lemma 3.1 gives $Z(P(n,5))\ge12$ for every $n\ge26$. (At $n=24$ the certificate also gives $Z\ge12$ directly, and at $n=26$ the enumeration agrees.)

4. $n=23,24,25$. Step 2 gives $Z\ge12$ (sizes $\le11$ exhausted, Table 4.1); with step 1, $Z=12$.

5. Sharpness. $Z(P(22,5))=11<12$ by steps 1–2, so the threshold cannot be lowered. $\square$

What is machine-checked and what is human-proved. Human-proved for all $n$: P1–P9 and Lemmas 3.1–3.5. Machine-checked finite inputs: (a) the 129 DRAT certificates of §4.3 (external checker drat-trim, independent CNF rebuild); (b) the exhaustive enumerations of §4.1 for $n\le27$ (C program, cross-validated against a Python reference without symmetry reduction on P(5,2) and P(11,5), and against the DRAT-certified fort-cover path for $n\le22$); (c) the replayed chronologies of all witnesses. No step uses the shape of the table for $n\le30$ to infer anything about larger $n$.

Novelty (qualified). To our knowledge, the values for $n\in{12,13,15,17,18,20,22,23}$ and the statement $Z(P(n,5))=12$ for all $n\ge23$ with the sharp threshold are not in the literature; the bound 12, the value at $n=11$, the values at $n=14,16,19,21$ (via P6) and at $24\mid n$ are known or implied by known results. The proof method is that of Krishnan–Ma–Zhang for $k=3,4$, adapted to $k=5$ with $p=18$ and the window $[26,154]$; the obstruction at $n=25$ (inner pentagons) is specific to $k=5$ and forces the separate exhaustive treatment of $n=23,24,25$.

# 6. Numerical and symbolic verification log

code/verify_lemmas.py (results/lemma_checks.json): CS6 boundary identity 5400/5400 random $X$ for $13\le n\le30$; T8 deletion map 5600/5600; P6 identity symbolic and 40 numeric $n$; L2 counting rows $p=12..30$ all consistent; P7 index inequalities. code/graph_constructor.py (T1, 39 graphs), code/closure_oracle.py (T2, 1200/1200).

# 7. Negative results and the boundary of what is proved

• The first-force boundary method cannot certify $n=25$ for any $p\le24$ (§4.2): the three inner pentagons plus five outer vertices have boundary 10. Whether some $p>24$ works at $n=25$ was not tested; it is irrelevant to the theorem 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.
• $p=16$ (the $k=4$ value) fails for infinitely many $n$? Not established: it fails at every $n\le30$ tested and we did not run its window; the statement "$\beta_{16}(n)\le11$ for all $n$" is left open.
• The round-based encoding (P4) is impractical as a lower-bound engine beyond $n\approx16$ (timeouts at 600 s); the fort-cover engine with lazy minimal forts and dihedral images works to $n=22$ but stalled at $n=24$ (more than $10^5$ fort clauses in 300 s). The boundary engine scales to $n=154$ with modest proofs because it never reasons about the forcing process.
• Certificate volume: 37 GB of DRAT proofs. They are reproducible from the generator in minutes per instance; the archive may ship hashes plus the generator rather than the proofs themselves, which is stated as such.
• No Lean formalization was attempted in this stage (Stage G decides); nothing in §5 depends on it.
• Values for $n>154$ are proved (Lemma 3.3), but the per-$n$ enumeration cross-check exists only for $n\le27$ and the fort-cover certificates only for $n\le22$.