# 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)

| dimension | score | basis |
|---|---|---|
| novelty_relevance | 4 | new sharp theorem for k = 5, method borrowed and credited |
| scientific_validity | 5 | all proofs checked by hand; decisive computations independently reproduced |
| evidence_traceability | 4 | all reported numbers trace to artifacts; one artifact/manuscript inconsistency (M1), manifest missing |
| reproducibility_robustness | 4 | pinned environment, one-command script, certificates re-verified by the referee; large proofs not shipped, script scope gaps |
| manuscript_craftsmanship | 4 | clear and well organized; bib capitalization, one factual slip on automorphism groups, small figure labels |
| integrity_disclosure | 5 | careful novelty qualification, honest certification vocabulary, no overclaiming |

## 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.