# Referee report, round 1

Manuscript: Sharp Zero-Forcing Bounds for Generalized Petersen Graphs: Computational Discovery and Certified Proofs for P(n,5) (AS-WP-2026-0001, v1, 25 pages) Reviewer: independent referee context (claude-fable-5-1), 2026-10-30. The reviewer did not author the manuscript or any artifact outside review/. Recommendation: minor revision.

# 1. Summary of the submission

The paper determines Z(P(n,5)) for every n ≥ 11: the values 6, 8, 9, 8, 8, 8, 10, 10, 10, 10, 10, 11 for n = 11..22 and Z = 12 for all n ≥ 23, with the stabilization threshold n₀ = 23 sharp. The upper bound is the published 2k+2 construction (re-proved column by column). The lower bound for n ≥ 26 adapts the Krishnan–Ma–Zhang first-force boundary method to k = 5: the minimum boundary β₁₈(n) of an 18-set is shown to be ≥ 12 on the finite window 26 ≤ n ≤ 154 by 129 CaDiCaL/DRAT refutations checked by drat-trim, and a column-deletion lemma propagates this to all n ≥ 26. The method provably fails at n = 25 (two inner pentagons give an 18-set with boundary 10), so n = 23, 24, 25 and all n ≤ 22 are settled by exhaustive enumeration (two independently written C programs; n = 24 also has a boundary certificate; n ≤ 22 also have DRAT-certified fort-cover refutations). The paper also proves that the k = 4 parameter p = 16 can never work for k = 5, reports zero slack of the boundary bound, a pre-registered holdout and a falsification campaign.

# 2. What the referee verified independently

I re-derived every lemma by hand and re-ran or re-implemented the decisive computations. Details and outputs are in review/referee-checks/.

Mathematics (hand-checked, all correct as written).

• Proposition 3.4 (order independence), 3.5 (fort characterization), 3.6 (orbit reduction with any subgroup), 3.7 (graph facts), 3.8 (isomorphism P(n,k) ≅ P(n,l), kl ≡ 1): proofs are complete. The list {11, 14, 16, 19, 21} of n with a partner l′ ≤ 4 is correct (n | 5l′ ∓ 1).
• Proposition 4.1 (12 consecutive outer vertices force P(n,5), n ≥ 12): I checked every neighbourhood claim; the only index facts used are j − 5 ≥ 7 and j − 10 ≥ 2, both valid for j ≥ 12.
• Lemma 5.1 (first-force boundary) and Lemma 5.2 (column deletion with 11 empty columns, delete column 5): both inclusions f(N[X]) ⊆ N[X′] and ⊇ hold; the deleted column cannot meet N[X] because i + d ≤ n + 4 < n + 5. The hypothesis of eleven empty columns matches Lemma 2.2 of Krishnan–Ma–Zhang for k = 5 (2k+1 columns).
• Lemmas 5.3–5.5: the counting (singly occupied columns = 2c − p exactly; n − c > 10c forces a gap of ≥ 11 empty columns; c_max = 14 and N_max = 154 for p = 18; Lemma 5.3 applies for n ≥ 15) is correct.
• Lemma 5.6 (boundary CNF ⇔ β_p(n) ≤ 11) and Lemma 5.7 (fort-cover CNF, four D_n-orbits of directed edges: outer both directions, outward spokes, inward spokes, inner both directions): correct; the direction used by the certificates (UNSAT ⇒ β ≥ 12, resp. Z ≥ b+1) needs only rotation invariance and completeness of the sequential counter.
• Assembly of Theorem 1.1: correct. No step extrapolates from the table.

Certificates and encodings.

• drat-trim re-run by me on P26_5_p18_b11 (CNF 1,779 vars / 3,589 clauses): s VERIFIED, exit 0, 15.4 s. SHA-256 prefixes of the n = 26 and n = 154 CNF/DRAT pairs match Table 10.
• The CNF in the stored n = 26 file begins with exactly the edge clauses of Lemma 5.6; the project's independent checker rebuilds the formula (reusing only PySAT's CardEnc for the counter) and compares sorted clause multisets. I additionally tested the semantics of the encoder against my own brute force on P(13,5) for p = 3..7: F(13,p,β−1) is UNSAT and F(13,p,β) is SAT in every case. This is independent of the authors' 94-instance check and confirms that the encoding is neither over- nor under-constrained on small instances.
• All 37,521 stored forts of the n = 22 certificate and all 87,239 forts of the n = 23 file were re-validated as forts by my own code.
• Window statistics recomputed from results/tables/boundary_window_p18.csv: 129 rows covering n = 26..154 without gap; solve total 12,972.1 s (min 17.4, max 266.8, mean 100.6), drat-trim total 11,700.7 s (min 13.3, max 231.3, mean 90.7), 346,502,796 proof lines (min 1,214,641, max 4,923,281). All numbers in Computational Result 7.5 and the abstract agree with the artifacts; results/metrics.json carries the 130-certificate totals (including n = 24), which is consistent.

