Papers With

← All papers
First page of Sharp zero forcing numbers for the generalized Petersen graphs $P(n,3)$ and $P(n,4)$

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

Arnav Krishnan, Haobo Ma, Wenlin Zhang

math.CO Oct 16, 2026 · v1
formalization mathlib combinatorics
Read PDF arXiv abstract Code
TL;DR
The k=3 stabilization theorem Z(P(n,3))=8 for n≥13 is formalized in Lean 4 with Mathlib, modeling P(n,3) as a simple graph on Bool×Fin n.
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.
Problem

The goal is to determine the zero forcing numbers of the generalized Petersen graphs P(n,3) and P(n,4) for all n. A central case is Krishnan's Conjecture 5, which states that Z(P(n,3))=8 for all n≥13.

Approach

A zero forcing set yields the sources of its first forces, and these form a vertex set with small external boundary. Deleting a column inside an empty interval of columns preserves the boundary, which reduces the problem to finite checks. For k=3 the finite checks run over gap words and layer assignments, using a C checker, and the stabilization theorem is formalized in Lean 4 with Mathlib. For k=4 the finite checks use 89 boundary SAT formulas and 11 fort formulas, each with a DRAT certificate, plus explicit forcing sequences.

Results

Z(P(n,3))=8 for all n≥13 and Z(P(n,4))=10 for all n≥18, and both thresholds are sharp. Exact values are given for all smaller admissible n. Only the k=3 result is Lean-formalized; the k=4 formalization is left to future work.

n789101112
Z(P(n,3))666877
Small values of Z(P(n,3))