# 🔗 Zero-Forcing Bounds for Generalized Petersen Graphs **UQO Working Paper No. 32** — *Computational Discovery and Certified Proofs for P(n,5)* [-b31b1b?logo=latex&logoColor=white)](paper/main.pdf) [](requirements.txt) [](code/proofs/certificates/) [](code/reproduce.sh) [](https://www.autoscholar.ai) [](https://uqo.ca) [](mailto:simon-pierre.boucher@uqo.ca) > **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 | Item | Value | |---|---| | Version | 1.0 (October 2026) | | 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`) | | SSRN | not yet submitted | | Journal | — (candidates: *Linear Algebra and its Applications*, *Discrete Applied Mathematics*, *Electronic Journal of Combinatorics*) | | 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) | ## 🎯 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 | Object | Result | |---|---| | 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}) | | Z(P(n,5)), n ≥ 23 | 12 (new: the threshold statement, n₀ = 23 sharp since Z(P(22,5)) = 11) | | Boundary parameter | p = 18 is the smallest that works; p = 16 fails for every n ≥ 22 (Prop. 7.3) | | Obstruction | every p ≤ 24 fails at n = 25 (two inner pentagons, boundary 10) | | Certified window | 129 DRAT certificates, 26 ≤ n ≤ 154 (+ n = 24); solve 17–267 s each, 39 GB of proofs in the original run | | Zero slack | β₁₈(n) = 12 exactly for 26 ≤ n ≤ 40 | | Exhaustive oracle | 432 billion subsets enumerated (4 126 s, 16 threads); second enumerator 344 billion sets | | Holdout | H = {32, 35, 37, 41, 44, 48} frozen before fitting; all six values = 12 as registered | ## 🗂 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 ```bash # 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 | Figure | Content | |---|---| | `fig1_anatomy_P13_5`, `fig1_anatomy_P15_5` | anatomy of P(n,5), one 13-cycle vs five triangles | | `fig2a_chronology_P14_5_P7`, `fig2b_chronology_P15_5_optimal` | replayed forcing chronologies | | `fig3_exact_values` | certified values vs published bounds, 11 ≤ n ≤ 48 | | `fig4_obstruction_P25_5` | the 18-set with boundary 10 that defeats the method at n = 25 | | `fig5a_window_scaling`, `fig5b_enumeration_scaling` | cost of the two certified lower-bound engines | | `fig6_boundary_heatmap` | β_p(n) for 12 ≤ p ≤ 24, 13 ≤ n ≤ 30 | 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 ```bibtex @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](mailto: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).