The uncertified cases n = 23 and n = 25. These two values are the load-bearing ones for the threshold (n₀ = 23) and for the n = 25 exception, and in the manuscript they rest only on exhaustive enumeration. I wrote my own first-force enumerator from the mathematical statement (not from the authors' code), validated it on ten controls (no forcing set at Z−1, forcing sets at Z, for n = 11, 13, 14, 15, 22; enumerated counts identical to the paper's E′ column), and ran it on all 472,120,740 normalised 11-sets of P(23,5) and all 1,043,731,260 of P(25,5): no zero-forcing 11-set exists in either graph. With the authors' two programs this makes three independent exhaustive confirmations of Z(P(23,5)) = Z(P(25,5)) = 12.

Other. The n = 25 obstruction sets recount to boundary 10 (both the p = 18 and the p = 20 set). Pre-registration timing checks out: conjectures registered 18:00:31 UTC, the earliest n > 30 boundary certificate is 18:01:10, holdout records 18:10–19:02. The second enumerator's logs for n = 31..40 exist and show 0 forcing 11-sets. All 20 cited keys exist in sources/sources.json with verified: true; all \cite keys in main.tex resolve; reading depth is stated honestly. My own searches of OpenAlex and arXiv for zero forcing on generalized Petersen graphs returned nothing on k = 5 beyond the sources already cited (Semantic Scholar returned HTTP 429 and could not be queried).

# 3. Assessment

Novelty. The result is a genuine new theorem: the complete determination of Z(P(n,5)) with a sharp threshold, closing the k = 5 case the 2026 papers leave open. The method is borrowed, and the paper says so plainly and repeatedly; the k = 5-specific content (p = 18 is needed, p = 16 provably never works, the n = 25 pentagon obstruction, the window) is a real contribution of moderate size. The "what is new and what is not" paragraph is exemplary.

Validity. I found no mathematical error in any proof. The solver encodings are proved correct, the certificates are externally checked, and the one place where the chain is purely computational (n = 23, 25) I confirmed independently.

Integrity and disclosure. Very good: three-valued certification status never collapsed, second-hand attribution of the 24r family flagged everywhere it matters, no Lean claim, heuristic evidence labelled as such, limitations are specific.

# 4. Major issues

M1. Inconsistency between the manuscript and the certificate archive for n = 23 and n = 25; these two values lack an externally checkable certificate. Observation 7.7 and Table 1 state that the fort-cover engine "returned UNSAT without a proof log" at n = 23 (837 s) and n = 25 (1,796 s), and these cases are marked "(s)". But code/proofs/certificates/fortcover/ contains P23_5_atmost11.cnf, P23_5_atmost11.forts.json (87,239 forts, all valid) and a 4.0 GB P23_5_atmost11.drat, plus P25_5_atmost11.cnf and .forts.json (149,950 forts) without a proof. None of these appear in results/lower_bound_certificates.jsonl or in lower_bound_verification.json. Either a proof-logging re-solve for n = 23 was completed and never checked/recorded, or the file is a partial/aborted log; in both cases the manuscript's description of the artifact state is inaccurate. Because n = 23 and n = 25 are exactly the cases the boundary method cannot reach, and the brief asks for independently checkable lower-bound evidence wherever possible, the authors should (a) run drat-trim on the existing n = 23 proof and, if it verifies, record it and upgrade the entry; (b) produce and verify a proof-logging re-solve for n = 25 (the CNF and fort list already exist; the plain solve took 30 min, so this is feasible), or, if infeasible, state explicitly in Observation 7.7, Table 1 and the Limitations that these two values have no external certificate and rest on exhaustive enumeration only; and (c) remove or document unrecorded files in the certificate directory. This is not a validity concern: I confirmed both values with my own program (Section 2). (The referee started drat-trim on the n = 23 file; the outcome is recorded in review/referee-checks/drat_P23_fortcover.txt if it finished.)

