1# Research plan23Run 951263fc-5b4f-4db3-8660-153a5f5ec04a · AS-WP-2026-0001 · mode: theoretical (+computational) · discipline: mathematics45Working title: Sharp Zero-Forcing Bounds for Generalized Petersen Graphs: Computational Discovery and Certified Proofs (short: Zero Forcing in P(n,5)).67## 1. Research question89Let P(n,k), n > 2k, be the generalized Petersen graph on u_0..u_{n-1}, v_0..v_{n-1} with edges u_i u_{i+1}, u_i v_i, v_i v_{i+k} (indices mod n). Let Z(G) be the zero-forcing number.1011Primary question. For k = 5 and n >= 11: what is Z(P(n,5))? Concretely, (Q1) for which n can the exact value be independently certified; (Q2) how does the value depend on n (residues, gcd(n,5), parity); (Q3) does an infinite arithmetic family of n admit a proved exact value or a strictly improved bound; (Q4) can lower bounds be established by forts, fort covers, path covers / maximum nullity or finite-state arguments.1213Secondary question. Can every reported value be backed by an independently checkable certificate (replayed chronology for upper bounds; exhaustive search, checked SAT proof, or handwritten proof for lower bounds)?1415## 2. Hypotheses and propositions1617Proof obligations (must be proved before use; no data needed):1819- P1. The final black set of the closure process is independent of the order of forces (so "S is zero forcing" is well defined and one replay suffices).20- P2. Fort characterization: S is a zero-forcing set iff S meets every fort.21- P3. Automorphisms map zero-forcing sets to zero-forcing sets of equal size, so orbit reduction in brute force loses no minimum.22- P4. The SAT/CP encoding of the forcing process is sound and complete for a fixed round horizon T, with T chosen so that every forcing process terminates within T rounds.23- P5. For n >= 11, P(n,5) is simple, cubic, connected, has 2n vertices and 3n edges, and its inner subgraph is gcd(n,5) disjoint cycles.2425Falsifiable hypotheses about Z(P(n,5)) (all status: proposed):2627- H0 (null). The exact values on the feasible range are already determined by published work. Tested in Stage B against the verified literature; if true, no novelty claim is made.28- H1 (uniform upper bound). There is a constant C and an explicit template S(n) with |S(n)| = C forcing P(n,5) for all n >= n_0. The literature reports 12 for the subfamily P(24r,5); whether 12 (or smaller) holds for all large n is open to us until verified. Refuted if certified exact values exceed every candidate C infinitely often within the tested range, or if no uniform template is found.29- H2 (eventual periodicity). Z(P(n,5)) is eventually periodic in n with a period dividing a small modulus m (candidates m in {1,2,3,4,5,6,8,10,12,24}; the modulus will be chosen only from n <= 30 data and then tested on the fixed holdout in §7). Refuted by any holdout value disagreeing with the prediction.30- H3 (fort lower bounds match). For every n in the certified range, the integer fort-hitting-set optimum equals Z (this is P2, so it is a check), and a fractional or disjoint-fort bound is within 1 of Z. The second part is falsifiable and measures whether fort arguments can give tight lower bounds.31- H4 (small-n exceptions). P(11,5) = P(2k+1,k) and possibly a few further small n behave differently from the eventual pattern. Tested by direct computation.3233## 3. Novelty target and intended contribution3435Target, in qualified language: to our knowledge, a certified table of exact Z(P(n,5)) values on a range beyond the published one, and at least one of (a) a proved exact value or sharp bound on a previously unresolved infinite arithmetic subfamily, (b) a strictly stronger general upper or lower bound with proof, (c) a rigorously verified counterexample to a published or natural conjecture, or (d) a clearly finite certified classification that is itself new. The novelty of whatever is achieved is decided only after plan/prior-art.md exists (Stage B) and is re-checked by the referee context. If none of (a)–(d) is established, the run reports an honest null result and expects quality_failed.3637## 4. Methodology (theoretical, with computational support)3839Two tracks with different evidentiary standards. Track A (computation) produces exact values, witnesses and counterexamples; it can refute but never prove a statement about all n. Track B (proof) supplies uniform constructions for upper bounds and fort / path-cover / finite-state arguments for lower bounds, with every lemma written out and the inductive step checked under the modulo-n adjacency.4041Tools: Python 3.14, python-sat (CaDiCaL/Glucose backends) and, if installable, OR-Tools CP-SAT as a second exact path; brute force with orbit reduction as gold standard for small n; a fort-based hitting-set formulation as an independent third path; DRAT/LRAT proof checking if a checker can be built from an allowlisted host; Lean 4 only if the toolchain installs, with scope reported exactly. Compute: the 16 cores of worker M4M64c, one job per n, wall-clock timeouts, checkpoints, timed-out = unknown.4243## 5. Evaluation metrics, proof obligations and inclusion criteria (fixed before any analysis)4445Certification status per n (never collapsed):4647- fully certified: upper witness replayed by closure_oracle.py, and lower bound by exhaustive brute force, a checked external SAT proof, or a handwritten proof;48- solver-supported: two independent exact formulations agree on optimality without an external certificate;49- candidate: upper bound only;50- unknown: timeout or disagreement (disagreement is a bug and halts the table until resolved).5152Metrics recorded in results/metrics.json: number of n per status; largest fully certified n; pairwise agreement of brute force / SAT / hitting set on every n where all finish; count of order-independence tests passed; holdout pass/fail per conjecture; per-n wall time, CPU time, peak memory, solver version, certificate hash, timeout flag.5354Inclusion criteria for the manuscript: a value appears in the main table only with status fully certified or solver-supported, labeled; a statement is called Theorem only with a complete proof read independently in the referee context; anything else is Conjecture, Observation or Computational Result.5556## 6. Competing explanations5758- A pattern on n <= 30 reflects small-n effects, not asymptotics; countered by the fixed holdout.59- A constant value could be an artifact of a particular upper-bound construction while true values are lower; countered by certified lower bounds.60- Residue dependence might come from gcd(n,5) (inner cycle structure) rather than from n mod 24 or other moduli; both are tested explicitly.61- Solver agreement may hide a shared bug (too short round horizon, wrong adjacency); countered by brute force on n <= 14 and by P4/P5 proofs and tests.62- A claimed improvement may already be implied by a general bound in the literature; countered by the prior-art gate.6364## 7. Pre-registration6566The following are committed now, before any P(n,5) computation.6768Holdout. Conjectures are fitted only on n in [11, 30]. Holdout H = {32, 35, 37, 41, 44, 48} is frozen; values for n in H are computed but not inspected for pattern fitting, and are used only to test the registered conjectures. If budget forbids some holdout values, they are reported as untested, not replaced.6970Tests to run first, in order:7172- T1 graph invariants, n = 11..48, k = 5: two independent constructors produce identical canonical edge lists and SHA-256; 2n vertices; 3n edges; all degrees 3; connected; inner subgraph is gcd(n,5) cycles; no loops or multi-edges. Also P(5,2) (Petersen) built for T3.73- T2 order independence: for n = 11..16, 200 random S of sizes 3..8 per n, 20 random force orders each; the final black set must be identical across orders (empirical check of P1 alongside the proof).74- T3 reference cases: Z(Petersen) = 5 (AIM 2008, to be verified against the fetched text), Z(C_m) = 2, Z(K_m) = m - 1, Z(path) = 1, plus two small P(n,5) values or bounds extracted from the 2020 paper in Stage B. Mismatch halts the study until the definition is reconciled.75- T4 brute force with orbit reduction, n = 11..14 (and higher while each n finishes within 30 min); witnesses and "no set of size Z-1 works" recorded.76- T5 SAT exact values, n = 11..30 then 31..48, time limit 20 min per n; round horizon T = 2n - |S| + 1; witness replayed by closure_oracle; lower side by UNSAT at size Z-1 with DRAT if a checker is available, otherwise solver-supported.77- T6 fort hitting set (or CP-SAT) as independent exact path on every n where T5 finished; disagreement is an error, not a result.78- T7 only after T1–T6 on n <= 30: register conjectures in plan/conjectures.jsonl with timestamp, then compute holdout H and record outcomes.7980Theorem gate (unchanged from CLAUDE.md §8): precise statement; literature search; falsification by brute force/SAT over the feasible range; boundary cases n near 11; independent derivation of each step; referee context; point-by-point response.8182## 8. Failure modes and null-result pathway8384- Result already known: reported as reproduction, no novelty claim, quality_failed.85- No infinite-family proof: no theorem published; the certified finite table, registered conjectures with holdout record and the failed attempts are reported; quality_failed expected.86- No external proof checker: lower bounds beyond brute force stay solver-supported and are labeled so.87- Timeouts: entries unknown; no extrapolation across gaps.88- Counterexample to a published claim: verified by two methods (brute force where possible) before being reported, in restrained wording.89- Lean unavailable: formal scope reported as none.90- Budget exhaustion (session shows about USD 12): checkpoints each stage; a smaller fully certified study is preferred.9192## 9. Deliverables mapped to the artifact contract9394plan/ (this plan, prior-art.md, feasibility.json, conjectures.jsonl, formal-setup.md); sources/ (sources.json via scholar_add_source, reading depth per source); data/ (generated edge lists with SHA-256 and manifest.json; no external or synthetic data); code/ (the constructor, closure oracle, brute force, SAT/ILP solver, upper/lower verifiers, reproduce.sh, pinned requirements, README, code/proofs/{handwritten,lean,certificates}); results/ (exact_values.csv, known_vs_new.csv, witnesses and certificate logs, solver_runs.jsonl, counterexamples.jsonl, derivations.md, robustness.md, metrics.json, experiment-log.jsonl, figures/, tables/); manuscript/ (main.tex, references.bib, main.pdf, abstract.md, metadata.json); review/ (review-1.md, revisions.md).9596## Prior art and novelty9798Full audit: plan/prior-art.md (20 verified sources; three read in full text: Rashidi et al. 2020, Krishnan 2026, Krishnan–Ma–Zhang 2026).99100What exists for k = 5. Z(P(n,5)) ≤ 12 for all n ≥ 11 (Alameda et al. 2018; Rashidi et al. 2020, Thm 2.2). Rashidi Thm 2.1 gives smaller upper bounds only at n = 12, 13, 14, 16 (8, 10, 11, 9). Z(P(11,5)) = 6 (Rashidi Thm 2.6, independently confirmed by exhaustive search in Krishnan 2026). Z(P(24r,5)) = 12 for r ≥ 1 is attributed by Rashidi (Remark 2.4) to Alameda et al.; the Alameda primary text could not be fetched in this sandbox, so this is recorded as a second-hand report and will be cross-checked at n = 24 (and at the holdout value 48 only after conjecture registration). General lower bounds are weak: Z ≥ min{5, ⌊n/5⌋} + 1 (≥ 6 for n ≥ 15) and the girth bound Z ≥ 4. For k = 3 and 4 the sharp stabilization theorems were proved in 2026 by a boundary-of-first-sources argument plus a column-deletion lemma (stated for general k), finite SAT/DRAT or fort checks, and Lean 4 (k = 3); Krishnan 2026 lists thresholds and lower bounds for k ≥ 4 as open, and neither 2026 paper says anything about k = 5. Rashidi's P(n,3) theorem was shown false at n = 12, so figure-based case analyses in that paper are cited only with independent confirmation.101102Gap addressed. To our knowledge, no exact value of Z(P(n,5)) is published for any n ≥ 12 with 24 ∤ n, and no stabilization threshold or uniform lower bound for k = 5 is known. Hypothesis H0 (everything already known) is therefore rejected at the literature level for 12 ≤ n ≤ 23 and for all n not divisible by 24; it remains true for n = 11 and n ≡ 0 (mod 24), which will be reported as reproductions.103104Novelty language. Any theorem of the form "Z(P(n,5)) = 12 for all n ≥ n_0, with n_0 sharp and all smaller values listed" would, to our knowledge, be new; its proof method would be adapted from Krishnan–Ma–Zhang and credited as such. The upper bound 12 is not new. Values at n ≡ 0 (mod 24) are not new. A certified finite table alone is new data but, per CLAUDE.md §13, not by itself a publishable contribution. Prioritized targets N1–N4 are listed in plan/prior-art.md §5; risks (unread Alameda statement, possible concurrent k = 5 work, unindexed reports) are listed in §4.105106## Design107108Final protocol (Stage 3). Definitions, propositions P1–P9, candidate theorems T1–T4 and the counterexample plan CS1–CS7 are fixed in plan/formal-setup.md; this section records the operational protocol. No data are involved: the graphs are generated from the definition, and nothing in this study is synthetic in the statistical sense (there is no simulated or sampled data; random seed sets in tests T2/T8 are random inputs to deterministic checks and are recorded with their seeds).109110Objects. P(n,5), 11 ≤ n ≤ 48 for exact values (pilot 11–20, discovery 21–30, holdout {32,35,37,41,44,48}; extension beyond 48 only if a solver finishes n = 48 within 20 min and budget remains). Boundary minimization β_p(n) for 12 ≤ p ≤ 30 and 13 ≤ n ≤ 60, and the finite SAT window [n_1, N_max] of the lower-bound proof, where N_max = 11⌊(p+11)/2⌋ is fixed by the chosen p (plan/formal-setup.md §5).111112Known values excluded from novelty (fixed before computation): n = 11 (6), n = 14, 16 (8), n = 19, 21 (10) via the isomorphism P6 and the published k = 2,3,4 theorems; n ≡ 0 (mod 24) (12) via Alameda et al. as reported second-hand. These serve as solver reference tests and are labeled "known" in results/known_vs_new.csv.113114Pipeline and modules (code/).1151. graph_constructor.py: two independent constructors (edge-list formula; adjacency built from the three cyclic permutations) with canonical labeling, SHA-256 of the sorted edge list, GraphML/JSON export; invariant tests T1 and the isomorphism test for P6.1162. closure_oracle.py: deterministic closure with full chronology; random-order test T2; replay function used by every verifier.1173. brute_force.py: enumeration by cardinality with D_n-orbit representatives (P3), bitset closures; gold standard for n ≤ 14 and wherever a size finishes within 30 min; records the exhausted size Z − 1.1184. sat_or_ilp_solver.py: (a) round-based SAT encoding of P4 with T = 2n − s, python-sat, CaDiCaL primary and Glucose secondary, DRUP proof output when supported; (b) fort-cover SAT with lazy fort generation and first-force normalization; (c) boundary minimization for β_p(n). One process per n, 16-core pool, 20 min wall-clock limit per instance, timeouts recorded as unknown.1195. verify_upper_bounds.py and verify_lower_bounds.py: independent checkers (no import of the solver module); external DRAT checker if drat-trim can be built in Stage G.1206. reproduce.sh / reproduce_all.py: rebuilds everything tractable and re-checks all certificates; requirements.txt pinned.121122Decision rules. A value enters results/exact_values.csv with status fully certified only when the witness replays and the lower bound is brute force, an externally checked proof, or a handwritten proof; two agreeing solver paths without an external certificate give solver-supported; any disagreement halts. Conjectures are registered (plan/conjectures.jsonl) from n ≤ 30 only, then the holdout is computed once. p for the boundary route is chosen by the exact β_p(n) data (CS2), not guessed. T1 is asserted only if L1–L3 close with per-n certificates; otherwise T2, the refutation branch, or the finite table T4 is reported with its honest label, and the publication gate is expected to fail if no theorem is proved.123124Compute and provenance. Per instance: start/end UTC, n, k, graph SHA-256, command, solver version, wall and CPU time, peak RSS, timeout flag, witness, certificate path and SHA-256, written to results/solver_runs.jsonl and results/experiment-log.jsonl. Worker: 16 cores of M4M64c, as reported by the environment; no cluster metrics are invented.125126Formal verification. Lean is attempted once in Stage G (toolchain install under the allowlist); if unavailable, the formal scope is reported as none. Target statements, in order, are P1, P7, P8 (plan/formal-setup.md §7). No CAS component.127128## Log129130- 2026-10-30 Stage 0 preflight. Read CLAUDE.md and input/run.json. Environment probe: Python 3.14.7, pip 26.2.1, 16 CPUs, tectonic, gcc, git present; pdflatex/latexmk, lean/elan/lake, drat-trim, pysat, ortools, networkx absent. Judged feasible as theoretical+computational mathematics with no restricted activities. Noted live budget (~USD 9.6) is far below the nominal USD 150 cap; plan sized accordingly. Wrote plan/feasibility.json and this plan. Research not started.131- 2026-10-30 Stage 1 framing. Rewrote the plan with explicit proof obligations P1–P5, hypotheses H0–H4, qualified novelty target, fixed certification statuses and inclusion criteria, competing explanations, and a pre-registration section. Froze the conjecture-fitting range n in [11,30] and holdout H = {32,35,37,41,44,48} before any P(n,5) computation. Session budget counter now reads about USD 12 (earlier note said 9.6); plan sizing unchanged. No computation or literature fetching yet.132- 2026-10-30 Stage 2 literature audit. Registered 20 sources via scholar_add_source (all verified; 3 full-text, 8 abstract, 9 metadata). Read in full: Rashidi et al. 2020 (OA PDF), Krishnan 2026 and Krishnan–Ma–Zhang 2026 (arXiv HTML + PDF); PDFs and SHA-256 kept in sources/fulltext/. Alameda et al. 2018 (primary source of Z(P(24r,5)) = 12) could not be fetched: De Gruyter and the Iowa State repository are outside the sandbox allowlist; recorded as abstract-level with the 24r claim marked second-hand. Wrote plan/prior-art.md, sources/source-map.json (13 mapped claims) and the "Prior art and novelty" section above. Preliminary closure check (code/prelim_check_published_constructions.py, output plan/prior-art-prelim-check.txt): all published 2k+2 and r(s+2) constructions force P(n,k) at k = 2, 3, 5 on the tested ranges; lower bounds untouched. Decision: H0 rejected at the literature level for 12 ≤ n ≤ 23 and 24 ∤ n; primary target N1 (sharp stabilization theorem for k = 5 by the boundary/deletion method). Session budget counter ~USD 4 of 33.6. Next: Stage C oracles.133- 2026-10-30 Stage 3 design. Wrote plan/formal-setup.md (definitions D1–D7, foundational propositions P1–P9 with proof routes, candidate theorems T1–T4, the Krishnan–Ma–Zhang-style lower-bound strategy L1–L5 adapted to k = 5 with N_max = 11⌊(p+11)/2⌋, counterexample plan CS1–CS7, Lean/checker plan, conjecture-registry schema) and the Design section above. Preliminary check code/prelim_check_isomorphisms.py (output plan/formal-setup-prelim-check.txt): the explicit map ψ(v_{jk}) = u_j, ψ(u_{jk}) = v_j is an isomorphism P(n,5) → P(n,l), 5l ≡ 1 (mod n), for all 11 ≤ n ≤ 60 with gcd(n,5) = 1; the partner index is ≤ 4 exactly at n = 11, 14, 16, 19, 21, so Z(P(14,5)) = Z(P(16,5)) = 8 and Z(P(19,5)) = Z(P(21,5)) = 10 are implied by the published k = 3, 4 theorems and are removed from the novelty claim (prior-art.md §7 added). The 12-vertex forcing order of P7 replays legally for 13 ≤ n ≤ 40. Decision: T = 2n − s rounds in the SAT encoding (exact bound from P4); p for the boundary route to be chosen from exact β_p(n) data, not guessed. Budget counter ~USD 2 used this stage. Next: Stage C oracles.134- 2026-10-30 Stage 4 execution (interim, 18:00 UTC). Tooling: python-sat 1.9.dev17 and sympy 1.14.0 installed into .pydeps from PyPI wheels fetched by curl (Python's Homebrew OpenSSL cannot use the sandbox trust store; SHA-256 of each wheel checked against the PyPI digest, wheels archived in code/wheels/); drat-trim built from the GitHub source (code/tools/drat-trim, SHA-256 recorded). T1 passed for n = 11..48 and P(5,2); T2 1200/1200; lemma checks CS6/T8/P6/L2/P7 all pass (results/lemma_checks.json). Brute force (C oracle, D_n orbit reduction, 16 threads) certified Z(P(n,5)) = 6, 8, 9, 8, 8, 8, 10, 10, 10, 10, 10, 11 for n = 11..22 in seconds to minutes; n = 23, 24 running. SAT paths agree on n = 11..16 (fort cover with DRAT, round encoding). Boundary table p = 12..24, n = 13..30 computed: beta_p(n) >= 12 holds at n = 24 and 26..30 for p = 18, 19 (and 26..30 for p = 20..23), fails at n = 25 for every p <= 24 (three inner pentagons plus five outer vertices, boundary 10) and at n = 26 for p = 24. Decision (rule L4): p = 18, n_1 = 26, N_max = 154. Certified window p = 18 on the fit range 26..30 running; the window 31..154 and the holdout are computed only after conjecture registration.135- 2026-10-30 Stage 4 execution complete (19:05 UTC). Results: exhaustive C oracle certified Z(P(n,5)) for n = 11..27 (6,8,9,8,8,8,10,10,10,10,10,11,12,12,12,12,12; sizes 1..Z−1 exhausted, orbit reduction by D_n per P3); fort-cover DRAT certificates (CaDiCaL + drat-trim) for n = 11..19 (20..22 still running at the time of this entry) agree; Glucose round encoding agrees for n = 11..17 and times out beyond. Boundary route (Krishnan–Ma–Zhang method adapted to k = 5): p = 18, n_1 = 26, N_max = 154; F(n,18) UNSAT with drat-trim-verified DRAT proofs for all 26 ≤ n ≤ 154 (129 certificates, plus n = 24 and five p = 20 cross-checks; 37 GB of proofs, hashes recorded, generator provided); independent checker rebuilt every CNF and re-verified every proof (results/lower_bound_verification.json, 134 + 12 certificates, all ok). Theorem 5.1 (results/derivations.md, full proofs P1–P9, Lemmas 3.1–3.5): Z(P(n,5)) = 12 for all n ≥ 23, Z(P(22,5)) = 11, explicit table for 11 ≤ n ≤ 22; threshold sharp. The boundary method fails at n = 25 for every p ≤ 24 (inner pentagons; obstructions archived in results/counterexamples.jsonl), so n = 23, 24, 25 rest on enumeration (n = 24 also on a p = 18 certificate). Holdout {32,35,37,41,44,48}: all predicted 12, all certified 12; no 11-vertex forcing set found by a 600 s fort-cover search. Conjectures C1–C3 marked proved, C4 computationally tested, H0 refuted, H4 confirmed. Novelty, qualified: values at n ∈ {12,13,15,17,18,20,22,23} and the sharp stabilization theorem for k = 5 are, to our knowledge, new; the bound 12, n = 11, n = 14,16,19,21 (via isomorphism) and 24 | n are known. Artifacts: results/{exact_values.csv, known_vs_new.csv, upper_bound_witnesses.jsonl, lower_bound_certificates.jsonl, boundary_certificates.jsonl, boundary_table.jsonl, solver_runs.jsonl, counterexamples.jsonl, derivations.md, robustness.md, metrics.json, experiment-log.jsonl, tables/}, code/ (all modules, reproduce.sh, requirements.txt, README), code/proofs/{handwritten, certificates}. Session budget ≈ USD 30 of 48 used. Open for later stages: Lean (Stage G), figures as TikZ/pgfplots (no matplotlib in the sandbox), compressing or omitting the 37 GB of DRAT files from the archive with hashes, re-running verify_lower_bounds.py and build_tables.py once the n = 20..22 fort-cover certificates finish.136- 2026-10-30 Stage 5 robustness, completion (Stage 6 start). The two background enumerations (ff_brute n = 31..40, exhaustive β check) had finished; ran code/robustness/collect_robustness_metrics.py (results/robustness/summary.json; metrics.json["robustness"]) and filled the six placeholders in results/robustness.md from it: 344,080,112,924 first-force sets in 2,345.7 s (n ≤ 40); 135 boundary + 14 fort-cover certificates re-verified, all ok. Found and corrected a textual error in results/derivations.md §4.2: the archived n = 25, p = 18 obstruction is two complete inner pentagons {v_i : i ≡ 0,1 (5)} plus eight outer vertices (boundary 10), not "three pentagons minus two vertices"; recounted independently in code/build_figures.py. No mathematical statement changed.137- 2026-10-30 Stage 6 manuscript. Figures: matplotlib unavailable, so code/build_figures.py emits TikZ/pgfplots sources (results/figures/src/) compiled with the locally cached tectonic bundle using the autoscholar class (results/figures/*.pdf, 9 files: anatomy P(13,5)/P(15,5), P7 chronology on P(14,5) and the optimal 8-set chronology on P(15,5) (both re-validated force by force before drawing), exact values 11..48, the n = 25 obstruction, window and enumeration scaling, β_p(n) heat map). Tables: code/build_manuscript_tables.py writes results/tables/tab_*.tex from the CSV/JSON artifacts (exact values, paths per n, brute force, witnesses, boundary table, window scaling, fort-cover certificates, conjecture registry, verification summary, machine-checking scope). Wrote manuscript/main.tex (25 pages: theorem, all proofs P1–P9 and Lemmas 3.1–3.5, encodings, framework, results, robustness, discussion with Question on n_0(k) = 5k − 2, limitations, appendices incl. round encoding, protocol, reproducibility, scope, process note), abstract.md, metadata.json (synthetic: false). Registered 45 further reported values (71 total). latex_build: ok, zero errors; residual warnings are minor over/underfull boxes. Not done in this stage: review/ (Stage I) and Lean (none; scope reported as none in the paper).138- 2026-10-31 Stage 8 revision, second pass (after quality-gate failure). Causes found: seven registered numbers typeset with `{,}` separators that the consistency check cannot match (rewritten with plain separators); pysat's compiled extension modules in .pydeps/ flagged as binaries (.pydeps/ now excluded from the archive, reproduce.sh re-installs from code/wheels/); two log files still being written by background jobs after the platform's checksum snapshot (no job is left writing into the tree at the end of this pass); reproduce.sh default mode cut by the 60 min limit (trimmed to about 25 min, removed pieces in FULL=1). Referee F1 closed: n = 23 fort-cover DRAT proof verified by drat-trim (exit 0, 2486 s) and recorded; the 7.7 GB n = 25 proof file could not be checked within the stage limits, so it is recorded with status unknown, counted nowhere, and the manuscript says n = 25 rests on the two exhaustive enumerations. Observation 7.7, Tables 1 and 9, abstract, metadata, revisions.md, review-1.json, reproducibility.md updated; no theorem statement changed.139