{
  "file_path": "D:\\Python\\Quantum\\research\\journal\\session-042.md",
  "content": "# Session 042 (2026-08-26) \u2014 REVIEW REVISION: the user's Paper-A review fully actioned\n\n## Mission\nThe user returned a detailed expert review of the ii\u2032-7 Paper A (\"the\nrevised Paper A is dramatically stronger ... but I would not submit this\nexact PDF yet\") with six required fixes. Action all of them, with\nverification where the review flagged a factual vulnerability.\n\n## 1. THE CERTIFICATE RETRACTION (the review's top finding \u2014 REAL)\nThe review: Step 5's \"\u03bb_n > 0 to 5\u00d710\u2075 by Misguich\u2013Voros\" could not be\nallowed to carry the finite splice unless checked theorem-by-theorem,\nsince the cited reference is explicitly *Discretized* Keiper/Li.\nVerification performed (not assumed):\n- The bib entry is Voros alone, Exp. Math. 29(4):452\u2013469, 2020\n  (arXiv:1703.02844).\n- Fetched and read the paper (pypdf extraction of the full text):\n  Misguich computed the DEFORMED sequence {\u039b_n} (Voros's eq. 36), not\n  the ordinary \u03bb_n \u2014 and the source is \"G. Misguich, calculations ...\n  (private communications, 2017)\" [their ref. 25]. Doubly unsuitable:\n  wrong sequence AND not a checkable published source.\n- The same read surfaced the **sound replacement**: \"n = 10\u2075 attained by\n  Johansson [18, \u00a7 4.2]\" \u2014 F. Johansson, \"Rigorous high-precision\n  computation of the Hurwitz zeta function and its derivatives\", Numer.\n  Algor. 69 (2015) 253\u2013270 (arXiv:1309.2877). Verified in that paper's\n  \u00a7 4.2 (\"Computing the Keiper\u2013Li coefficients\"): the ORDINARY\n  coefficients \u03bb_0\u2026\u03bb_{100000} computed with rigorous interval-arithmetic\n  error bounds, all positive (\"shows agreement with Keiper's conjecture\n  (and the Riemann hypothesis)\"), \u03bb_100000 certified to ~2900 digits.\n- AND the novelty-relevant precursor: Oesterl\u00e9 [26, prop. 2] (typescript\n  2000, revised 2001, uncirculated, cited in Voros): RH-to-T\u2080 \u27f9\n  \u03bb_n \u2265 0 for n \u2264 T\u2080\u00b2 \u2014 the finite-height STATEMENT exists unpublished.\nAction: Lean perimeter `LiVerifiedUpTo` reduced (5\u00b710\u2075) \u2192 (10\u2075) (three\ntheorem sites + docstrings; the assembly's hfinite branch uses exactly\nn < 10\u2075, so nothing else changes; rebuild GREEN 8775 jobs; audit\nre-run: 29 decls, 3 standard axioms only). Paper Step 5 rewritten as\nthe declared certificate `LiVerifiedUpTo($10^5$)` with the honest\ntwo-leg evidence (Johansson to 10\u2075 + E-011/E-015 to 3000) and a\nfootnote recording the retraction. Archive: R-004, D-037 erratum\nADDENDUM, NGUYEN.md (3.2 + ii\u2032-7 + Ledger #6), STATE.md.\n\n## 2. Hypothesis count (user-caught arithmetic error)\n\"Eight named hypotheses\" was wrong: 2 computational + 5 analytic =\nSEVEN (the analytic list itself names five: ZeroCountProp,\nZeroCountProp2, ZeroCountGlobalProp, NoLowZeros, MZeroProp). Fixed\neverywhere; per the review's advice, Appendix B now carries the final\nLean signature copied verbatim (tt-quote form, unicode via math) and\nthe count is taken from the signature, not from memory.\n\n## 3. Theorem statement \u2194 trust boundary\nBoth Theorem environments now assume (i) RH verified to T\u2080\n(Platt\u2013Trudgian, interval arithmetic) and (ii) \u03bb_n > 0 for n \u2264 10\u2075\n(Step 5) \u2014 the abstract's \"conditional on RH verification and finite Li\ncomputations\" and the formal theorem's hypotheses now agree. Appendix B\ngains the instantiation list mapping each of the seven hypotheses to\nits cited source (Platt\u2013Trudgian also discharges NoLowZeros via the\nlowest zero at 14.134\u2026; Trudgian 2014 discharges the three counting\nProps; E-023 discharges MZeroProp).\n\n## 4. Novelty hedged\n\"first assembled explicit chain\" \u2192 \"we have found no previous explicit\nassembly\"; \"maximal content of the Li route short of RH\" \u2192 the narrow\nVoros form (eventual positivity of all large \u03bb_n \u27f9 RH, so no result\nshort of RH asserts an infinite positive tail). Oesterl\u00e9's unpublished\nprecursor (n \u2264 T\u2080\u00b2) explicitly noted with a new bib entry\n(oesterle2000); Lagarias 2007's published weaker window\n(n \u2264 T\u00b2/(4 log\u00b2 T)) already in Remark (i).\n\n## 5. F-D dog-leg promoted to \u00a73.1\n\"Repair of the right-horizontal estimate\": the failed implication\n(e/2 > 1), the exact deformation H_low = H_high \u2212 V_right + V_left, the\nsafe high-tail contraction (q = e^{4/9}/2 < 1), the precise Lagarias\nwording (\"the geometric-decrease conclusion following (6.12) is not\nimplied by the displayed bounds when T \u224d \u221an\" \u2014 proof-gap framing, not\ntheorem-false), and the open hidden-cancellation question (E-032)\nrecorded but not relied on. The Step-2 footnote now carries only\nF-A/F-B/F-E and points at \u00a73.1.\n\n## 6. Appendix B additions\nThe verbatim signature, the instantiation list, and the review's\ndependency-chain display (partial fractions \u2192 S_f = Res\u2081 \u2192 rectangle\nidentity \u2192 four side bounds \u2192 sfBoundProp \u2192\nlambda_pos_finite_height_closed). Plus Section 2 compressed to one\nparagraph (certificate method; R(\u03c8) detail deferred to the companion\nnote) and the revision date 2026-08-20 \u2192 2026-08-26.\n\n## Verification + side effects\n- pdflatex + bibtex cycle: compiles clean, **11 pp**, zero undefined\n  refs; both new bib entries (johansson2015, oesterle2000) resolve.\n  One LaTeX issue hit and fixed (unicode \u2200/\u2115/\u2264/\u211d in the verbatim block\n  \u2192 tt-quote with math).\n- cover-letter.md + referee-list.md Misguich mentions corrected to\n  Johansson. draft.tex (FROZEN), paperB.tex, and the user's\n  correspondence package untouched.\n\n## Commits\n79c96f2 (Lean certificate reduction + audit) + this one (paper revision\n+ archive closure).\n\n## Status at close\nPaper A is at the revised state the review describes. NEXT: the user's\nread-through of the REVISED paperA.pdf + the submission decision\n(cover-letter.md + referee-list.md updated, target Experimental\nMathematics).\n"
}