Research you can check, not just read.

Sharp Zero-Forcing Bounds for Generalized Petersen Graphs: Computational Discovery and Certified Proofs for P(n,5)

The zero forcing number Z(G) of a graph is the minimum size of a set of initially black vertices from which the colour-change rule (a black vertex with exactly one white neighbour forces that neighbour black) eventually colours the whole graph; it bounds the maximum nullity of the matrices described by G. For the generalized Petersen graphs P(n,k) the sharp values were, to our knowledge, reported for k=2 (with independent confirmation only for n≤ 16), proved for k=3 and k=4 (2026), and known for k=5 only at n=11 and at n≡ 0(mod 24). We determine Z(P(n,5)) for every n≥ 11: the values are 6,8,9,8,8,8,10,10,10,10,10,11 for n=11,…,22, and Z(P(n,5))=12 for all n≥ 23, so the stabilization threshold is exactly n_0=23. The upper bound 12 is the published 2k+2 construction. The lower bound for all n≥ 26 follows the first-force boundary method of Krishnan, Ma and Zhang, adapted to k=5: we prove that the minimum boundary of an 18-vertex set in P(n,5) is at least 12 for every n≥ 26 by a column-deletion lemma that reduces the statement to the finite window 26≤ n≤ 154, which is settled by 129 unsatisfiability certificates in DRAT format, each verified by the external checker drat-trim and rebuilt from the graph definition by an independent checker. The method provably fails at n=25 for every parameter p≤ 24 (two inner pentagons give an obstruction), so n=23,24,25 and all n≤ 22 are settled by exhaustive enumeration with dihedral orbit reduction, cross-validated by a second, independently written enumeration based on first-force normalization (through n=40) and, for n≤ 23, by DRAT-certified fort-cover refutations. We also show that the k=4 parameter p=16 cannot work for k=5 at any n≥ 22, that the certified bound has zero slack, and that a pre-registered holdout of six values of n confirmed the registered conjectures. All proofs are written out; all certificates, code and a reproduction script are released.