{
  "replace_all": false,
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDisc.lean",
  "old_string": "/-! ## 2. The center lower bound, the Jensen count, and the R-gap -/\n\n/-- The M\u00f6bius L-series is bounded by \u03b6(2) on re s \u2265 2: |1/\u03b6(s)| \u2264 \u03c0\u00b2/6. -/\ntheorem norm_inv_riemannZeta_le {s : \u2102} (hs : 2 \u2264 s.re) :\n    \u2016(riemannZeta s)\u207b\u00b9\u2016 \u2264 Real.pi ^ 2 / 6 := by\n  have hs1 : 1 < s.re := by linarith\n  have hprod : riemannZeta s * L \u2197ArithmeticFunction.moebius s = 1 := by\n    rw [\u2190 LSeries_zeta_eq_riemannZeta hs1]\n    exact LSeries_zeta_mul_Lseries_moebius hs1\n  have hsum : Summable fun n : \u2115 => \u2016((ArithmeticFunction.moebius n : \u2124) : \u2102) / (n : \u2102) ^ s\u2016 := by\n    have h2 : Summable fun n : \u2115 => (1 : \u211d) / (n : \u211d) ^ 2 := hasSum_zeta_two.summable\n    apply h2.of_norm_bounded (fun n => ?_)\n    rw [norm_div]\n    have h3 : \u2016((ArithmeticFunction.moebius n : \u2124) : \u2102)\u2016 \u2264 1 := by\n      rw [\u2190 Int.cast_abs]\n      apply Int.cast_le.mpr\n      exact ArithmeticFunction.abs_moebius_le_one... sorry\n    sorry\n  sorry\n\nend NguyenRH1\n\nend",
  "new_string": "/-! ## 2. The scaled function, the Jensen count, and the R-gap\n\nThe scaled function F(w) = \u03b6(s\u2080 + (5/2)w)/\u03b6(s\u2080) on the unit disc, to\nwhich Zeta23's `ZerosBound` (Jensen) applies: F(0) = 1 (the center lower\nbound \u2016\u03b6(2+it)\u2016 \u2265 1/3 is Zeta23's `RvM.zeta_lower_bound_two`), and\n\u2016F\u2016 \u2264 (9/4)|t|\u00b2 on the closed unit disc (ii\u2032-5b's disc bound). -/\n\n/-- The scaled function F(w) = \u03b6(s\u2080 + (5/2)\u00b7w)/\u03b6(s\u2080), s\u2080 = 2+it. -/\nnoncomputable def scaledZeta (t : \u211d) (w : \u2102) : \u2102 :=\n  riemannZeta (discCenter t + (5 / 2 : \u2102) * w) / riemannZeta (discCenter t)\n\ntheorem scaledZeta_zero (t : \u211d) : scaledZeta t 0 = 1 := by\n  unfold scaledZeta\n  simp only [mul_zero, add_zero]\n  exact div_self (by\n    have h := RvM.zeta_lower_bound_two t\n    intro h0\n    rw [h0, norm_zero] at h\n    norm_num at h)\n\n/-- F is analytic on the closed unit disc (\u03b6 is analytic on B(s\u2080, 5/2),\nwhich avoids the pole at 1 since |t| \u2265 10 \u27f9 |im| \u2265 15/2). -/\ntheorem scaledZeta_analytic {t : \u211d} (ht : 10 \u2264 |t|) :\n    AnalyticOnNhd \u2102 (scaledZeta t) (Metric.closedBall 0 1) := by\n  intro w hw\n  rw [Metric.mem_closedBall, dist_zero_right] at hw\n  have hw' : \u2016(5 / 2 : \u2102) * w\u2016 \u2264 5 / 2 := by\n    rw [norm_mul]\n    calc \u2016(5 / 2 : \u2102)\u2016 * \u2016w\u2016 \u2264 (5 / 2) * 1 := by\n          apply mul_le_mul _ hw (norm_nonneg _) (by norm_num)\n          \u00b7 rw [norm_div, norm_one]; norm_num\n      _ = 5 / 2 := by norm_num\n  have hmem : discCenter t + (5 / 2 : \u2102) * w \u2208 Metric.closedBall (discCenter t) (5 / 2) := by\n    rw [Metric.mem_closedBall, Complex.dist_eq]\n    rw [add_sub_cancel_left]\n    exact hw'\n  -- the point is not 1 (its imaginary part is \u2265 15/2 in absolute value)\n  have hne : discCenter t + (5 / 2 : \u2102) * w \u2260 1 := by\n    intro h\n    have him : (discCenter t + (5 / 2 : \u2102) * w).im = t + (5 / 2) * w.im := by\n      simp [discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im, mul_re]\n    have h1 : |(discCenter t + (5 / 2 : \u2102) * w - discCenter t).im| \u2264 5 / 2 := by\n      calc |(discCenter t + (5 / 2 : \u2102) * w - discCenter t).im|\n          \u2264 \u2016discCenter t + (5 / 2 : \u2102) * w - discCenter t\u2016 := abs_im_le_norm _\n        _ \u2264 5 / 2 := by rw [add_sub_cancel_left]; exact hw'\n    rw [show (discCenter t + (5 / 2 : \u2102) * w - discCenter t) = (5 / 2 : \u2102) * w by ring] at h1\n    rw [h] at him\n    simp at him  -- him : (1:\u2102).im = t + (5/2)*w.im; (1:\u2102).im = 0\n    -- |t + (5/2) w.im| \u2265 |t| \u2212 (5/2)|w.im| \u2265 10 \u2212 5/2 = 15/2 > 0\n    have hwim : |w.im| \u2264 1 := (abs_im_le_norm _).trans hw\n    have : |t + (5 / 2) * w.im| \u2265 15 / 2 := by\n      have h2 : |t + (5 / 2) * w.im| \u2265 |t| - |(5 / 2) * w.im| := by\n        have h3 : |t| \u2264 |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by\n          calc |t| = |(t + (5 / 2) * w.im) + (-(5 / 2) * w.im)| := by ring_nf\n            _ \u2264 |t + (5 / 2) * w.im| + |-(5 / 2) * w.im| := abs_add_le _ _\n            _ = |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by rw [abs_neg]\n        linarith [h3]\n      have h4 : |(5 / 2) * w.im| \u2264 5 / 2 := by\n        rw [abs_mul, abs_of_nonneg (by norm_num : (0:\u211d) \u2264 5/2)]\n        calc (5 / 2) * |w.im| \u2264 (5 / 2) * 1 := by\n              apply mul_le_mul_of_nonneg_left hwim (by norm_num)\n          _ = 5 / 2 := by norm_num\n      linarith [h2, h4, ht]\n    rw [him] at this\n    norm_num at this\n  -- \u03b6 analytic at the point\n  have h\u03b6 : AnalyticAt \u2102 riemannZeta (discCenter t + (5 / 2 : \u2102) * w) := by\n    have hd := differentiableAt_riemannZeta hne\n    -- DifferentiableAt at a point doesn't give AnalyticAt directly; use the\n    -- neighborhood differentiability on {z \u2260 1}.\n    have hU : {z : \u2102 | z \u2260 1} \u2208 \ud835\udcdd (discCenter t + (5 / 2 : \u2102) * w) :=\n      isOpen_compl_singleton.mem_nhds hne\n    exact ((HolomorphicOn_riemannZeta.mono (Set.subset_univ _) |>.analyticOnNhd\n      isOpen_compl_singleton) _ hU ... )\n  sorry\n\nend NguyenRH1\n\nend"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\paper\\paperA.tex",
  "oldString": "content of Step 2, in the dependency chain\n\\[\n\\text{partial fractions} \\;\\longrightarrow\\; S_f = \\operatorname{Res}_1\n\\;\\longrightarrow\\; \\text{rectangle identity} \\;\\longrightarrow\\;\n\\text{four side bounds} \\;\\longrightarrow\\;\n\\boxed{\\texttt{sfBoundProp}} \\;\\longrightarrow\\;\n\\boxed{\\texttt{lambda\\_pos\\_finite\\_height\\_closed}},\n\\]",
  "newString": "content of Step 2, in the dependency chain\n\\begin{center}\n\\begin{tabular}{c}\npartial fractions \\\\\n$\\downarrow$ \\\\\n$S_f = \\operatorname{Res}_1$ \\\\\n$\\downarrow$ \\\\\nrectangle identity \\\\\n$\\downarrow$ \\\\\nfour side bounds \\\\\n$\\downarrow$ \\\\\n\\boxed{\\texttt{sfBoundProp}} \\\\\n$\\downarrow$ \\\\\n\\boxed{\\texttt{lambda\\_pos\\_finite\\_height\\_closed}}\n\\end{tabular}\n\\end{center}",
  "originalFile": "% ============================================================\n% NGUYEN-RH-1 \u2014 PAPER A (split 2026-08-20, session 013, from draft.tex)\n% An explicit finite-height Li-positivity theorem, machine-verified.\n% Self-contained artifact per the session-012-end-notes review:\n% \u00a73.1 + Appendices A.1/B of the combined draft, retargeted.\n% The spectral-line material lives in paperB.tex (in preparation).\n% ============================================================\n\\documentclass[11pt]{article}\n\\usepackage{amsmath,amssymb,amsthm,mathtools}\n\\usepackage{microtype}\n\\usepackage[colorlinks=true,linkcolor=blue,citecolor=blue]{hyperref}\n\n% The prose is dense with unhyphenatable compounds (Li-positivity,\n% [proved, ...] tags). Give TeX room to spread the slack instead of\n% running past the right margin.\n\\emergencystretch=2em\n\n\\newtheorem{theorem}{Theorem}\n\\newtheorem{lemma}[theorem]{Lemma}\n\\newtheorem{corollary}[theorem]{Corollary}\n\\theoremstyle{definition}\n\\newtheorem{definition}[theorem]{Definition}\n\\theoremstyle{remark}\n\\newtheorem{remark}[theorem]{Remark}\n\n\\title{An explicit finite-height Li-positivity theorem\\\\\nwith a machine-verified assembly\\thanks{This work was produced with\nsubstantial machine assistance; see the AI Contribution Statement.}}\n\\author{Dan T Nguyen\\thanks{Research Ai}}\n\\date{Started: 2026-08-17; revised 2026-08-26}\n\n\\begin{document}\n\\maketitle\n\n\\begin{abstract}\n[proved, conditional on computation] The Keiper--Li coefficients of the\nRiemann $\\xi$-function satisfy $\\lambda_n > 0$ for all\n$1 \\le n \\le (T_0-1)^2 \\approx 9\\times10^{24}$, conditional on the\ninterval-arithmetic verification of RH to height $T_0 = 3\\times10^{12}$\n(Platt--Trudgian) and on finite Li-coefficient computations\n(Johansson's rigorous table to $10^5$ and this project's to $3000$),\nwith every constant traced. We have found no previous explicit assembly\nof this chain in the literature; by Voros's sharpening, positivity of\nall sufficiently large $\\lambda_n$ would itself imply RH, so no result\nshort of RH can assert an infinite positive tail. Moreover the full\nreduction is machine-verified in Lean~4 (package \\texttt{NguyenRH1}):\nthe theorem is proved from exactly seven named hypotheses --- the two\ncomputational certificates above and five declared analytic inputs\n(Trudgian's explicit zero-counting bounds in their unit-window,\ntwo-unit, and global forms, a Platt-class zero-location certificate,\nand one short-segment interval constant), with the traced contour bound\n$|S_f(n)| \\le B(n)$ on $10^5 \\le n \\le (T_0-1)^2$ itself machine-proved\nfrom those five --- with axiom profile exactly the three standard\naxioms (\\texttt{propext}, \\texttt{Classical.choice},\n\\texttt{Quot.sound}) and no \\texttt{sorry} anywhere in the\ndevelopment's Li chain.\n\\end{abstract}\n\n\\section{Introduction}\n\nThe Riemann hypothesis (RH) asserts that every nontrivial zero of\n$\\zeta(s)$ has real part $1/2$. The strongest unconditional density\nresult to date is the (machine-verified) theorem that at least $2/3$\nof the nontrivial zeros are simple and on the critical line, and at\nleast $5/6$ of the zeros in a given range are distinct\n\\cite{anthropic2026riemann}; the underlying certificate method has a\ndocumented bandwidth-one ceiling near $0.682$ of the zeros. Two\nclassical reformulations frame most modern attacks: \\emph{Weil\npositivity} --- positivity of the Weil quadratic form on all of\n$C_c^2(\\mathbb R)$ is equivalent to RH \\cite{weil1952fonctions,\nbombieri2000weil}, and the negative index of its truncations counts\noff-line zero pairs \\cite{bombieri2000weil} --- and \\emph{Li's\ncriterion} --- $\\lambda_n > 0$ for all $n$ is equivalent to RH\n\\cite{li1997, bombieri1999lagarias}, with Voros's sharpening that\npositivity of any tail $\\{\\lambda_n\\}_{n \\ge N_0}$ already implies RH\n\\cite{voros2006sharpenings}.\n\nThis paper reports one theorem-level outcome of a systematic research\nprogram on RH: an explicit finite-height Li-positivity theorem,\nassembled with every constant traced, and with its full reduction ---\nincluding the contour estimate --- machine-verified in Lean~4 modulo a\ndeclared perimeter (computational certificates and explicit\nzero-counting bounds). A companion note (in preparation)\ncovers the spectral-line results of the same program (an exact\nfactorization on Suzuki's operator line and a valley theorem for the\nassociated model spaces). Every claim carries an explicit correctness\ntag, and every numerical input is produced by a deterministic,\narchived script.\n\n\\begin{theorem}[R-004; conditional on computation]\n\\label{thm:finite-height-li-intro}\nAssume (i) the Riemann hypothesis verified to height\n$T_0 = 3\\times 10^{12}$ (Platt--Trudgian \\cite{platt2021riemann},\ninterval arithmetic), and (ii) $\\lambda_n > 0$ for all $n \\le 10^5$\n(finite computation; Section~3, Step~5). Then the Keiper--Li\ncoefficients satisfy\n$\\lambda_n > 0$ for all $1 \\le n \\le (T_0-1)^2 \\approx 9\\times10^{24}$.\n\\end{theorem}\n\nBy Voros's sharpening, eventual positivity of all sufficiently large\n$\\lambda_n$ would itself imply RH, so a result short of RH cannot\nassert an infinite positive tail; an explicit finite-height statement\nis the natural form of partial progress on this route. The statement\nhas an unpublished precursor (Oesterl\u00e9 \\cite{oesterle2000}, as cited in\n\\cite{voros2017li}: RH to height $T_0$ implies $\\lambda_n \\ge 0$ for\n$n \\le T_0^2$) and a published weaker form (Lagarias's window with a\n$\\log^2$ denominator, Remark~(i)); the explicit, fully constant-traced,\nmachine-verified assembly --- Lagarias's contour argument\n\\cite{lagarias2007li} with Trudgian's explicit zero-counting bounds\n\\cite{trudgian2014}, an elementary archimedean lower bound, a proved\nmargin convexity, and the finite verifications --- we have found\nnowhere else in the literature.\n\nSection~2 recalls the certificate-method background and the sanity\ngate. Section~3 states and proves the theorem. Section~4 collects the\nobstruction analysis delimiting the method. Appendix~A describes the\nnumerical machinery; Appendix~B the formal-verification status.\n\n\\section{Background: the Weil-form certificate method}\n\nWe recall, in one paragraph, the machinery behind the state-of-the-art\ndensity theorem \\cite{anthropic2026riemann} --- the launchpad of this\nproject and the sanity gate for everything below; details follow that\npaper, and a companion note (in preparation) covers this project's own\nwork on that line. The Weil explicit formula \\cite{weil1952fonctions}\nexpresses, for a bandwidth-one test function, a quadratic form on the\nzeros as a functional of the primes; compressing it via a Gabor frame\nat the critical density yields a finite matrix identity\n$\\tilde G = P + Q$, with the prime side computed unconditionally from\nMontgomery's second moment \\cite{montgomery1973pair}. A rank--trace\ninequality converts that input into a lower bound on the number of\nsimple on-line zeros in a window, whose strength is governed by a\nwindow ratio $R(\\psi)$: $2 - R(\\psi)$ certifies $0.6725$ of zeros\nsimple and on the line and $0.83625$ distinct, and a sharpness analysis\nlocates the bandwidth-one ceiling of the method at $\\approx 0.682$ with\nstructural obstructions beyond (Section~4). One feature of this\nmachinery matters here: the certificate fails, as it must, for the\nDavenport--Heilbronn and Epstein zeta functions (which violate the\nRH-analogue); the main theorem of this paper has been required to pass\nthis gate structurally (project file D-053).\n\n\\section{The finite-height Li theorem (R-004)}\n\nLet $\\lambda_n = \\sum_{\\rho}{}'\\,\\bigl[1-\\bigl(1-\\tfrac1\\rho\\bigr)^n\\bigr]$\nbe the Keiper--Li coefficients of the Riemann $\\xi$-function. Li's\ncriterion states $\\lambda_n > 0$ for all $n \\geq 1$ if and only if the\nRiemann hypothesis holds \\cite{li1997,bombieri1999lagarias}. Voros\n\\cite{voros2006sharpenings} showed that ``$\\lambda_n > 0$ for all\n$n \\geq N_0$'' is already equivalent to RH for any $N_0$, so no\npartial infinite-range statement exists; the maximal content of the Li\nroute short of RH is an \\emph{explicit finite-height} statement.\n\n\\begin{theorem}[R-004; conditional on computation]\n\\label{thm:finite-height-li}\nAssume (i) the Riemann hypothesis verified to height\n$T_0 = 3\\times 10^{12}$ (Platt--Trudgian \\cite{platt2021riemann},\ninterval arithmetic), and (ii) $\\lambda_n > 0$ for all $n \\le 10^5$\n(finite computation; Step~5). Then\n\\[\n\\lambda_n > 0 \\qquad \\text{for all } 1 \\le n \\le N_1 := (T_0-1)^2\n\\approx 9.0\\times 10^{24},\n\\]\nwith $N_1 = 8\\,999\\,999\\,999\\,994\\,000\\,000\\,000\\,001$ exactly.\n\\end{theorem}\n\n\\begin{proof}[Proof sketch (full assembly: D-037)]\nBombieri--Lagarias \\cite{bombieri1999lagarias} give\n$\\lambda_n = S_\\infty(n) - S_f(n) + 1$ with $S_\\infty$ the archimedean\nand $S_f$ the finite-place contribution.\n\n\\emph{Step 1 (archimedean lower bound).} From Lagarias's formula\n\\cite[(4.11)]{lagarias2007li},\n$S_\\infty(n) = \\sum_{j=1}^n (-1)^j \\binom{n}{j} a_j$ with\n$a_1 = (\\log 4\\pi + \\gamma)/2$ and $a_j = (1-2^{-j})\\zeta(j)\n= \\sum_{m \\text{ odd}} m^{-j}$ ($j \\ge 2$), the $j$-sum is a finite\ndifference and one obtains the \\emph{exact} identity\n$S_\\infty(n) = (1-a_1)n - 1 + \\sum_{m \\ge 3,\\, m \\text{ odd}}\n\\bigl[(1-\\tfrac1m)^n - 1 + \\tfrac{n}{m}\\bigr]$.\nBernoulli's inequality and the explicit harmonic bounds\n$\\log M + \\gamma + \\tfrac{1}{2M} - \\tfrac{1}{12M^2} \\le H_M \\le\n\\log M + \\gamma + \\tfrac{1}{2M}$ give, for $n \\ge 20$,\n\\[\nS_\\infty(n) \\;\\ge\\; \\tfrac12 n\\log n + (C_1 - \\tfrac{\\gamma}{2})\\,n - 4,\n\\qquad C_1 = \\tfrac{\\gamma - 1 - \\log 2\\pi}{2}.\n\\]\n(Machine-validated against exact values for $20 \\le n \\le 5000$.)\n\n\\emph{Step 2 (finite-part upper bound).} Tracing Lagarias's contour\nargument \\cite[Thm~6.1]{lagarias2007li} with explicit constants\n(Trudgian's $N(T)$ and $S(T)$ bounds \\cite{trudgian2014}, partial\nfractions for $\\zeta'/\\zeta$ with the reference-point estimate\n$|R(s)| \\le 10.5\\log(|t|{+}2) + 48$ for $-5/2 \\le \\sigma \\le 3$,\n$|t| \\ge 10$ (D-056), kernel bounds $e^4+1$, a measured\nshort-segment constant $M_0 = 1.3352$) gives\n$|S_f(n)| \\le B(n)$ with\n\\[\n\\begin{split}\nB(n) =\\;& 4F(T) + 4T\\bigl[\\tfrac23 Z_2(T) + 10.5\\log(T{+}2) + 48\\bigr] \\\\\n& + 40M_0 + 2(e^4{+}1)\\,7H(T) + 2\\,\\mathrm{DL}(n) + I_{\\mathrm{Maj}}(n) + 1,\n\\end{split}\n\\]\n$T = \\sqrt n + 1$, $F$ the honest zero-count majorant (the formal\ndevelopment's mildly enlarged Trudgian shape), $Z_2(t)$ the explicit\ntwo-unit-interval zero count (including the $\\log\\log$ term),\n$H(T) = 3C_0(T)^2 + 10.5\\log(T{+}2) + 48$ with $C_0$ the unit-interval\ncount, $\\mathrm{DL}(n) = \\tfrac{\\sqrt n+1}{4}(e^{5/2}+1) + 8.38 +\n\\tfrac14 I_{\\mathrm{Maj}}(n)$ the zero-free dog-leg charge for the\nright tail, $I_{\\mathrm{Maj}}(n) = 2(\\sqrt n+1)(e^{\\sqrt n/2}+1)\\cdot\n0.57\\cdot 2^{-(2\\sqrt n-2)}$ the right-vertical majorant, and the\nfinal $1$ the trivial-zero contribution.\\footnote{\\emph{Correction\nnote} (D-071 with E-034): three further adjustments to this $B(n)$\naccount were made during the machine closure of Step 2, and the\ndisplayed formula is the corrected one; the theorem statement is\nunaffected. (i) The bridge is $4F$, not $2N$: the residue sum runs\nover both signs of $\\gamma$ (a factor-2 accounting slip in the first\ntracing). (ii) The left-vertical near-sum charges the two-unit count\n$Z_2$ (its window $|\\gamma - T| \\le 1$ spans two unit intervals), not\nthe unit-interval $C_0$. (iii) The right-vertical kernel is charged\nhonestly as $e^{1/3} I_{\\mathrm{Maj}}(n)$ (the uniform bound is\n$e^{\\sqrt n/2+1/3}+1$), the factor $e^{1/3} \\le 1.4$ being absorbed by\nthe $2\\pi$ normalization of the residue theorem. The fourth and most\nsubstantive correction --- the repair of the right-horizontal estimate\n--- is Section~\\ref{subsec:dogleg}. All are machine-verified in\n\\texttt{NguyenRH1}.}\n\n\\emph{Step 3 (bridge).} For $n \\le (T_0-1)^2$ every zero with\n$|\\gamma| \\le \\sqrt n + 1$ is on the line, so\n$|1-(1-1/\\rho)^n| \\le 2$ per zero and\n$|\\lambda_n(T)| \\le 4F(T)$ (the residue sum runs over both signs of\n$\\gamma$); all other contour terms are \\emph{unconditional}.\n\n\\emph{Step 4 (margin).}\n$\\mathrm{margin}(n) := \\tfrac12 n\\log n + (C_1 - \\gamma/2)n - 4 - B(n) + 1$\nis convex for $n \\ge 20$ (proved: chain-rule reduction to eleven\none-variable sign conditions, each discharged elementarily \u2014 D-057),\nand $\\mathrm{margin}(8\\times 10^4) = 15\\,764 > 0$ with\n$\\mathrm{margin}(10^5) > \\mathrm{margin}(8\\times 10^4)$; by convexity\n(secant slopes increase) hence\n$\\mathrm{margin}(n) > 0$ for all $n \\in [10^5, N_1]$\\footnote{The\nmargin value at $8\\times10^4$ has a documented trail: $16\\,020$ with\nthe Trudgian $F + S_b$ zero-count majorant (E-028); $15\\,764$ with the\nmildly enlarged majorant consumed by the machine verification --- a\nnegative-weight term of $F + S_b$ dropped so that every convexity\nblock has provably negative $\\psi$ (the true majorant's $\\psi$ crosses\nzero near $T \\approx 16$), at a traced cost of $\\approx 0.9\\sqrt n$,\ni.e.\\ $256$ of the $16\\,020$; and $\\ge 8\\,001$ as the certified\nrational interval lower bound that the machine discharge actually\nconsumes (\\texttt{NguyenRH1},\n\\texttt{marginTilde\\_FAlt\\_80000\\_pos}).}\n(also computed to $n = 4\\times10^5$ on a unit grid and to $N_1$ on a\nlogarithmic grid; $\\mathrm{margin}(N_1) = 2.458\\times 10^{26}$).\n\n\\emph{Step 5 (finite verification; the declared certificate\n\\texttt{LiVerifiedUpTo($10^5$)}).} The base range $n < 10^5$ is covered\nby rigorous high-precision computation of the ordinary Keiper--Li\ncoefficients: for all $n \\le 10^5$ by Johansson \\cite{johansson2015}\n(interval-arithmetic error bounds throughout; the full table\n$\\lambda_0, \\dots, \\lambda_{100000}$ all positive, matching the\nRH-true asymptotic, with $\\lambda_{100000} = 4.6258\\ldots$ certified\nto $\\sim 2900$ digits), and independently for all $n \\le 3000$ by this\nproject (two methods --- the arithmetic side via Bombieri--Lagarias\nThm~2 and the zero side --- agreeing to $4.8\\times10^{-25}$ relative,\nand $\\lambda_1$ agreeing with its closed form to better than $10^{-28}$\nrelative). The crossover $N_0 = 8\\times 10^4$ is covered by a factor\n$1.25$.\\footnote{An earlier draft cited Voros's discretized Keiper--Li\ncomputations \\cite{voros2017li} (with Misguich) for this range; those\nconcern a \\emph{deformed} sequence $\\Lambda_n$, not the ordinary\n$\\lambda_n$, and the citation has been replaced by Johansson's rigorous\nordinary-$\\lambda_n$ table.}\n\\end{proof}\n\n\\subsection{Repair of the right-horizontal estimate}\n\\label{subsec:dogleg}\n\nThe geometric-decrease conclusion following\n\\cite[(6.12)]{lagarias2007li} is not implied by the displayed bounds\nwhen $T \\asymp \\sqrt n$: the per-step majorant ratio there is $e/2 > 1$\n(the zeta factor halves per unit step while the kernel ratio is $\\le e$),\nso the right-tail envelope grows like $e^{0.066\\sqrt n}$ rather than\ndecreasing ($\\sim 6\\times 10^{10}$ at $n = 10^5$ measured; E-031). In\nthe zeta specialization we replace this step by the following zero-free\ncontour deformation (D-073/D-074).\n\nKeep the cut height $T = \\sqrt n$ (so the bridge and the endpoint\n$N_1 = (T_0-1)^2$ are untouched) and deform only the right horizontal\nsegment $[3, 2\\sqrt n]$ at height $T$ into a \\emph{dog-leg}: lift\nvertically from $3 + iT$ to $3 + iU$ with $U = \\tfrac32 \\sqrt n$ (the\nleft vertical), traverse horizontally at height $U$ (the high\nsegment), and drop back at $2\\sqrt n$ (the right vertical). The\nrectangle this traverses lies entirely in $\\Re w \\ge 3$, where $\\zeta$\nis zero-free and pole-free \\emph{unconditionally}, so Cauchy's theorem\ngives the exact identity\n\\[\nH_{\\mathrm{low}} \\;=\\; H_{\\mathrm{high}} - V_{\\mathrm{right}} +\n  V_{\\mathrm{left}}\n\\]\n(\\texttt{upper\\_right\\_horizontal\\_eq\\_dogleg} in the formal\ndevelopment). Each dog-leg piece has an honest bound: the left vertical\ncontributes $\\le \\tfrac{\\sqrt n}{2}(e^{5/2}+1)\\cdot\\tfrac12$; the high\nsegment contracts geometrically (the repaired stepping ratio\n$q = e^{4/9}/2 < 1$, certified) and contributes $\\le 8.38$; and the\nright vertical is exponentially small, $\\le \\tfrac14 I_{\\mathrm{Maj}}(n)$.\nThe charge replacing the broken ``$3.3$'' is therefore\n$\\mathrm{DL}(n) = \\tfrac{\\sqrt n + 1}{4}(e^{5/2}+1) + 8.38 +\n\\tfrac14 I_{\\mathrm{Maj}}(n)$ per side, with the margin essentially\nunchanged (margins $13\\,160$ / $88\\,911$ / $2.458\\times10^{26}$ at\n$8\\times10^4$ / $10^5$ / $N_1$). We record for completeness that the\nper-side bound at $T = \\sqrt n$ appears to hold empirically by a strong\nhidden cancellation (E-032: true-integral to envelope ratio down to\n$5.6\\times10^{-10}$); whether that cancellation admits a proof is an\nopen question we do not rely on.\n\n\\begin{remark}\n(i) Using Lagarias's printed bridge window $n \\le T^2/(4\\log^2 T)$\ninstead of the traced proof gives the conservative\n$N_1^* = 2.73\\times 10^{21}$; the theorem is robust either way.\n(ii) The traced worst-case bound $|S_f|$ is $\\sim 170\\times$ loose\nagainst the measured curve ($|S_f| \\le 13.52$ for $n \\le 5000$); the\nslack is structural to contour constants, not a gap.\n(iii) The dependence on computation is explicit and checkable:\nPlatt--Trudgian's interval-arithmetic verification of RH\n\\cite{platt2021riemann} and Johansson's rigorous ordinary-$\\lambda_n$\ntable \\cite{johansson2015}, supplemented by this project's independent\nverification to $n \\le 3000$ (E-011/E-015).\n\\end{remark}\n\n\\section{Obstruction analysis}\n% Documented dead ends from research/graveyard/ where they\n% delimit the method (contributes to success criterion 4).\n\nThe following routes are closed with documented obstructions\n(full files in the project archive: graveyard G-001--G-003;\nderivations D-009--D-031):\n\\begin{itemize}\n\\item \\emph{Certificate extension past $2/3$ in the bandwidth-one\nframework} (Track A): a six-wall map (D-013) shows $>2/3$ is\nimpossible within the current data class; the window-class optimum is\nsaturated in both the $\\xi$ and $\\xi'$ worlds (D-009, D-030), and\nmoment-ladder certificates cap below $2/3$ at every order (G-002).\n\\item \\emph{Multiple-zero bounds as chain input} (G-001): the\n$s_2/p$ substitution symmetry makes depth$\\to$0 off-line pairs\nindistinguishable from double zeros in all two-moment data.\n\\item \\emph{Density theorems $\\to$ de~Bruijn--Newman $\\Lambda$}\n(G-003): one-sided information \u2014 density theorems lower-bound the\non-line fraction while $\\Lambda$ requires an upper bound on the\ncomplex fraction.\n\\item \\emph{$\\xi^{(k)}$-certificate routes} (T4/T4b, D-022, D-031):\nthe strength mechanism (a perfect-square node in the diagonal law)\ndoes not transfer to $\\xi$, and the $s_2/p$ symmetry caps every\nderivative class below $100\\%$.\n\\end{itemize}\n\n\\appendix\n\\section{Numerical experiments}\n% Tables/figures generated from research/numerics/data/ CSVs.\n\nAll experiments are deterministic scripts with CSV+JSON sidecars in the\nproject archive (\\texttt{research/numerics/}); checks as stated.\n\n\\subsection{Li-coefficient machinery (E-011/E-015/E-021/E-023)}\n\\begin{itemize}\n\\item $\\lambda_n > 0$ verified for $n \\le 3000$ from the arithmetic\nside (Bombieri--Lagarias Thm~2, zero-free; \\textsc{flint} Stieltjes +\nArb $\\zeta$, 1000--1450-digit working precision), cross-validated\nagainst the zero-side computation (agreement $4.8\\times10^{-25}$\nrelative) and $\\lambda_1$ agreeing with its closed form to better\nthan $10^{-28}$ relative.\n\\item Exact archimedean part: $S_\\infty(n) = \\tfrac12 n\\log n + C_1 n\n- \\tfrac14 - \\tfrac{1}{24n} + o(1/n)$ measured to $n = 5000$\n($c_0 = -1/4$ identified exactly; residuals match $-1/4 - 1/(24n)$ to\nall printed digits), and $|S_f(n)| \\le 13.52$ for $n \\le 5000$\n(max at $n = 3298$) vs the traced worst-case $\\sim 2280$ there \u2014\nthe contour constants are $\\sim 170\\times$ loose, as documented.\n\\item Margin assembly (E-028, fully traced constants $A = 10.5$,\n$B_0 = 48$): crossover at $n = 75\\,451$; adopted $N_0 = 8\\times10^4$\nwith margin $16\\,020$ and positive derivative ($15\\,764$ with the\nformal development's majorant --- Step-4 footnote); convexity proved\n(D-057) and grid-confirmed to $N_1 \\approx 9\\times10^{24}$;\n$\\mathrm{margin}(N_1) = 2.458\\times10^{26}$. (First-estimate\nconstants $2/2$: crossover $32\\,871$; measured $0.9/1.0$: $30\\,217$.)\n\\end{itemize}\n\n\\section{Formal verification}\n\nThe inherited density theorem \\cite{anthropic2026riemann} is formally\nverified in Lean~4 (repository \\texttt{zeta-23-lean}, tag v1.0); this\nproject performed a full \\texttt{lake} rebuild (9010 jobs) and a live\n\\texttt{\\#print axioms} audit of all comparator statements, confirming\nthe published axiom profile verbatim: no axioms beyond \\texttt{propext},\n\\texttt{Classical.choice}, and \\texttt{Quot.sound}, with \\texttt{sorry}\noccurring only in the trusted challenge-statement stubs.\n\nThe new result of this paper is formalized in the companion\npackage \\texttt{NguyenRH1} (same toolchain, path-linked to the vendored\n\\texttt{zeta-23-lean} and its \\textsc{Mathlib} build; no new axioms are\nintroduced anywhere). The first tier is complete: the archimedean lower\nbound for $S_\\infty(n)$ and the margin convexity are machine-proved\n(\\texttt{sInfty\\_lower\\_bound}, \\texttt{marginTilde\\_convex}, and the\nchain-rule identity \\texttt{chain\\_rule\\_sqrt\\_shift}), each with axiom\nprofile exactly the three standard axioms above. A design note on the\nconvexity proof: the pen-and-paper argument uses eleven one-variable\nsign conditions, but the Lean development proves an eight-block\n$\\psi$-table plus a separate analytic bound for the $I_I$ term\n($\\widetilde B_4$); the divergence from the eleven-row table is that\n$\\widetilde B_4$ is not concave, so it is excluded from the $\\psi$\nmachinery and bounded directly. That direct bound is itself a worked\nexample of this project's measured-to-traced conversion: the grid\ncheck of E-029 (maximum $2n\\,|\\widetilde B_4''(n)| = 0.189$ on\n$[20, 10^4]$, with the decay argument covering the tail) is superseded\nby a fully analytic factor-monotonicity proof of the sufficient\ninequality $\\widetilde\\psi''(s) - \\widetilde\\psi'(s)/s \\le 1.316 < 2$\nfor $s \\ge \\sqrt{20}$, i.e.\\ $\\widetilde B_4''(n) < 1/(2n)$ for all\n$n \\ge 20$ (\\texttt{iimaj\\_bracket\\_bound},\n\\texttt{IIMaj\\_deriv2\\_lt}).\n\nThe second tier is complete; the named analytic hypothesis is\ndischarged. The traced contour bound $|S_f(n)| \\le B(n)$ of Section~3\n(\\texttt{SfBoundProp}) is machine-proved (tier ii$'$), so the closed\nheadline theorem is machine-proved from exactly seven named hypotheses.\nIts final signature, copied verbatim from the development\n(\\texttt{LiClosed.lean}), is\n\\begin{quote}\\ttfamily\\upshape\\small\ntheorem lambda\\_pos\\_finite\\_height\\_closed\\\\\n\\hspace*{2em}(hRH : RHUpTo (3 * 10 \\^{} 12)) (hfinite : LiVerifiedUpTo (10 \\^{} 5))\\\\\n\\hspace*{2em}(hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\\\\\n\\hspace*{2em}(hZCG : ZeroCountGlobalProp) (hNLZ : NoLowZeros)\\\\\n\\hspace*{2em}(hMZ : MZeroProp) :\\\\\n\\hspace*{2em}$\\forall$ n : $\\mathbb{N}$, 1 $\\leq$ n $\\to$ (n : $\\mathbb{R}$) $\\leq$ (3 * 10 \\^{} 12 $-$ 1) \\^{} 2 $\\to$\\\\\n\\hspace*{2em}0 $<$ (liCoeff n).re\n\\end{quote}\nThe seven hypotheses instantiate from cited results and certificates as\nfollows. \\texttt{RHUpTo} comes from the Platt--Trudgian\ninterval-arithmetic verification of RH to height $3\\times10^{12}$\n\\cite{platt2021riemann}, which also gives the zero-location certificate\n\\texttt{NoLowZeros} (every nontrivial zero has $|\\gamma| \\ge 14$, the\nlowest lying at $14.134\\ldots$). \\texttt{LiVerifiedUpTo} comes from\nJohansson's rigorous ordinary-$\\lambda_n$ table to $10^5$\n\\cite{johansson2015} together with this project's independent\nverification to $3000$ (Appendix~A). \\texttt{ZeroCountProp},\n\\texttt{ZeroCountProp2}, and \\texttt{ZeroCountGlobalProp} are the\nunit-window, two-unit, and global specializations of Trudgian's\nexplicit zero-counting bounds \\cite{trudgian2014}.\n\\texttt{MZeroProp} is the short-segment constant $M_0 = 1.3352$, an\ninterval-arithmetic certificate (E-023: grid evaluation with a\nsampled-Lipschitz margin of safety $\\times 2$) in the same trust class.\n\nThe proof of \\texttt{SfBoundProp} contains the full complex-analytic\ncontent of Step 2, in the dependency chain\n\\[\n\\text{partial fractions} \\;\\longrightarrow\\; S_f = \\operatorname{Res}_1\n\\;\\longrightarrow\\; \\text{rectangle identity} \\;\\longrightarrow\\;\n\\text{four side bounds} \\;\\longrightarrow\\;\n\\boxed{\\texttt{sfBoundProp}} \\;\\longrightarrow\\;\n\\boxed{\\texttt{lambda\\_pos\\_finite\\_height\\_closed}},\n\\]\nwith named capstones \\texttt{rectInt'\\_Jlag} (meromorphic residue\nmachinery on rectangles), \\texttt{partialFraction\\_identity} (the\npartial-fraction identity for $\\zeta'/\\zeta$),\n\\texttt{logDeriv\\_riemannZeta\\_sub\\_nearZeros\\_le\\_tight} (the\nreference-point bound $|R(s)| \\le 10.5\\log(|t|{+}2) + 48$),\n\\texttt{sf\\_eq\\_resW1} (the exact identity\n$S_f(n) = \\mathrm{Res}_1(n)$),\n\\texttt{upper\\_right\\_horizontal\\_eq\\_dogleg} and the\n\\texttt{LiDogLeg} bounds (Section~\\ref{subsec:dogleg}),\n\\texttt{LiSideBounds} (the four side bounds), and the fold\n\\texttt{sfBoundProp}. The two elementary evaluations of the explicit\nmargin function that the assembly consumes\n($\\mathrm{margin}(8{\\cdot}10^4) > 0$ and\n$\\mathrm{margin}(10^5) > \\mathrm{margin}(8{\\cdot}10^4)$) are discharged\nin the development itself, by certified rational interval bounds on\n$\\log$, $\\exp$, and $\\sqrt{\\cdot}$ (\\texttt{LiBasePoints.lean}). The\nmargin majorant in the development is a mildly enlarged Trudgian-shape\nfunction (a negative-weight term dropped, at a cost of $\\approx\n0.9\\sqrt n$ in the bound) chosen so that every convexity block has\nprovably negative $\\psi$; the axiom profile is unchanged --- the three\nstandard axioms, no \\texttt{sorryAx}, audited declaration-by-declaration\non the full chain.\n\nThe finite-height Li theorem remains, by design, \\emph{conditional} on\ncomputations (Platt--Trudgian's interval arithmetic; the\nLi-coefficient verifications); the five analytic inputs are explicit\npublished bounds of the same literature class \\cite{trudgian2014,\nplatt2021riemann}. The formal reduction leaves exactly those as\ntrusted inputs, which we regard as the honest formal target: every\nother step of the proof is machine-checked.\n\n\\section*{AI Contribution Statement}\nThis research was conducted with substantial assistance from two AI\nsystems: Kimi K3 (Moonshot AI), operated through the Claude Code\nharness (Anthropic), over an archived series of research sessions\n(project ledger: sessions 001--041). Machine contributions included:\nderivation drafting and constant-tracing (D-036/D-037/D-056/D-057),\nthe Lean~4 formalization of the Li chain (package \\texttt{NguyenRH1}:\n\\texttt{sInfty\\_lower\\_bound}, \\texttt{marginTilde\\_convex},\n\\texttt{lambda\\_pos\\_finite\\_height\\_verified},\n\\texttt{sfBoundProp}, \\texttt{lambda\\_pos\\_finite\\_height\\_closed}),\nthe numerical experiment suite (E-001--E-034), and adversarial\nself-audit (D-060: four independent audit instances, $\\sim$55 claims\nchecked, 10 corrections filed; D-071/D-072/D-074: four further\n$B(n)$-account corrections found and repaired during the machine\nclosure). All research direction, verification decisions,\nperimeter declarations, and final approval are the responsibility of\nthe human author, who serves as guarantor of the work. All\nmachine-produced mathematics was validated by machine-checked proof\n(Lean~4, axiom profiles as stated in Appendix~B), by cross-validated\ndeterministic computation, or is explicitly tagged otherwise in the\ntext. Session logs and audit trails are preserved in the project\narchive.\n\n\\section*{Acknowledgments}\nThe author thanks Moonshot AI (Kimi K3) and Anthropic (the Claude Code\nharness) for making their systems available for research use. The\nsubstantive record of machine assistance is the AI Contribution\nStatement above.\n\n\\bibliographystyle{plain}\n\\bibliography{references}\n\\end{document}\n",
  "structuredPatch": [
    {
      "oldStart": 446,
      "oldLines": 13,
      "newStart": 446,
      "newLines": 21,
      "lines": [
        " ",
        " The proof of \\texttt{SfBoundProp} contains the full complex-analytic",
        " content of Step 2, in the dependency chain",
        "-\\[",
        "-\\text{partial fractions} \\;\\longrightarrow\\; S_f = \\operatorname{Res}_1",
        "-\\;\\longrightarrow\\; \\text{rectangle identity} \\;\\longrightarrow\\;",
        "-\\text{four side bounds} \\;\\longrightarrow\\;",
        "-\\boxed{\\texttt{sfBoundProp}} \\;\\longrightarrow\\;",
        "-\\boxed{\\texttt{lambda\\_pos\\_finite\\_height\\_closed}},",
        "-\\]",
        "+\\begin{center}",
        "+\\begin{tabular}{c}",
        "+partial fractions \\\\",
        "+$\\downarrow$ \\\\",
        "+$S_f = \\operatorname{Res}_1$ \\\\",
        "+$\\downarrow$ \\\\",
        "+rectangle identity \\\\",
        "+$\\downarrow$ \\\\",
        "+four side bounds \\\\",
        "+$\\downarrow$ \\\\",
        "+\\boxed{\\texttt{sfBoundProp}} \\\\",
        "+$\\downarrow$ \\\\",
        "+\\boxed{\\texttt{lambda\\_pos\\_finite\\_height\\_closed}}",
        "+\\end{tabular}",
        "+\\end{center}",
        " with named capstones \\texttt{rectInt'\\_Jlag} (meromorphic residue",
        " machinery on rectangles), \\texttt{partialFraction\\_identity} (the",
        " partial-fraction identity for $\\zeta'/\\zeta$),"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}