1<!-- Author: Simon-Pierre Boucher — simon-pierre.boucher@uqo.ca -->2# 🔗 Sharp Zero-Forcing Bounds for Generalized Petersen Graphs34**UQO Working Paper No. 32** — *Computational Discovery and Certified Proofs for P(n,5)*56[-b31b1b?logo=latex&logoColor=white)](paper/main.pdf)7[](requirements.txt)8[](code/proofs/certificates/)9[](code/reproduce.sh)10[](https://www.autoscholar.ai)11[](https://uqo.ca)12[](mailto:simon-pierre.boucher@uqo.ca)1314> **TL;DR** — The zero forcing number of the generalized Petersen graph P(n,5) is determined for every n ≥ 11:15> 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).16> Upper bound: the published 2k+2 construction. Lower bound for n ≥ 26: the Krishnan–Ma–Zhang first-force boundary17> method adapted to k = 5 (parameter p = 18, column-deletion lemma reducing to the window 26 ≤ n ≤ 154, 129 DRAT18> unsatisfiability certificates verified by drat-trim and rebuilt by an independent checker). The method provably19> fails at n = 25 (inner pentagons) and p = 16 fails for every n ≥ 22, so n ≤ 27 is settled by two independently20> written exhaustive enumerators. Pre-registered holdout (6 values of n) confirmed; falsification campaign found no error.2122---2324## 📌 Status2526| Item | Value |27|---|---|28| Version | 1.0 (October 2026) |29| Origin | AutoScholar Working Paper **AS-WP-2026-0001** v1 (2026-10-30), produced by the author's AutoScholar.ai autonomous research pipeline (Claude Fable 5.1, worker M4M64c); reissued unchanged in content as UQO WP 32 (see `docs/TRANSFER-NOTE.md`) |30| SSRN | not yet submitted |31| Journal | — (candidates: *Linear Algebra and its Applications*, *Discrete Applied Mathematics*, *Electronic Journal of Combinatorics*) |32| Code & data | no external data; everything regenerable from `code/` (`code/reproduce.sh`, three modes); CNF certificates and fort lists shipped, DRAT proofs shipped locally but **not committed** (8.8 GB, regenerable) |3334## 🎯 What this paper does3536The zero forcing number Z(G) is the minimum size of an initially black vertex set from which the colour-change rule37(a black vertex with exactly one white neighbour forces it black) colours the whole graph; it bounds the maximum38nullity of the symmetric matrices described by G. For generalized Petersen graphs P(n,k) sharp values were known for39k = 2 (reported), k = 3 and k = 4 (2026), and for k = 5 only at n = 11 and n ≡ 0 (mod 24). The paper closes the40k = 5 case.4142The proof combines (i) the 12-outer-vertex forcing construction (upper bound), (ii) the first-force boundary lemma43and a column-deletion lemma for k = 5 that reduce the lower bound 12 for all n ≥ 26 to the finite statement44β₁₈(n) ≥ 12 for 26 ≤ n ≤ 154, (iii) one CaDiCaL refutation with DRAT proof per n in the window, each verified by45drat-trim and re-verified by an independent checker that rebuilds the CNF from the graph definition, and (iv) exhaustive46enumeration with dihedral orbit reduction for n ≤ 27 (cross-validated by a second enumerator through n = 40 and by47fort-cover DRAT refutations for n ≤ 23). Every reported number is traceable to a stored result record.4849## 🏆 Headline results5051| Object | Result |52|---|---|53| Z(P(n,5)), n = 11…22 | 6, 8, 9, 8, 8, 8, 10, 10, 10, 10, 10, 11 (new at n ∈ {12, 13, 15, 17, 18, 20, 22}) |54| Z(P(n,5)), n ≥ 23 | 12 (new: the threshold statement, n₀ = 23 sharp since Z(P(22,5)) = 11) |55| Boundary parameter | p = 18 is the smallest that works; p = 16 fails for every n ≥ 22 (Prop. 7.3) |56| Obstruction | every p ≤ 24 fails at n = 25 (two inner pentagons, boundary 10) |57| Certified window | 129 DRAT certificates, 26 ≤ n ≤ 154 (+ n = 24); solve 17–267 s each, 39 GB of proofs in the original run |58| Zero slack | β₁₈(n) = 12 exactly for 26 ≤ n ≤ 40 |59| Exhaustive oracle | 432 billion subsets enumerated (4 126 s, 16 threads); second enumerator 344 billion sets |60| Holdout | H = {32, 35, 37, 41, 44, 48} frozen before fitting; all six values = 12 as registered |6162## 🗂 Repository layout6364```65zero-forcing-petersen-pn5/66├── paper/ # UQO WP 32: main.tex + sections/ + appendix/ + tables/ + figures/ + references.bib → main.pdf67├── manuscript/ # ORIGINAL AutoScholar manuscript (autoscholar.cls, main.tex, main.pdf, metadata.json, abstract.md)68├── code/ # graph constructors, closure oracle, two C enumerators, SAT drivers, independent checkers,69│ │ # figure/table generators, reproduce.sh, requirements.txt, wheels/, tools/drat-trim/70│ └── proofs/ # handwritten/ (step-numbered proofs), lean/ (not attempted), certificates/{boundary,fortcover}71├── results/ # metrics.json, robustness.md, tables/*.csv|*.tex, figures/*.pdf, result records72├── plan/ # pre-registered research plan + feasibility (conjecture registry, frozen holdout)73├── review/ # automated referee report (round 1), revisions, QA report (24 gates)74├── provenance/ # run-summary.json (model, cost, toolchain), checksums.sha25675├── sources/ # verified bibliography (20 sources, Crossref/OpenAlex/arXiv identifiers), claim→source map76├── data/manifest.json # no observational or synthetic data; literature full texts and wheels are the only inputs77├── docs/TRANSFER-NOTE.md # how AS-WP-2026-0001 became UQO WP 3278└── requirements.txt # = code/requirements.txt (python-sat 1.9.dev17, sympy 1.14, six, mpmath)79```8081`paper/tables/*.tex` and `paper/figures/*.pdf` are copies of `results/tables/tab_*.tex` and `results/figures/*.pdf`82(regenerated by `code/build_manuscript_tables.py` and `code/build_figures.py`).8384## 🚀 Quick start8586```bash87# dependencies into .pydeps from the archived wheels (no network), then build drat-trim and the C enumerators88python3 -m pip install --no-index --target .pydeps code/wheels/*.whl89QUICK=1 bash code/reproduce.sh # ~10 min: re-verify shipped certificates, robustness checks90bash code/reproduce.sh # ~25 min on 16 cores: oracle n ≤ 22, boundary table p = 16..20, window n ≤ 40 with fresh proofs91FULL=1 bash code/reproduce.sh # several hours: everything, incl. the complete window 26..15492cd paper && make # latexmk → main.pdf (pdflatex + bibtex, aer.bst)93```9495Reproduction runs in a working copy under `results/reproduction/work/`; the shipped artifacts are never modified and96the comparison is written to `results/reproduction/summary.json`. Original run: Python 3.14.7, PySAT 1.9.dev1797(CaDiCaL 1.9.5, Glucose 4.1), drat-trim built from source, gcc -O2, one Apple Silicon node (16 cores).9899## 🗃 Data100101No external data set. Every graph P(n,5) is generated from the definition by `code/graph_constructor.py` (two102independent constructors, canonical edge lists with SHA-256 digests). Inputs consumed by the run: the open-access103full texts of the cited papers and the archived Python wheels (`data/manifest.json`).104105## 🔬 Methodology1061071. 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/`.1082. Upper bound: 12 consecutive outer vertices force P(n,5) for n ≥ 12 (`verify_upper_bounds.py` replays every witness).1093. Lower bound: first-force boundary lemma + column deletion for k = 5 → finite window; SAT encodings with correctness lemmas (`sat_or_ilp_solver.py`).1104. Certificates: CaDiCaL + DRAT, drat-trim, independent rebuild of every CNF (`run_boundary_window.py`, `verify_lower_bounds.py`).1115. Exhaustive oracles: `brute_force.c` (D_n orbit reduction) and `robustness/ff_brute` (first-force normalization).1126. Pre-registration, holdout and falsification campaign (`plan/`, `results/robustness.md`, `check_exceptional_automorphisms.py`).113114## 🖼 Figures & tables inventory115116| Figure | Content |117|---|---|118| `fig1_anatomy_P13_5`, `fig1_anatomy_P15_5` | anatomy of P(n,5), one 13-cycle vs five triangles |119| `fig2a_chronology_P14_5_P7`, `fig2b_chronology_P15_5_optimal` | replayed forcing chronologies |120| `fig3_exact_values` | certified values vs published bounds, 11 ≤ n ≤ 48 |121| `fig4_obstruction_P25_5` | the 18-set with boundary 10 that defeats the method at n = 25 |122| `fig5a_window_scaling`, `fig5b_enumeration_scaling` | cost of the two certified lower-bound engines |123| `fig6_boundary_heatmap` | β_p(n) for 12 ≤ p ≤ 24, 13 ≤ n ≤ 30 |124125Tables (`paper/tables/`): `tab_paths` (lower-bound paths per n), `tab_brute_force`, `tab_exact_values`, `tab_conjectures`,126`tab_verification`, `tab_scope` (A1), `tab_witnesses` (A2), `tab_boundary_table` (A3), `tab_fortcover` (A4), `tab_window_scaling` (A5).127128## ⚠️ Limitations129130- For n > 40 the lower bound rests on one certified path; for n > 154 only on the proved (not formalized) deletion lemma.131- No Lean 4 formalization; "verified" means drat-trim + independent re-implementation, never proof-assistant verified.132- 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.133- Z(P(24r,5)) = 12 is cited second-hand (primary text not accessible to the pipeline).134- The two C enumerators are cross-validated but not formally proved correct; heuristic attacks are evidence only in the heuristic sense.135136## 📝 Citation137138```bibtex139@techreport{boucher2026zeroforcing,140 author = {Boucher, Simon-Pierre},141 title = {Sharp Zero-Forcing Bounds for Generalized Petersen Graphs: Computational Discovery and Certified Proofs for $P(n,5)$},142 institution = {Universit\'e du Qu\'ebec en Outaouais, D\'epartement des sciences administratives},143 type = {Working Paper},144 number = {32},145 year = {2026},146 month = {October},147 note = {First released as AutoScholar Working Paper AS-WP-2026-0001}148}149```150151## 👤 Author & contact152153**Simon-Pierre Boucher** — Département des sciences administratives,154Université du Québec en Outaouais (UQO), Gatineau, QC.155📧 [simon-pierre.boucher@uqo.ca](mailto:simon-pierre.boucher@uqo.ca)156157## 🗒 Notes158159- **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.160- **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).161- Appendix tables are numbered A1–A5 (the AutoScholar edition continued the main numbering 7–11).162