Session 045 (2026-09-01) — Paper A: expert-review revision (five suggestions)

Input

An external expert review of the frozen paperA.pdf (session 044 state, 13 pp) with five suggestions:

1. §2 (certificate-method background) and §4 (obstruction analysis) do not belong — Paper B material; make the paper a focused note (theorem, proof, dog-leg, formalization).
2. Do not lean the introduction on anthropic2026riemann (dated after the reviewer's knowledge; @misc to a GitHub tag; not peer-reviewed; R-004 does not depend on it mathematically).
3. Verify the Lagarias-gap claim against the published version (Ann. Inst. Fourier 2007) and the latest arXiv revision (whose comment mentions a remainder-term correction).
4. Venue: Math. Comp. / Exp. Math. / Res. Number Theory or a formalization venue; pitch as "explicit + machine-verified transfer theorem, with a repair to a classical contour estimate".
5. The three derived zero-count bounds are the soft spot of the trust boundary; include their derivations in an appendix.

User decision (AskUserQuestion): apply all five.

Verification work before editing

• Suggestion 3 — DONE, gap confirmed in both versions. Downloaded the published version (AIF Tome 57 (2007) fasc. 5, pp. 1689–1740, DOI 10.5802/aif.2311; saved as research/paper/refs/lagarias-AIF-2007-published.pdf, 53 pp). The (6.12) stepping and the sentence "an upper bound … that decreases geometrically at each step" appear verbatim on pp. 1724–1725 (only Lemma 6.1 → Lemma 6.2 renumbered). No erratum listed on the journal page. The local arXiv copy is already v4 (4 May 2005 — the last revision); its comment "correction to remainder term in Theorem 1.1" is the O(√n) → O(√n log n) change flowing from the left-vertical bound (6.13), not from (6.12). Conclusion: §3.1 stays "repair of a gap"; a sentence stating exactly this, with page-precise citations, was added.
• Suggestion 2 — dependency check. NguyenRH1 imports from zeta-23-lean only infrastructure modules (Statement, SeamClosed, RvM., WeilEF.ZeroSummability, GammaFacts., FromPNTPlus.*, Analytic.RectangleLogDeriv, ZetaReflect); grep confirms no density-theorem statement (thmA/thmB/two_thirds/…) is referenced (the one "Zeta23.Final" hit is a docstring about conventions). So the library is a software dependency, cited as such in Appendix B; the density theorem itself is gone from the paper.
• Suggestion 5 — derivations worked and grid-checked (E-035). Inputs: Rosser Thm 19 (T ≥ 1467; used in the reading-independent form |N−P| ≤ R + 0.2/T), Trudgian-II (1.2) |S| ≤ 2 to 6.8·10⁶, Trudgian-II Cor. 1 theta remainder 0.2/T, Trudgian-II Thm 1 (published constants 0.112/0.278/2.510, corroborated by Hasanalizade–Shen–Wong 2022 Table 1: 0.1120/0.2780/3.3850 = 2.510 + 7/8), and γ₁ = 14.13. Results:
• ZeroCountGlobalProp: Rosser + (1.2) for all T ≥ 2 (slack ≥ 6.69 low range, ≥ 662 Rosser range; F increasing, F(2) = 2.616).
• ZeroCountProp2: Rosser + (1.2) for all t ≥ 10 (slack ≥ 0.78 low, ≥ 0.166 Rosser; coefficient 0.59231 < 0.6).
• ZeroCountProp: NOT Rosser-derivable for all t. The two-endpoint Rosser bound has log-coefficient 1/(2π) + 0.274 = 0.433155 > 0.433, so it proves the declared bound only for u ≤ e^{106.6} (E-035 locates the sign change at log u = 106.57). Trudgian Thm 1 covers u ≥ 10⁸ (slack 0.052 at 10⁸, increasing). Since the Schwarz squeeze (LiSqueeze) consumes ZeroCountProp at radii → ∞, the universal form is genuinely needed; the honest attribution is "Rosser and Trudgian". Abstract/intro/App. B wording changed accordingly.
• E-035 first run tripped on a precision artifact (T₂ − T₁ lost at T ~ 1e31 in dps 30); fixed by passing the window width exactly and dps 60. ALL CHECKS PASS; registered in research.db (session 45).
• Also found while editing: the "≈ 0.9√n" cost of the enlarged majorant (Step-4 footnote, App. B) is the 2F-era figure; with the 4F bridge it is ≈ 1.8√n (dropped term (T/2π)(1 + log 2π) ≈ 0.4517·T per unit bridge factor; the 256 trail entry at n = 8·10⁴ is the 2F value). Corrected in both places. C₀(t) had never been written out explicitly in the paper — Appendix C fixes that.

Edits to paperA.tex (honesty audit re-opened for these lines, D-060 §5)

1. Abstract: "derived from Rosser's … bound" → "derived in Appendix C from the explicit Riemann–von Mangoldt error bounds of Rosser and Trudgian".
2. Introduction rewritten: Li criterion + Voros only (Weil-positivity and the 2/3 density theorem removed); "transfer theorem" framing; one clause on the larger project; roadmap paragraph to §2 / §2.1 / App. A / App. B / App. C. Novelty sentence: "Rosser and Trudgian".
3. §2 "Background: the Weil-form certificate method" DELETED; §4 "Obstruction analysis" DELETED (both Paper B material). Three hard-coded "Section 3" references → \ref{sec:theorem}.
4. §2.1 (dog-leg): page-precise citation (p. 1725, (6.12)); the mechanism sentence now names (6.10) and (6.12); new sentences: same step in the published version pp. 1724–1725 and arXiv v4, the v4 remainder correction concerns (6.13), no erratum listed; "gap in the displayed proof, not a claim that the conclusion fails".
5. Step 2: "finite-range verification |S| ≤ 2 to 6.8·10⁶" (the unused |S| ≤ 1 to 280 dropped) + pointer to App. C; F, C₀, Z₂ described as the three explicit majorants of App. C.
6. Step-4 footnote + App. B: 0.9√n → 1.8√n (4F form) with the explanation.
7. App. B first paragraph rewritten: NguyenRH1 toolchain; zeta-23-lean cited as the imported library (\cite{zeta23lean}, software) with the list of infrastructure used and the statement that none of its density theorems is referenced; the rebuild + axiom re-audit kept as due diligence on the dependency.
8. App. B table: the three zero-count rows now state the windows precisely and point to App. C (A)/(B)/(C); Source column "Rosser for t ≤ 10⁸, Trudgian beyond" for ZeroCountProp. The generic post-table derivation paragraph replaced by "all counts with multiplicity" + pointer to App. C. Final conditional paragraph: "Rosser and Trudgian".
9. NEW Appendix C "Derivation of the three zero-counting bounds": Lean statements written out (F, C₀, Z₂ explicit); the note that (B) is consumed at arbitrarily large heights; inputs (R1)–(R5) with the reading-independence footnote (Trudgian Table 1 vs HSW Table 1); the window bound (W); derivations (A), (B) [three regimes: (1.2) below 1467, Rosser to 10⁸, Trudgian Thm 1 beyond], (C); E-035 closing sentence with the direct (W)-slacks.
10. AI Contribution Statement: sessions 001–045, E-001–E-035. Revision date 2026-09-01. Header comment updated.
11. references.bib: zeta23lean (software @misc) and hasanalizade2022counting (JNT 235 (2022) 219–241, DOI verified via CrossRef) ADDED; anthropic2026riemann left in place (draft.tex, frozen, still cites it).

Compile: pdflatex + bibtex + 2× pdflatex → 15 pp, 0 errors, 0 overfull hboxes, 0 undefined references/citations (four long Appendix-C displays converted to split).

Submission package

• cover-letter.md REWRITTEN (was stale: three hypotheses → seven; "Trudgian's zero-counting bounds" → Rosser/Trudgian derived in App. C; the retracted Misguich–Voros verification → Johansson; "Research Ai" → Independent researcher; the reviewer's pitch adopted; the Lagarias repair paragraph with the published-version check; venue alternatives listed).
• referee-list.md: Trudgian and Lagarias entries updated; note on item 4 (the repair); venue swap note.

Reference downloads (research/paper/refs/, not committed unless asked)

lagarias-AIF-2007-published.pdf (open access, Centre Mersenne), trudgian-1208.5846.pdf (arXiv v2), hsw-2107.06506.pdf (arXiv v1). Rosser 1941 (JSTOR) and Rosser–Schoenfeld 1962 (Project Euclid) could not be fetched from this environment; the Rosser threshold question (1467 per Trudgian's table vs 2 per HSW's table) is handled by using the conservative 1467 and covering the range below by (1.2).

Open items

• The user's own Lagarias correspondence package (research/correspondence/lagarias-F-D-package/) is untouched; the published-version check above (pp. 1724–1725 verbatim; no erratum) is directly usable in that letter.
• Trudgian-II published Theorem-1 constants (0.112/0.278/2.510) are taken from HSW's table + memory of the JNT version; the arXiv v2 prints 0.111/0.275/2.450. The paper uses the larger published constants and cites HSW as corroboration. A direct check of the JNT text would close this (ScienceDirect blocked here).