Session 042 (2026-08-26) — REVIEW REVISION: the user's Paper-A review fully actioned

Mission

The user returned a detailed expert review of the ii′-7 Paper A ("the revised Paper A is dramatically stronger ... but I would not submit this exact PDF yet") with six required fixes. Action all of them, with verification where the review flagged a factual vulnerability.

1. THE CERTIFICATE RETRACTION (the review's top finding — REAL)

The review: Step 5's "λ_n > 0 to 5×10⁵ by Misguich–Voros" could not be allowed to carry the finite splice unless checked theorem-by-theorem, since the cited reference is explicitly Discretized Keiper/Li. Verification performed (not assumed):

• The bib entry is Voros alone, Exp. Math. 29(4):452–469, 2020 (arXiv:1703.02844).
• Fetched and read the paper (pypdf extraction of the full text): Misguich computed the DEFORMED sequence {Λ_n} (Voros's eq. 36), not the ordinary λ_n — and the source is "G. Misguich, calculations ... (private communications, 2017)" [their ref. 25]. Doubly unsuitable: wrong sequence AND not a checkable published source.
• The same read surfaced the sound replacement: "n = 10⁵ attained by Johansson [18, § 4.2]" — F. Johansson, "Rigorous high-precision computation of the Hurwitz zeta function and its derivatives", Numer. Algor. 69 (2015) 253–270 (arXiv:1309.2877). Verified in that paper's § 4.2 ("Computing the Keiper–Li coefficients"): the ORDINARY coefficients λ_0…λ_{100000} computed with rigorous interval-arithmetic error bounds, all positive ("shows agreement with Keiper's conjecture (and the Riemann hypothesis)"), λ_100000 certified to ~2900 digits.
• AND the novelty-relevant precursor: Oesterlé [26, prop. 2] (typescript 2000, revised 2001, uncirculated, cited in Voros): RH-to-T₀ ⟹ λ_n ≥ 0 for n ≤ T₀² — the finite-height STATEMENT exists unpublished. Action: Lean perimeter LiVerifiedUpTo reduced (5·10⁵) → (10⁵) (three theorem sites + docstrings; the assembly's hfinite branch uses exactly n < 10⁵, so nothing else changes; rebuild GREEN 8775 jobs; audit re-run: 29 decls, 3 standard axioms only). Paper Step 5 rewritten as the declared certificate LiVerifiedUpTo($10^5$) with the honest two-leg evidence (Johansson to 10⁵ + E-011/E-015 to 3000) and a footnote recording the retraction. Archive: R-004, D-037 erratum ADDENDUM, NGUYEN.md (3.2 + ii′-7 + Ledger #6), STATE.md.

2. Hypothesis count (user-caught arithmetic error)

"Eight named hypotheses" was wrong: 2 computational + 5 analytic = SEVEN (the analytic list itself names five: ZeroCountProp, ZeroCountProp2, ZeroCountGlobalProp, NoLowZeros, MZeroProp). Fixed everywhere; per the review's advice, Appendix B now carries the final Lean signature copied verbatim (tt-quote form, unicode via math) and the count is taken from the signature, not from memory.

3. Theorem statement ↔ trust boundary

Both Theorem environments now assume (i) RH verified to T₀ (Platt–Trudgian, interval arithmetic) and (ii) λ_n > 0 for n ≤ 10⁵ (Step 5) — the abstract's "conditional on RH verification and finite Li computations" and the formal theorem's hypotheses now agree. Appendix B gains the instantiation list mapping each of the seven hypotheses to its cited source (Platt–Trudgian also discharges NoLowZeros via the lowest zero at 14.134…; Trudgian 2014 discharges the three counting Props; E-023 discharges MZeroProp).

4. Novelty hedged

"first assembled explicit chain" → "we have found no previous explicit assembly"; "maximal content of the Li route short of RH" → the narrow Voros form (eventual positivity of all large λ_n ⟹ RH, so no result short of RH asserts an infinite positive tail). Oesterlé's unpublished precursor (n ≤ T₀²) explicitly noted with a new bib entry (oesterle2000); Lagarias 2007's published weaker window (n ≤ T²/(4 log² T)) already in Remark (i).

5. F-D dog-leg promoted to §3.1

"Repair of the right-horizontal estimate": the failed implication (e/2 > 1), the exact deformation H_low = H_high − V_right + V_left, the safe high-tail contraction (q = e^{4/9}/2 < 1), the precise Lagarias wording ("the geometric-decrease conclusion following (6.12) is not implied by the displayed bounds when T ≍ √n" — proof-gap framing, not theorem-false), and the open hidden-cancellation question (E-032) recorded but not relied on. The Step-2 footnote now carries only F-A/F-B/F-E and points at §3.1.

6. Appendix B additions

The verbatim signature, the instantiation list, and the review's dependency-chain display (partial fractions → S_f = Res₁ → rectangle identity → four side bounds → sfBoundProp → lambda_pos_finite_height_closed). Plus Section 2 compressed to one paragraph (certificate method; R(ψ) detail deferred to the companion note) and the revision date 2026-08-20 → 2026-08-26.

Verification + side effects

• pdflatex + bibtex cycle: compiles clean, 11 pp, zero undefined refs; both new bib entries (johansson2015, oesterle2000) resolve. One LaTeX issue hit and fixed (unicode ∀/ℕ/≤/ℝ in the verbatim block → tt-quote with math).
• cover-letter.md + referee-list.md Misguich mentions corrected to Johansson. draft.tex (FROZEN), paperB.tex, and the user's correspondence package untouched.

Commits

79c96f2 (Lean certificate reduction + audit) + 973edbb (paper revision

• archive closure) + 9d74895 (layout fixes, below).

7. Layout fixes (9d74895, user-reported out-of-bounds)

• Appendix B dependency chain: the left-to-right arrow display was overfull — now a centered top-to-bottom table with downward arrows (partial fractions ↓ S_f = Res₁ ↓ rectangle identity ↓ four side bounds ↓ sfBoundProp ↓ lambda_pos_finite_height_closed).
• §3 Step 2: the B(n) display was out of bounds — split at the relation (split environment).
• §3 Theorem: the N₁ line (full 25-digit integer) was out of bounds — the main line now carries only N₁ := (T₀−1)² ≈ 9.0×10²⁴ with the exact integer moved to a following inline clause.
• Knock-on overflows fixed: the verbatim signature's first line split (4.5pt) and the AI-statement declaration list given a forced break (75pt, long unbreakable \texttt names).
• Verified: compiles clean, 11 pp, zero undefined refs, ZERO overfull hboxes remaining.

Status at close

Paper A is at the revised state the review describes, with all layout issues resolved (zero overfull hboxes). NEXT: the user's read-through of the REVISED paperA.pdf + the submission decision (cover-letter.md + referee-list.md updated, target Experimental Mathematics).