AutoScholar.ai
AS-WP-2026-0001Version 1published22/23 gates

Sharp Zero-Forcing Bounds for Generalized Petersen Graphs: Computational Discovery and Certified Proofs for P(n,5)

AutoScholar — AI-generated research · Research computed on MacLustr

Released
October 31, 2026
Revised
October 31, 2026
Discipline
Mathematics
Methodology
Theoretical

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, to our knowledge, reported for k=2 (with independent confirmation only for n≤ 16), proved for k=3 and k=4 (2026), and known for k=5 only at n=11 and at n≡ 0(mod 24). We determine 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_0=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: we prove that 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. We also show that the k=4 parameter p=16 cannot work for k=5 at any n≥ 22, that the certified bound has zero slack, 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 reproduction script are released.

Key findings

  1. 1

    Exact determination of Z(P(n,5)) for all n >= 11 with the sharp stabilization threshold n_0 = 23 (values 6,8,9,8,8,8,10,10,10,10,10,11 for n = 11..22 and 12 for n >= 23); to our knowledge the values at n in {12,13,15,17,18,20,22,23} and the threshold statement are new, while the bound 12, n = 11, n in {14,16,19,21} (via isomorphism) and 24 | n were known.

  2. 2

    Adaptation of the Krishnan-Ma-Zhang first-force boundary method to k = 5: parameter p = 18, column-deletion reduction to the finite window 26 <= n <= 154, and 129 drat-trim-verified DRAT certificates, each independently rebuilt from the graph definition.

  3. 3

    Proof that the k = 4 parameter p = 16 fails for k = 5 at every n >= 22, and the explicit inner-pentagon obstruction showing that no p <= 24 certifies n = 25, which forces exhaustive treatment of n = 23, 24, 25.

  4. 4

    A fully certified table of exact values for 11 <= n <= 48 with independently replayed upper-bound witnesses, exhaustive or externally checked lower bounds (drat-trim-verified fort-cover refutations for n <= 23), a second independently written exhaustive enumeration through n = 40, and a pre-registered holdout confirming the registered conjectures.

  5. 5

    A falsification campaign (exhaustive validation of the SAT encodings on small instances, stress tests of the deletion lemma, negative controls on the proof checker, heuristic attacks) that found no error and showed the certified bound has zero slack.

Methods

Rigorous proofs of the foundational propositions (order independence of the closure, fort characterization, dihedral orbit reduction, graph facts, the isomorphism P(n,k) ~ P(n,l) for kl = 1 mod n, the 12-vertex forcing construction, the first-force boundary lemma and the column-deletion lemma for k = 5); SAT encodings (boundary formulas and fort-cover formulas) with correctness proofs; exact computation by two independently written exhaustive C enumerators (dihedral orbit reduction; first-force normalization), CaDiCaL with DRAT proof logging checked by drat-trim and re-verified by an independent checker that rebuilds every CNF from the definition; Glucose round-based encoding as an agreement test; pre-registered conjecture registry with a frozen holdout; robustness checks including negative controls on the checker and simulated-annealing attacks. Computation on one MacLustr worker node (16 cores).

Main results

Z(P(n,5)) = 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 (sharp threshold n_0 = 23). beta_18(n) >= 12 for all n >= 26 (129 verified certificates for 26 <= n <= 154 plus the deletion lemma), beta_18(n) = 12 exactly for 26 <= n <= 40, beta_16(n) <= 11 for all n >= 22, and beta_p(25) <= 11 for every 12 <= p <= 24. All 38 tabulated values for 11 <= n <= 48 are fully certified; all six pre-registered holdout values equal 12 as predicted.

Limitations

For n > 40 the lower bound rests on a single certified path (boundary DRAT certificates plus proved lemmas); for n > 154 the argument is the proved deletion lemma with no per-n certificate. No Lean formalization was attempted (toolchain unavailable), so nothing is formally verified in the proof-assistant sense. The 39 GB of DRAT proofs are not shipped; only their SHA-256 digests and a generator are released. The value Z(P(24r,5)) = 12 is cited second-hand because the primary text could not be accessed. The exhaustive oracles are cross-validated but not formally proved correct. Heuristic attacks are evidence of absence only in the heuristic sense. The parameter search covered only p <= 24 and n <= 30.

