UQO Working Papers · WP32 · v1.0
Zero-Forcing Bounds for Generalized Petersen Graphs: Computational Discovery and Certified Proofs for P(n,5)
- Year
- 2026
- First release
- October 2026
- Latest revision
- October 2026
- Publication status
- Working paper
Z(P(n,5)) = 12 for all n ≥ 23, and the threshold is sharp
The k = 5 case is closed: values 6, 8, 9, 8, 8, 8, 10, 10, 10, 10, 10, 11 for n = 11–22, then 12 forever, certified by 129 externally checked DRAT refutations and two independent exhaustive enumerators.
Abstract
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 reported for k = 2, proved for k = 3 and k = 4 (2026), and known for k = 5 only at n = 11 and at n ≡ 0 (mod 24). This paper determines 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₀ = 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: 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.
The paper also shows that the k = 4 parameter p = 16 cannot work for k = 5 at any n ≥ 22, that the certified bound has zero slack (β₁₈(n) = 12 exactly for 26 ≤ n ≤ 40), 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 one-command reproduction script are released. The work was first produced by the author's AutoScholar.ai autonomous research pipeline and is reissued unchanged in content as a UQO working paper.
Key findings
n₀ = 23
sharp threshold: Z = 12 for all n ≥ 23
129
DRAT certificates for 26 ≤ n ≤ 154, drat-trim verified
8
new exact values of n between 12 and 23
432 billion
subsets enumerated exhaustively in 4,126 s on 16 threads
39.0 GB
of DRAT proofs in the original run, digests recorded
6 / 6
pre-registered holdout values confirmed as 12
Scientific contributions
- The k = 5 case closed
- Z(P(n,5)) is determined for every n ≥ 11; the values at n ∈ {12, 13, 15, 17, 18, 20, 22, 23}, the statement Z = 12 for all n ≥ 23 and the sharpness of n₀ = 23 are new.
- Boundary method adapted to k = 5
- The parameter p = 18 is shown to be the smallest that works; p = 16 (used for k = 4) fails for every n ≥ 22, and no p ≤ 24 works at n = 25, where two inner pentagons give an 18-set of boundary 10.
- A finite window closed by certificates
- A column-deletion lemma reduces the lower bound for all n ≥ 26 to 26 ≤ n ≤ 154; each of the 129 instances is refuted by CaDiCaL with a DRAT proof checked by drat-trim and re-verified by an independent checker that rebuilds the CNF from the graph definition.
- Certified table with explicit status
- Every value for 11 ≤ n ≤ 48 has an upper-bound witness replayed by an independent program and a lower bound supported by an externally checkable or exhaustive argument; the three-valued status (fully certified / solver-supported / candidate) is never collapsed.
- A falsification campaign found no error
- Pre-registered holdout H = {32, 35, 37, 41, 44, 48}, a second exhaustive enumerator (344 billion sets) by a different reduction principle, exhaustive validation of the SAT encodings on small instances, negative controls for the proof checker and heuristic attacks on the theorem.
Methodology
Methodology (5)
Foundational propositions proved in full
Order independence of the closure, the fort characterization, dihedral orbit reduction, graph facts and the isomorphism P(n,k) ≅ P(n,l) for kl ≡ 1 (mod n), each with a step-numbered written proof.
Upper bound by explicit witnesses
Twelve consecutive outer vertices force P(n,5) for n ≥ 12 (the 2k + 2 construction); every witness is replayed by an independent program.
First-force boundary lower bound and SAT encodings
The boundary lemma with p = 18 and a column-deletion lemma reduce the lower bound to a finite window; two SAT encodings with correctness lemmas are refuted by CaDiCaL with DRAT proofs.
Exhaustive enumeration with symmetry reduction
A C enumerator with D_n orbit reduction settles n ≤ 27 (unavoidable at n = 25), cross-validated by a second enumerator using first-force normalization and by fort-cover DRAT refutations.
Pre-registration and falsification
Conjectures and a six-value holdout were frozen before fitting; negative controls, stress tests of the deletion lemma and simulated-annealing attacks were run against the theorem.
Research data
- Graph instances generated from the definition
- No external data: every P(n,5) is built by two independent constructors with canonical SHA-256-digested edge lists; the exhaustive oracle enumerated 432,226,268,255 subsets (4,125.7 s wall-clock, 16 threads) for n ≤ 27 and the second enumerator 344 billion sets through n = 40.
- Certificate corpus
- 129 DRAT unsatisfiability certificates for the boundary window 26 ≤ n ≤ 154 plus one at n = 24 (solve times 17–267 s, 346,502,796 proof lines, 39.0 GB; largest CNF 14,323 variables and 28,933 clauses), 14 fort-cover certificates for n ≤ 23, and DIMACS files, fort lists and digests shipped with the archive.
- Solver and verification records
- Every solver run is a JSON record with UTC time, graph digest, method, bound, solver version, wall time, timeout flag and certificate SHA-256 (results/*.jsonl); independent-checker verdicts are stored for all 135 boundary and 14 fort-cover certificates.
Reproducibility
- One-command script code/reproduce.sh with QUICK (10 min), default (25 min on 16 cores) and FULL (several hours, complete window 26–154) modes; shipped artifacts are never modified
- Certificates re-verified with drat-trim and an independent checker that rebuilds each CNF from the graph definition; proofs absent from disk are reported as skipped, never as verified
- Pre-registered plan, frozen holdout, conjecture registry and robustness report in plan/ and results/; provenance checksums for every artifact
- Full LaTeX source of the 36-page paper plus the original AutoScholar manuscript (AS-WP-2026-0001); no Lean formalization is claimed
Research artifacts
Version history
| Version | Date | Description | File |
|---|---|---|---|
| v1.0current | October 2026 | Current manuscript as published on www.spboucher.ai (revised edition after the 2026-10-17 scientific review for papers 1–17). | PDF · 36 p. |