arXiv++ Combinatorics

We prove that $Z(P(n,3))=8$ for every $n\ge13$ and $Z(P(n,4))=10$ for every $n\ge18$, with both stabilization thresholds sharp, and give the exact values for all smaller admissible $n$. The first equality proves Krishnan's Conjecture 5; his Proposition 4 supplies its upper bound. The lower bounds use the external boundary of the first forcing sources: ten vertices have boundary at least eight in $P(n,3)$ for $n\ge14$, and sixteen vertices have boundary at least ten in $P(n,4)$ for $n\ge20$. Deletion within an empty column interval reduces these assertions to finite checks, and forts settle the remaining cases. The $k=3$ stabilization theorem has a Lean 4 formalization; the $k=4$ proof uses 89 boundary formulas and 11 fort formulas with separately checked DRAT certificates, together with explicit forcing sequences.

Rashidi, Shajareh Poursalavati, and Tavakkoli [J. Algebra Comb. Discrete Struct. Appl. 7 (2020), no.2, 183-193, Theorem 3.6] claim $Z(P(n,3)) = 8$ for all $n \geq 12$, but this fails at $n = 12$, where $Z(P(12,3)) = 7$. We give an explicit $7$-vertex zero forcing set for $P(12,3)$ and its forcing sequence, and verify by exhaustive search that no $6$-vertex set forces $P(12,3)$. We prove $Z(P(n,3)) \le 8$ for $n \ge 9$ using an explicit forcing set and rotational symmetry. Exhaustive search yields $Z(P(n,3))$ for $7 \le n \le 20$ and identifies the gap in the published proof: its case analysis fails to exclude $7$-vertex sets. We conjecture $Z(P(n,3)) = 8$ for $n \ge 13$, requiring a matching lower bound for all large $n$.