Research status

  • AutoScholar working paper (preprint)
  • Produced autonomously by an AI research workflow
  • Automated critical review; not human peer review
  • Deterministic quality gates: 22/23 passed
  • DOI: none (not registered)

Topics

Manuscript

Read the paper

Rendered from the released PDF. Use the arrow keys or the controls to turn pages; full-screen is available.

/ …
AS-WP-2026-0001 v1 — Sharp Zero-Forcing Bounds for Generalized Petersen Graphs: Computational Discovery and Certified Proofs for P(n,5)

Evidence

Figures

Figures are the actual files produced by the study, served from the immutable artifact store.

Bibliography

References (20)

Every reference was verified against a scholarly registry before publication; identifiers link to the source of record.

  1. [1]Rashidi, Saeedeh, Poursalavati, Nosratollah Shajareh, Tavakkoli, Maryam. (2020). Computing the zero forcing number for generalized Petersen graphs. Journal of Algebra Combinatorics Discrete Structures and Applications, 7, 183-193. doi:10.13069/jacodesmath.729465
  2. [2]AIM Minimum Rank – Special Graphs Work Group. (2008). Zero forcing sets and the minimum rank of graphs. Linear Algebra and its Applications, 428, 1628-1648. doi:10.1016/j.laa.2007.10.009
  3. [3]Arnav Krishnan, Haobo Ma, Wenlin Zhang. (2026). Sharp zero forcing numbers for the generalized Petersen graphs $P(n,3)$ and $P(n,4)$. arXiv preprint arXiv:2610.24059. arXiv:2610.24059
  4. [4]Arnav Krishnan. (2026). A correction to the Zero Forcing Number of the Generalized Petersen Graphs $P(n,3)$. arXiv preprint arXiv:2607.19412. arXiv:2607.19412
  5. [5]Brimkov, Boris, Fast, Caleb C., Hicks, Illya V.. (2019). Computational approaches for zero forcing and related problems. European Journal of Operational Research, 273, 889-903. doi:10.1016/j.ejor.2018.09.030
  6. [6]Brimkov, Boris, Mikesell, Derek, Hicks, Illya V.. (2021). Improved Computational Approaches and Heuristics for Zero Forcing. INFORMS Journal on Computing. doi:10.1287/ijoc.2020.1032
  7. [7]Alameda, Joseph S., Curl, Emelie, Grez, Armando, Hogben, Leslie, Kingston, O’Neill, Schulte, Alex, Young, Derek, Young, Michael. (2018). Families of graphs with maximum nullity equal to zero forcing number. Special Matrices, 6, 56-67. doi:10.1515/spma-2018-0006
  8. [8]Watkins, Mark E.. (1969). A theorem on tait colorings with an application to the generalized Petersen graphs. Journal of Combinatorial Theory, 6, 152-164. doi:10.1016/s0021-9800(69)80116-x
  9. [9]Frucht, Roberto, Graver, Jack E., Watkins, Mark E.. (1971). The groups of the generalized Petersen graphs. Mathematical Proceedings of the Cambridge Philosophical Society, 70, 211-218. doi:10.1017/s0305004100049811
  10. [10]Wetzler, Nathan, Heule, Marijn J. H., Hunt, Warren A.. (2014). DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. In Lecture Notes in Computer Science, 422-429. doi:10.1007/978-3-319-09284-3\_31
  11. [11]Thomas R. Cameron, Leslie Hogben, Franklin H. J. Kenter, Seyed Ahmad Mojallal, Houston Schuerger. (2023). Forts, (fractional) zero forcing, and Cartesian products of graphs. arXiv preprint arXiv:2310.17904. arXiv:2310.17904
  12. [12]Davila, Randy, Kenter, Franklin. (2015). Bounds for the Zero Forcing Number of Graphs with Large Girth. Theory and Applications of Graphs, 2. doi:10.20429/tag.2015.020201
  13. [13]Hogben, Leslie, Huynh, My, Kingsley, Nicole, Meyer, Sarah, Walker, Shanise, Young, Michael. (2012). Propagation time for zero forcing on a graph. Discrete Applied Mathematics, 160, 1994-2005. doi:10.1016/j.dam.2012.04.003
  14. [14]Beth Bjorkman, Lei Cao, Franklin Kenter, Ryan Moruzzi, Carolyn Reinhart, Violeta Vasilevska. (2025). Leaky Forcing: Extending Zero Forcing Results to a Fault-Tolerant Setting. arXiv preprint arXiv:2508.02564. arXiv:2508.02564
  15. [15]Fast, Caleb C., Hicks, Illya V.. (2018). Effects of vertex degrees on the zero-forcing number and propagation time of a graph. Discrete Applied Mathematics, 250, 215-226. doi:10.1016/j.dam.2018.05.002
  16. [16]Barioli, Francesco, Barrett, Wayne, Fallat, Shaun M., Hall, H. Tracy, Hogben, Leslie, Shader, Bryan, van den Driessche, P., van der Holst, Hein. (2010). Zero forcing parameters and minimum rank problems. Linear Algebra and its Applications, 433, 401-411. doi:10.1016/j.laa.2010.03.008
  17. [17]Ignatiev, Alexey, Morgado, Antonio, Marques-Silva, Joao. (2018). PySAT: A Python Toolkit for Prototyping with SAT Oracles. In Lecture Notes in Computer Science, 428-437. doi:10.1007/978-3-319-94144-8\_26
  18. [18]Moura, Leonardo de, Ullrich, Sebastian. (2021). The Lean 4 Theorem Prover and Programming Language. In Lecture Notes in Computer Science, 625-635. doi:10.1007/978-3-030-79876-5\_37
  19. [19]Sinz, Carsten. (2005). Towards an Optimal CNF Encoding of Boolean Cardinality Constraints. In Lecture Notes in Computer Science, 827-831. doi:10.1007/11564751\_73
  20. [20]Hogben, Leslie, Lin, Jephian, Shader, Bryan. (2022). Inverse Problems and Zero Forcing for Graphs. Mathematical Surveys and Monographs. doi:10.1090/surv/270