# 5. Minor issues

m1. Exceptional automorphism groups misstated (Section 2 and Section 6). The paper says that for k = 5 and n ≥ 11 the only n with Aut(P(n,5)) larger than D_n are n = 12 and n = 24 (5² ≡ 1). By Frucht–Graver–Watkins the group is also larger when k² ≡ −1 (mod n), i.e. n = 13 and n = 26 (25 ≡ −1 mod 13 and mod 26; |Aut| = 4n). The orbit reduction remains sound (Proposition 3.6 works for any subgroup), but the statement should read n ∈ {12, 13, 24, 26}.

m2. Second-hand attribution dropped in one place. The "Maximum nullity" paragraph (Section 9) states "Alameda et al. (2018) show equality for 24 | n" without the second-hand qualifier used elsewhere; add "(as reported in Rashidi et al. 2020)" or cite Table 3's dagger.

m3. "Known for k = 2" in the abstract. The value Z(P(n,2)) = 6 for n ≥ 10 comes from the same figure-based style of argument in Rashidi et al. that failed for k = 3. If the authors treat it as known they should say where it is independently confirmed, or soften to "reported".

m4. data/manifest.json is absent. The platform contract requires a manifest with provenance, licence, timestamp and SHA-256 of data; the run has no external data, but the downloaded full texts in sources/fulltext/ (with SHA-256s given in plan/prior-art.md) and the archived wheels are inputs that belong there, and an explicit "no observational data" manifest avoids a failed deterministic check.

m5. Reproduction script scope. reproduce.sh re-runs the exhaustive oracle only for n ≤ 25 and does not regenerate the fort-cover runs for n = 23, 25 nor the n = 26, 27 enumerations; the QUICK path re-verifies "every certificate present" but the paper states the 39 GB of DRAT proofs are not shipped, so a reader of the archive gets no certificate verification in QUICK mode unless the window is regenerated (~30 min on 12 cores). State this explicitly in Appendix C, and mention the FULL=1 dependency of Table 2's E′ column for n = 31..40.

m6. Bibliography capitalization. The .bst lowercases protected words: "p(n,3)", "Pysat", "Drat-trim", "lean 4", "cnf", "petersen" in several titles. Protect with braces in references.bib.

m7. Holdout wording. Section 8 describes the holdout as an out-of-sample test, but by the time it was computed the prediction Z = 12 was already guaranteed by Lemma 5.5 for any n ≥ 26 once the window was certified; the holdout therefore tests the pipeline rather than the conjecture. The existing sentence "an honest out-of-sample test before the proof was complete" is fair; a half-sentence acknowledging this limited epistemic role would be more accurate.

m8. Table 2 caption / Observation 7.7. The brute-force table reports 371 s for the n = 25 size-11 pass, while Observation 7.7 reports the fort-cover engine's 1,796 s UNSAT at n = 25 as "without a proof log"; see M1. Also Figure 2's vertex labels are very small at print size.

# 6. Proposed tests for the revision

1. code/tools/drat-trim/drat-trim code/proofs/certificates/fortcover/P23_5_atmost11.cnf code/proofs/certificates/fortcover/P23_5_atmost11.drat → expect s VERIFIED, exit 0; then add the record to results/lower_bound_certificates.jsonl and re-run verify_lower_bounds.py.
2. Proof-logging re-solve of P25_5_atmost11.cnf (static CNF, 10 MB) with CaDiCaL and drat-trim; if it exceeds budget, document the attempt and keep "(s)".
3. python3 -c check that for n in {12, 13, 24, 26} the map ψ of Proposition 3.8 (with l = ±5) is an automorphism of P(n,5), to confirm m1 before editing the text.
4. Re-run build_tables.py after 1–2 so Table 1, Table 3 and exact_values.csv reflect the new status.

# 7. Scores (0–5)

# 8. Limitations of this review

I could not access the full text of Alameda et al. (2018) either, so the claim that the 24r family is the only prior exact result for k = 5 rests on the same secondary report as the paper's. Semantic Scholar was unavailable (HTTP 429). I re-ran drat-trim on one boundary certificate and sampled hashes rather than re-verifying all 129 proofs (the authors' independent checker log covers all; the full re-check costs ~3.3 CPU-hours). My own enumerator shares the first-force normalisation principle with the authors' second program (though not its code); the D_n-orbit program is a genuinely different principle and the three agree. The drat-trim run on the unrecorded n = 23 fort-cover proof may not have finished when this report was written.