# 🔗 Zero-Forcing Bounds for Generalized Petersen Graphs

UQO Working Paper No. 32 — Computational Discovery and Certified Proofs for P(n,5)

TL;DR — The zero forcing number of the generalized Petersen graph P(n,5) is determined for every n ≥ 11: Z = 6, 8, 9, 8, 8, 8, 10, 10, 10, 10, 10, 11 for n = 11…22 and Z = 12 for all n ≥ 23 (sharp threshold n₀ = 23). Upper bound: the published 2k+2 construction. Lower bound for n ≥ 26: the Krishnan–Ma–Zhang first-force boundary method adapted to k = 5 (parameter p = 18, column-deletion lemma reducing to the window 26 ≤ n ≤ 154, 129 DRAT unsatisfiability certificates verified by drat-trim and rebuilt by an independent checker). The method provably fails at n = 25 (inner pentagons) and p = 16 fails for every n ≥ 22, so n ≤ 27 is settled by two independently written exhaustive enumerators. Pre-registered holdout (6 values of n) confirmed; falsification campaign found no error.

# 📌 Status

# 🎯 What this paper does

The zero forcing number Z(G) is the minimum size of an initially black vertex set from which the colour-change rule (a black vertex with exactly one white neighbour forces it black) colours the whole graph; it bounds the maximum nullity of the symmetric matrices described by G. For generalized Petersen graphs P(n,k) sharp values were known for k = 2 (reported), k = 3 and k = 4 (2026), and for k = 5 only at n = 11 and n ≡ 0 (mod 24). The paper closes the k = 5 case.

The proof combines (i) the 12-outer-vertex forcing construction (upper bound), (ii) the first-force boundary lemma and a column-deletion lemma for k = 5 that reduce the lower bound 12 for all n ≥ 26 to the finite statement β₁₈(n) ≥ 12 for 26 ≤ n ≤ 154, (iii) one CaDiCaL refutation with DRAT proof per n in the window, each verified by drat-trim and re-verified by an independent checker that rebuilds the CNF from the graph definition, and (iv) exhaustive enumeration with dihedral orbit reduction for n ≤ 27 (cross-validated by a second enumerator through n = 40 and by fort-cover DRAT refutations for n ≤ 23). Every reported number is traceable to a stored result record.

# 🏆 Headline results

# 🗂 Repository layout

zero-forcing-petersen-pn5/
├── paper/                 # UQO WP 32: main.tex + sections/ + appendix/ + tables/ + figures/ + references.bib → main.pdf
├── manuscript/            # ORIGINAL AutoScholar manuscript (autoscholar.cls, main.tex, main.pdf, metadata.json, abstract.md)
├── code/                  # graph constructors, closure oracle, two C enumerators, SAT drivers, independent checkers,
│   │                      # figure/table generators, reproduce.sh, requirements.txt, wheels/, tools/drat-trim/
│   └── proofs/            # handwritten/ (step-numbered proofs), lean/ (not attempted), certificates/{boundary,fortcover}
├── results/               # metrics.json, robustness.md, tables/*.csv|*.tex, figures/*.pdf, result records
├── plan/                  # pre-registered research plan + feasibility (conjecture registry, frozen holdout)
├── review/                # automated referee report (round 1), revisions, QA report (24 gates)
├── provenance/            # run-summary.json (model, cost, toolchain), checksums.sha256
├── sources/               # verified bibliography (20 sources, Crossref/OpenAlex/arXiv identifiers), claim→source map
├── data/manifest.json     # no observational or synthetic data; literature full texts and wheels are the only inputs
├── docs/TRANSFER-NOTE.md  # how AS-WP-2026-0001 became UQO WP 32
└── requirements.txt       # = code/requirements.txt (python-sat 1.9.dev17, sympy 1.14, six, mpmath)