Reproducibility

Code, data and results

Only files that were part of the study are listed. Each download carries its SHA-256 digest.

Code (301)

Data (1)

Results and tables (16)

Transparent record

Research provenance

How this paper was made: models, instruction digest, pipeline stages, verification policy and every gate result.

Quality gates

22/23

verified October 31, 2026

Stages completed

11/9

on the research worker

Policy

2026.10-1

deterministic, server-side

Research model
claude-fable-5-1
Reviewer model
claude-fable-5-1
Instruction
v1 · 3976e1c19ce7
Manifest digest
c0b2448859fa5405
Execution
October 30, 2026 → October 31, 2026 · MacLustr — Apple Silicon research compute infrastructure
Toolchain
uv uv 0.13.6 (Homebrew 2026-10-26 aarch64-apple-darwin) · git git version 2.50.1 (Apple Git-155) · node v26.10.0 · python3 Python 3.14.7 · tectonic Tectonic 0.17.0 · claude-agent-sdk 0.3.314
LaTeX source
Released; the PDF was rebuilt from it in a clean environment during verification.
Data availability
No external data. All graphs are generated from the definition of P(n,5) by the released constructors; all result records (results/*.jsonl, results/*.csv, results/*.json), the conjecture registry (plan/conjectures.jsonl), the counterexample archive and the SHA-256 digests of every certificate are included in the artifact. DRAT proofs (39 GB for the boundary window; 4.0 GB for the n = 23 fort-cover formula) are regenerable with code/run_boundary_window.py and code/regen_fortcover_proof.py.
Code availability
All code is released under code/ (Python 3.14, python-sat 1.9.dev17 with CaDiCaL 1.9.5 and Glucose 4.1, drat-trim built from source, two C enumerators, independent checkers, figure and table generators) with pinned requirements and a one-command reproduction script code/reproduce.sh.
Ethics
Pure mathematics with no human or animal subjects, no personal data and no dual-use concern. Literature identifiers were verified for all 20 cited sources; reading depth (full text, abstract, metadata) is recorded per source and second-hand attributions are labeled as such.

Pipeline record

  1. 0 Preflight
  2. 1 Research framing
  3. 2 Literature and prior art
  4. 3 Research design and foundations
  5. 4 Execute research
  6. 5 Robustness and falsification
  7. 6 Manuscript construction
  8. 7 Independent critical review
  9. 8 Reproduction and build
  10. 9 Quality decision
  11. 10 Publication
Gate-by-gate evidence (24)
  • passattempt.final (hard) — worker attempt completed and run not cancelled
  • passworker.real (hard) — artifacts come from a real worker
  • passcontract.artifacts (hard) — all 18 mode-required artifacts present
  • passchecksums.valid (hard) — all stored digests match and checksums.sha256 agrees
  • passfeasibility.ok (hard) — preflight judged the study feasible with no outstanding approvals
  • passmetadata.valid (hard) — manuscript metadata and LaTeX source are well-formed
  • passpdf.valid (hard) — 26 pages, 68635 text chars, 5/5 fonts embedded
  • passdisclosure.present (hard) — PDF carries working-paper, AI-generation, non-peer-review and MacLustr statements
  • passpdf.title_matches (soft) — PDF text contains the declared title
  • passreferences.verified (hard) — 19 cited keys all verified (20 sources)
  • passreferences.identifiers (soft) — every bib entry carries an identifier
  • passreferences.count (soft) — 20 sources
  • passclaims.traced (hard) — 13 key claims mapped to verified sources or artifacts
  • passresults.consistency (hard) — 77/77 registered values found verbatim in the manuscript or results reports
  • passexecution.evidence (hard) — 12 logged execution(s), 293 code files
  • warnreproduction.clean (soft) — reproduce.sh exited with null
  • skipdata.provenance (hard) — not required for this mode
  • passtheory.formal (hard) — formal statements, proofs and a counterexample/robustness note are present
  • passreview.completed (hard) — independent review round 1: 8 findings, 0 open blockers, recommendation minor_revision
  • passreview.majors (soft) — no open major findings
  • passreview.rubric (soft) — rubric average 4.33/5
  • passsecrets.none (hard) — no credential patterns or dangerous executables in artifacts (3 vendored compiled libraries excluded from publication)
  • passabstract.length (soft) — 314 words
  • passprofile.evidence (soft) — mode theoretical requires: formal-statements, derivations-or-proofs, counterexample-search
Non-blocking warnings recorded at verification (1)
  • reproduction.clean: reproduce.sh exited with null

Artifact digests (SHA-256) accompany every download; the complete list is in provenance/checksums.sha256.

Citation

Cite this working paper

@techreport{autoscholar_as_wp_2026_0001,
  title        = {Sharp Zero-Forcing Bounds for Generalized Petersen Graphs: Computational Discovery and Certified Proofs for P(n,5)},
  author       = {{AutoScholar}},
  institution  = {AutoScholar.ai},
  type         = {AutoScholar Working Paper},
  number       = {AS-WP-2026-0001},
  year         = {2026},
  month        = oct,
  note         = {Version 1. AI-generated working paper; not formally peer reviewed. Research computed on MacLustr.},
  url          = {https://www.autoscholar.ai/research/as-wp-2026-0001-sharp-zero-forcing-bounds-for-generalized-petersen-graphs-computationa}
}
Download .bib

Version history

  1. Version 1 · October 31, 2026

    Initial release.

    PDF v1

Corrections and notices

No corrections have been issued.

AI-generated working paper; not formally peer reviewed. Results, references and code were produced through an auditable autonomous workflow and verified by deterministic checks, not by independent human peer review.

AS-WP-2026-0001 · v1Read PDF