1# Response to referee report, round 123Manuscript AS-WP-2026-0001, version 1 (revised 2026-10-30). The referee's report is `review/review-1.md` / `review/review-1.json`. Every finding is addressed below; resolutions are recorded in `review/review-1.json`. No theorem statement changed. All new numbers reported in the manuscript are registered and trace to artifacts in `results/revision/`, `results/lower_bound_certificates.jsonl` and `results/lower_bound_verification.json`.45## Major67### F1 — unrecorded n = 23 fort-cover DRAT proof; no external certificate for n = 23, 2589**Referee is right.** The file `P23_5_atmost11.drat` was produced by a proof-logging re-solve of the stored n = 23 formula (`code/regen_fortcover_proof.py 23 11`, run 19:41–20:03 UTC) whose process ended before drat-trim finished and before the record was appended; the n = 25 formula had never been re-solved under proof logging. The manuscript's statement "UNSAT without a proof log" described the solver runs of 19:41 and 19:57 UTC correctly but the artifact state incorrectly.1011**What we did.**1213* **n = 23.** `code/proofs/certificates/fortcover/P23_5_atmost11.drat` (59,527,561 lines, 4.0 GB, SHA-256 `7c10868af9341f0592a44dfa802e2b71426bab05424555ecbed286acbc58a020`) was checked by `drat-trim` through a plain subprocess (`code/check_fortcover_proof.py 23 11`, log `results/revision/check_fortcover_n23.log`): `s VERIFIED`, exit code 0, 2,486 s. The record (CNF, fort list and proof digests; 87,239 forts; 435 variables, 88,050 clauses) was appended to `results/lower_bound_certificates.jsonl` and `results/solver_runs.jsonl`. The referee's own earlier run of drat-trim on the same file (`review/referee-checks/drat_P23_fortcover.txt`) also ended with `s VERIFIED`. No solve time is claimed for the re-solve because its process did not write one (Table 9 marks it n/r). The independent checker (`code/verify_lower_bounds.py`: fort re-validation, CNF rebuilt from the definition, digests, drat-trim re-run) was started on this record in the revision stage; if its merged report is present in `results/lower_bound_verification.json` (fort-cover row n = 23, ok = true) it completed, otherwise it did not finish within the stage's time limit and the n = 23 certificate is described in the manuscript as drat-trim-verified only.14* **n = 25.** `P25_5_atmost11.cnf` / `.forts.json` were left by the solver run of 19:57 UTC (no proof log). A proof-logging re-solve (`code/regen_fortcover_proof.py 25 11`, 2026-10-30 ~23:10–23:48 UTC) wrote `P25_5_atmost11.drat` (103,621,714 lines, 7.7 GB, SHA-256 `2d4f66869a527ebdbd08e8b47960fbc4a6e3149f2ad1d1f4860df8eba4888a69`), but its drat-trim check was killed by the stage time limit after 3,335 s (`results/revision/check_fortcover_n25.log`, exit −15) and a second attempt started in this revision pass could not be completed within the stage either. The proof's status is therefore **unknown**; it is recorded (digest, line count, origin) in `results/solver_runs.jsonl` but **not** in `results/lower_bound_certificates.jsonl`, it is not counted anywhere, and `FULL=1 sh code/reproduce.sh` re-checks it (`code/check_fortcover_proof.py 25 11`). Z(P(25,5)) ≥ 12 continues to rest on the two exhaustive enumerations (and the referee's), as the manuscript now states explicitly (Observation 7.7; Table 1 keeps the "(s)" mark at n = 25).15* **Manuscript.** Observation 7.7 rewritten as above; Table 1 column F now shows a verified certificate at n = 23; Table 9 lists the n = 23 certificate with the n/r footnote; the abstract, Section 9 and metadata say "for n ≤ 23"; Appendix C documents the two large proof files and the FULL-mode check. The lower-bound *status* of n = 23 and n = 25 was already fully certified (exhaustive enumeration); what changed is that an external, independently checkable certificate now exists at n = 23, and that the artifact state at n = 25 is described accurately.1617**Resolution:** resolved (n = 23 externally certified; n = 25 documented as exhaustive-only with the unverified proof file recorded and excluded from every count).1819## Minor2021### F2 — exceptional automorphism groups (n = 13, 26 omitted)2223**Referee is right.** Frucht–Graver–Watkins give |Aut(P(n,k))| > 2n when k² ≡ ±1 (mod n); 25 ≡ −1 modulo 13 and 26. We ran the proposed test (`code/check_exceptional_automorphisms.py`, output `results/revision/aut_check.json`): the layer-swapping map ψ(v_{5j}) = u_j, ψ(u_{5j}) = v_j is an automorphism of P(n,5) exactly for n ∈ {12, 13, 24, 26} among 11 ≤ n ≤ 60, and for no other n with gcd(n,5) = 1. Section 2 now states the k² ≡ ±1 condition and lists n ∈ {12, 13, 24, 26}; Section 6 (exhaustive oracle) lists the same four n and notes that Proposition 3.6 holds for any subgroup, so no result changes. **Resolved.**2425### F3 — second-hand attribution dropped in the maximum-nullity paragraph2627**Referee is right.** The sentence now reads "Alameda et al. (2018) are reported to show equality for 24 | n (as stated in Rashidi et al. 2020, Remark 2.4; we could not read the primary text, see Table 3)". **Resolved.**2829### F4 — "known for k = 2" in the abstract3031**Referee is right.** The only source for Z(P(n,2)) = 6 (n ≥ 10) is Theorem 2.5 of Rashidi et al. (2020), proved by the figure-based case analysis that failed for k = 3; the correction note (arXiv:2607.19412) confirms the k = 2 values by exhaustive search only for 10 ≤ n ≤ 16. The abstract (`main.tex`, `abstract.md`, `metadata.json`) now says the sharp values were "reported for k = 2 (with independent confirmation only for n ≤ 16), proved for k = 3 and k = 4 (2026)", and the related-work paragraph states this explicitly with both citations. **Resolved.**3233### F5 — `data/manifest.json` missing3435**Referee is right.** Created `data/manifest.json`: it states that the study uses no observational or synthetic data, describes how every graph is generated from Definition 3.1 (with the location of the edge-list digests), and lists the eleven external inputs the run consumed — the three literature PDFs and their extracted texts (SHA-256, origin, licence where known, fetch time), the four archived wheels (SHA-256 equal to the PyPI digests, licences from the wheel metadata) and the drat-trim source (SHA-256) — plus the regeneration command and digest location for the unshipped 39 GB of boundary proofs. **Resolved.**3637### F6 — `reproduce.sh` scope and unshipped proofs not fully described3839**Referee is right.** (a) Appendix C now lists, mode by mode, which rows of Tables 1 and 2 each mode regenerates, states that QUICK mode on the bare archive re-verifies only the shipped fort-cover proofs and no boundary certificate (because those proofs must first be regenerated), and gives the cost of each mode. (b) `code/reproduce.sh` gained the same description in its header and a `FULL=1` block that runs the exhaustive oracle at n = 26, 27, the proof-logging re-solves of the stored fort-cover formulas for n = 23 and 25, the independent checker and the table builder, in addition to the second enumerator through n = 40 and the encoding checks. (c) The `FULL=1` dependency of the E′ column for n = 31..40 is stated in Appendix C. (d) A new `manuscript/reproducibility.md` records the environment, commands, seeds, digests and the outcome of the platform's clean re-execution (which completed the certified window with all visible instances verified but was stopped by the time limit before steps 7–10). **Resolved.**4041### F7 — bibliography capitalization; small figure labels4243**Referee is right.** Protected with braces in `references.bib`: {P}etersen, {$P(n,3)$}, {$P(n,4)$}, {T}ait, {C}artesian, {DRAT-trim}, {PySAT}, {P}ython, {SAT}, {Lean 4}, {CNF}, {B}oolean (title case otherwise left to the style). The vertex index labels in Figure 2 (and the other Petersen drawings) were enlarged from `\tiny` to `\scriptsize` with a slightly larger offset in `code/build_figures.py`; all nine figures were rebuilt from the artifacts. **Resolved.**4445### F8 — holdout's epistemic role4647**Referee is right.** Section 9, competing explanation (1), now adds: "by the time the holdout values were computed the window 26 ≤ n ≤ 154 had been certified, so Lemma 5.5 already guaranteed the prediction 12 at every holdout n, and the holdout therefore tested the pipeline (witness replay, certificate generation and checking at new n) rather than the conjecture itself." **Resolved.**4849## Other changes made in this revision5051* `results/metrics.json` now also carries a flat `metrics` record of the scalar headline values (the platform's metrics comparison expected one and reported "not compared"); `code/build_metrics.py` writes it.52* `code/README.md` documents the reproduction modes and the two scripts added in this revision.53* `plan/research-plan.md` log entry for Stage 8.5455## Checks re-run after the changes5657* Independent lower-bound checker, full run over all shipped certificates before the merge (135 boundary, 14 fort-cover rows): every checked certificate accepted (`results/lower_bound_verification.json`, `results/verify_lower_bounds_stdout.txt`).58* `code/reproduce.sh` default mode (working copy under `results/reproduction/work/`, 2026-10-31 01:05–01:34 UTC): steps 0–7 completed in 26 min with every step exiting 0 (`results/reproduction/work/results/experiment-log.jsonl`: T1, T2, lemma checks, witness replay, sample of shipped proofs re-verified, exhaustive oracle n = 11..22 reproduced, boundary table p = 16..20, window n = 26..40 regenerated with fresh verified proofs, fort-cover certificates n = 11..22 regenerated); step 8 (re-check of the regenerated certificates) was interrupted by the stage time limit. Because the platform's own clean run also hit its limit, the default mode was trimmed (fort-cover n ≤ 21, smaller sample of shipped proofs) to about 25 minutes; the removed pieces are in `FULL=1`.59* Witness replay (`code/verify_upper_bounds.py 60`): re-run after the table rebuild, all 35 witnesses and 49 P7 chronologies ok (`results/upper_bound_verification.json`).60* Tables and metrics rebuilt (`build_tables.py`, `build_metrics.py`, `collect_robustness_metrics.py`, `build_manuscript_tables.py`); `results/metrics.json` carries the flat `metrics` record and the `reportedValues` registry (77 values).61* Quality-gate fixes of this pass: seven numbers that the deterministic consistency check could not find were written with plain thousands separators; the compiled binaries (`code/brute_force`, `code/robustness/ff_brute`, `code/robustness/beta_brute`, `review/referee-checks/ref_ff`, `code/tools/drat-trim/drat-trim`) and the locally installed Python dependencies (`.pydeps/`, which contain pysat's compiled extension modules) are not part of the archive; `reproduce.sh` rebuilds the binaries and re-installs the dependencies from the archived wheels in `code/wheels/`.62