paper/tables/*.tex and paper/figures/*.pdf are copies of results/tables/tab_*.tex and results/figures/*.pdf (regenerated by code/build_manuscript_tables.py and code/build_figures.py).

# 🚀 Quick start

# dependencies into .pydeps from the archived wheels (no network), then build drat-trim and the C enumerators
python3 -m pip install --no-index --target .pydeps code/wheels/*.whl
QUICK=1 bash code/reproduce.sh        # ~10 min: re-verify shipped certificates, robustness checks
bash code/reproduce.sh                # ~25 min on 16 cores: oracle n ≤ 22, boundary table p = 16..20, window n ≤ 40 with fresh proofs
FULL=1 bash code/reproduce.sh         # several hours: everything, incl. the complete window 26..154
cd paper && make                      # latexmk → main.pdf (pdflatex + bibtex, aer.bst)

Reproduction runs in a working copy under results/reproduction/work/; the shipped artifacts are never modified and the comparison is written to results/reproduction/summary.json. Original run: Python 3.14.7, PySAT 1.9.dev17 (CaDiCaL 1.9.5, Glucose 4.1), drat-trim built from source, gcc -O2, one Apple Silicon node (16 cores).

# 🗃 Data

No external data set. Every graph P(n,5) is generated from the definition by code/graph_constructor.py (two independent constructors, canonical edge lists with SHA-256 digests). Inputs consumed by the run: the open-access full texts of the cited papers and the archived Python wheels (data/manifest.json).

# 🔬 Methodology

1. Foundational propositions proved in full (order independence, fort characterization, orbit reduction, graph facts, isomorphism P(n,k) ≅ P(n,l) for kl ≡ 1) — paper/sections/preliminaries.tex, code/proofs/handwritten/.
2. Upper bound: 12 consecutive outer vertices force P(n,5) for n ≥ 12 (verify_upper_bounds.py replays every witness).
3. Lower bound: first-force boundary lemma + column deletion for k = 5 → finite window; SAT encodings with correctness lemmas (sat_or_ilp_solver.py).
4. Certificates: CaDiCaL + DRAT, drat-trim, independent rebuild of every CNF (run_boundary_window.py, verify_lower_bounds.py).
5. Exhaustive oracles: brute_force.c (D_n orbit reduction) and robustness/ff_brute (first-force normalization).
6. Pre-registration, holdout and falsification campaign (plan/, results/robustness.md, check_exceptional_automorphisms.py).

# 🖼 Figures & tables inventory

Tables (paper/tables/): tab_paths (lower-bound paths per n), tab_brute_force, tab_exact_values, tab_conjectures, tab_verification, tab_scope (A1), tab_witnesses (A2), tab_boundary_table (A3), tab_fortcover (A4), tab_window_scaling (A5).

# ⚠️ Limitations

• For n > 40 the lower bound rests on one certified path; for n > 154 only on the proved (not formalized) deletion lemma.
• No Lean 4 formalization; "verified" means drat-trim + independent re-implementation, never proof-assistant verified.
• DRAT proofs (39 GB in the original run; 8.8 GB shipped locally for the window) are not in git; digests are in the result records.
• Z(P(24r,5)) = 12 is cited second-hand (primary text not accessible to the pipeline).
• The two C enumerators are cross-validated but not formally proved correct; heuristic attacks are evidence only in the heuristic sense.

# 📝 Citation

@techreport{boucher2026zeroforcing,
  author      = {Boucher, Simon-Pierre},
  title       = {Zero-Forcing Bounds for Generalized Petersen Graphs: Computational Discovery and Certified Proofs for $P(n,5)$},
  institution = {Universit\'e du Qu\'ebec en Outaouais, D\'epartement des sciences administratives},
  type        = {Working Paper},
  number      = {32},
  year        = {2026},
  month       = {October},
  note        = {First released as AutoScholar Working Paper AS-WP-2026-0001}
}

# 👤 Author & contact

Simon-Pierre Boucher — Département des sciences administratives, Université du Québec en Outaouais (UQO), Gatineau, QC. 📧 simon-pierre.boucher@uqo.ca

# 🗒 Notes

• Provenance. The research was executed autonomously by the AutoScholar.ai pipeline (run 951263fc-5b4f-4db3-8660-153a5f5ec04a, attempt 4, model claude-fable-5-1, 15/15 hard QA gates) under a brief written by the author; the UQO edition changes only the typesetting. The original manuscript is kept in manuscript/ because code/reproduce.sh and provenance/checksums.sha256 refer to it.
• Deviations from HARMONISATION.md. Code lives in code/ (flat layout expected by reproduce.sh, PYTHONPATH=.pydeps:code) instead of scripts/+src/; artifact directories plan/, review/, provenance/, sources/, manuscript/ are kept at the root; the JEL field carries MSC 2020 codes as well (pure mathematics).
• Appendix tables are numbered A1–A5 (the AutoScholar edition continued the main numbering 7–11).