Sharp zero forcing numbers for the generalized Petersen graphs $P(n,3)$ and $P(n,4)$

Abstract

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.