{
  "replace_all": false,
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-003-finite-Gtilde.py",
  "old_string": "    U = pad * L  # total padded window\n    full = np.zeros(pad * M)\n    full[: M // 2] = phi[M // 2:]          # u in [0, L/2)\n    full[-M // 2:] = phi[: M // 2]         # u in [\u2212L/2, 0)\n    F = np.fft.fft(full) * du              # \u03d5\u0302 at \u03be_m = 2\u03c0m/U (phase: u\u2080=\u2212L/2 handled by shift)\n    # correct phase: our samples start at u = \u2212L/2 \u27f9 multiply by e^{+i\u03be L/2}... but\n    # we placed phi at DFT positions for u\u2208[0,U); u=\u2212L/2..0 mapped to end.\n    # With the placement above, F[m] \u2248 \u03d5\u0302(\u03be_m) directly (periodic extension).\n    m = np.arange(pad * M)\n    xi = 2 * np.pi * m / U\n    xi_signed = np.where(xi <= np.pi * pad * M / U * 0 + np.pi * M * pad / U / 2,\n                         xi, xi - 2 * np.pi * pad * M / U * 1.0)\n    # simpler: signed frequencies\n    xi_signed = 2 * np.pi * np.fft.fftfreq(pad * M, d=du)\n    order = np.argsort(xi_signed)\n    spline = CubicSpline(xi_signed[order], F[order])\n    return spline, a",
  "new_string": "    # Zero-pad to pad*M samples, rotating so index 0 \u2194 u=0 (DFT convention);\n    # then FFT[m]\u00b7du = \u03d5\u0302(\u03be_m) directly on the signed grid fftfreq.\n    full = np.zeros(pad * M)\n    full[: M // 2] = phi[M // 2:]          # u in [0, L/2)\n    full[-M // 2:] = phi[: M // 2]         # u in [\u2212L/2, 0)\n    F = np.fft.fft(full) * du\n    xi_signed = 2 * np.pi * np.fft.fftfreq(pad * M, d=du)\n    order = np.argsort(xi_signed)\n    spline = CubicSpline(xi_signed[order], F[order])\n    return spline, a"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\paper\\paperA.tex",
  "oldString": "\\cite{lagarias2007li} with Rosser's explicit $S(T)$ bound\n\\cite{rosser1941}, an elementary archimedean lower bound, a proved\nmargin convexity, the dog-leg repair of Section~\\ref{subsec:dogleg},",
  "newString": "\\cite{lagarias2007li} with Rosser's explicit Riemann--von Mangoldt\nerror bound \\cite[Thm~19]{rosser1941}, an elementary archimedean\nlower bound, a proved\nmargin convexity, the dog-leg repair of Section~\\ref{subsec:dogleg},",
  "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{Independent researcher}}\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 explicit perimeter inputs,\nitemized with provenance in Appendix~B --- three explicit\nzero-counting bounds derived from Rosser's Riemann--von Mangoldt\nerror bound and four\ncomputational certificates\n(the Platt--Trudgian RH verification, Johansson's rigorous Li table,\na zero-location certificate for the low zeros, and one short-segment\ninterval 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 six of the seven (all but the Li table), and with axiom profile\nexactly 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: Voros \\cite{voros2017li} reports an\nunpublished result of Oesterl\u00e9 \\cite{oesterle2000} that RH to height\n$T_0$ implies $\\lambda_n \\ge 0$ for $n \\le T_0^2$ (the typescript is\nuncirculated; we rely on Voros's citation and have not independently\nverified it). A published weaker form is Lagarias's window with a\n$\\log^2$ denominator (Remark~(i)). The novelty claimed here is not the\n$T^2$ scale itself but the explicit, fully constant-traced,\n\\emph{strict}-positivity assembly --- Lagarias's contour argument\n\\cite{lagarias2007li} with Rosser's explicit $S(T)$ bound\n\\cite{rosser1941}, an elementary archimedean lower bound, a proved\nmargin convexity, the dog-leg repair of Section~\\ref{subsec:dogleg},\nand the finite verifications --- and its machine verification; that\nassembly we have found nowhere 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$: eventual\npositivity of all sufficiently large $\\lambda_n$ would itself imply RH,\nso a result short of RH cannot assert an infinite positive tail. The\nnatural partial statement on this route is an \\emph{explicit\nfinite-height} one.\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\nThe two assumptions displayed are the two computational certificates.\nThe formal theorem consumes five further explicit perimeter inputs ---\nzero-counting bounds, a zero-location certificate, and one interval\nconstant --- which are established published results or stand-alone\ncertificates, instantiated with provenance in Appendix~B; they enter as\nhypotheses of the Lean reduction, not as additional conjectural\nassumptions.\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(the Riemann--von Mangoldt formula $N(T) = F(T) + S(T)$ with Rosser's\nexplicit bound $|S(T)| \\le 0.137\\log T + 0.443\\log\\log T + 1.588$,\n$T \\ge 1467$ \\cite{rosser1941}, and the finite-range verifications\n$|S(T)| \\le 1$ for $T \\le 280$ and $|S(T)| \\le 2$ for\n$T \\le 6.8\\times10^6$ \\cite[Eq.~(1.2)]{trudgian2014ii}, 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_n) + 4T_n\\bigl[\\tfrac23 Z_2(T_n) + 10.5\\log(T_n{+}2) + 48\\bigr] \\\\\n& + 40M_0 + 2(e^4{+}1)\\,7H(T_n) + 2\\,\\mathrm{DL}(n) + I_{\\mathrm{Maj}}(n) + 1.\n\\end{split}\n\\]\nHere $T_n := \\sqrt n + 1$ is a deterministic majorant height: the\ncontour itself runs at a zero-avoiding height $\\tau_n \\in [\\sqrt n,\n\\sqrt n + 1]$, chosen by a pigeonhole on the unit-window zero count\nwith ordinate clearance $\\ge 1/(9C_0(\\sqrt n + 2))$\n(\\texttt{exists\\_zero\\_avoiding\\_T\\_wide}), and every majorant, being\nnondecreasing in the height, is evaluated at $T_n$. Further, $F$ is the\nhonest zero-count majorant (the formal\ndevelopment's mildly enlarged $F + S_b$ 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$ we have\n$\\tau_n \\le \\sqrt n + 1 \\le T_0$, so by assumption~(i) every zero with\n$|\\gamma| \\le \\tau_n$ is on the line; hence\n$|1-(1-1/\\rho)^n| \\le 2$ per zero and\n$|\\lambda_n(\\tau_n)| \\le 4F(T_n)$ (the residue sum runs over both signs\nof $\\gamma$, the count majorized at $T_n$); all other contour terms are\n\\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) = 13\\,160 > 0$ with\n$\\mathrm{margin}(10^5) = 88\\,911 > \\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 $F + S_b$ zero-count majorant (E-028); $15\\,764$ with the\nmildly enlarged majorant --- 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$;\n$14\\,682$ after the honest-$B(n)$ corrections (i)--(ii) of the Step-2\nfootnote (the $4F$ bridge and the two-unit count $Z_2$); and\n$13\\,160$ after the dog-leg repair of Section~\\ref{subsec:dogleg}\n(E-034). The machine discharge consumes certified rational interval\nbounds instead: $B(8{\\cdot}10^4) \\le 332\\,000$ and\n$S_\\infty(8{\\cdot}10^4) \\ge 336\\,000$, i.e.\\\n$\\mathrm{margin}(8\\times10^4) \\ge 4\\,001$, together with the direct\ncomparison $\\mathrm{margin}(10^5) > \\mathrm{margin}(8\\times10^4)$\n(\\texttt{NguyenRH1}, \\texttt{marginTilde\\_FAlt\\_80000\\_pos},\n\\texttt{marginTilde\\_FAlt\\_80000\\_lt\\_100000}).}\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. A normalization remark is required here. Johansson\n\\cite{johansson2015} tabulates the \\emph{Keiper} normalization,\ndefined by\n\\[\n\\log\\xi\\!\\left(\\frac1{1-x}\\right)\n= -\\log 2 + \\sum_{n \\ge 1} \\Lambda_n x^n,\n\\]\nwhich differs from the Li normalization $\\lambda_n$ used in this paper\nby the positive factor\n\\[\n\\lambda_n = n\\,\\Lambda_n \\qquad (n \\ge 1)\n\\]\n(equate coefficients in $x\\,\\frac{d}{dx}\\log\\xi(1/(1-x))$ and use the\nsymmetry $\\rho \\leftrightarrow 1-\\rho$ of the zero set), so positivity\nis identical in the two conventions. Johansson's table\n(interval-arithmetic error bounds throughout) gives\n$\\Lambda_1, \\dots, \\Lambda_{100000}$ all positive, matching the\nRH-true asymptotic, with $\\Lambda_{100000} = 4.6258\\ldots$ certified\nto $\\sim 2900$ digits --- i.e.\\ $\\lambda_{100000} =\n10^5\\,\\Lambda_{100000} \\approx 462\\,580.78$ in the present\nnormalization. Independently, this project verifies $\\lambda_n > 0$\nfor all $n \\le 3000$ in the Li normalization (two methods --- the\narithmetic 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 residue cut at the actual contour height\n$\\tau_n \\in [\\sqrt n, \\sqrt n + 1]$ (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 $\\tau_n$ into a \\emph{dog-leg}: lift\nvertically from $3 + i\\tau_n$ to $3 + iU_n$ with\n$U_n := \\tfrac32\\,\\tau_n$ (the\nleft vertical), traverse horizontally at height $U_n$ (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, charged at the\nmajorant height $T_n$: the left vertical has length\n$\\tau_n/2 \\le (\\sqrt n + 1)/2$ and\ncontributes $\\le \\tfrac{\\sqrt n + 1}{4}(e^{5/2}+1)$; 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$ in the Li normalization\nof Section~3 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 ($13\\,160$ with the\nfinal formal-development 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))\\\\\n\\hspace*{2em}(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}\nAll seven hypotheses are trusted inputs --- assumed in the development,\nnot proved within it; every other step of the proof is machine-checked.\nTheir provenance is itemized in the following table.\n\\begin{center}\\scriptsize\n\\setlength{\\tabcolsep}{3pt}\n\\begin{tabular}{@{}l p{3.9cm} p{2.7cm} p{2.5cm}@{}}\n\\hline\nHypothesis & Statement & Source & Status \\\\\n\\hline\n\\texttt{RHUpTo} & $\\operatorname{Re}\\rho = 1/2$ for all zeros with\n  $|\\gamma| \\le 3\\times10^{12}$ &\n  Platt--Trudgian \\cite{platt2021riemann}, interval arithmetic &\n  computational certificate \\\\\n\\texttt{LiVerifiedUpTo} & $\\lambda_n > 0$ for $1 \\le n \\le 10^5$ &\n  Johansson \\cite{johansson2015} (Step-5 normalization); this project\n  to $n \\le 3000$ (App.~A) & computational certificate \\\\\n\\texttt{ZeroCountProp} & unit-window zero count $\\le C_0(t{+}1)$,\n  $t \\ge 2$ & Rosser \\cite{rosser1941}; derived (see below) &\n  derived explicit bound \\\\\n\\texttt{ZeroCountProp2} & two-unit zero count $\\le 0.6\\log(t{+}2) +\n  0.886\\log\\log(t{+}2) + 2.7$, $t \\ge 10$ &\n  Rosser \\cite{rosser1941}; derived (see below) &\n  derived explicit bound \\\\\n\\texttt{ZeroCountGlobalProp} & global zero count $N(T) \\le F(T)$,\n  $T \\ge 2$ & Rosser \\cite{rosser1941} (enlarged majorant); derived\n  (see below) & derived explicit bound \\\\\n\\texttt{NoLowZeros} & $|\\gamma| \\ge 14$ for every nontrivial zero &\n  Platt \\cite{platt2017isolating}; Gram\n  \\cite{gram1903} (see below) & computational certificate \\\\\n\\texttt{MZeroProp} & $|\\zeta'/\\zeta(-\\tfrac52 + it)| \\le 1.3352$ for\n  $|t| \\le 10$ & this project (E-023), interval arithmetic &\n  computational certificate \\\\\n\\hline\n\\end{tabular}\n\\end{center}\nThe three zero-counting rows are derived bounds, not printed as such:\nthey are elementary specializations of the Riemann--von Mangoldt\nformula $N(T) = F(T) + S(T)$, $F(T) = \\frac{T}{2\\pi}\\log\\frac{T}{2\\pi\ne} + \\frac78$, combined with Rosser's explicit bound\n$|S(T)| \\le 0.137\\log T + 0.443\\log\\log T + 1.588$, valid for\n$T \\ge 1467$ \\cite{rosser1941} (tabulated with its provenance in\n\\cite[Table~1]{trudgian2014ii}). The two window forms take differences\nof the formula at the window endpoints, and the global form uses\n$N(T) \\le F(T) + |S(T)|$; the additive constants and the enlargement\nof $F$ absorb the ranges below Rosser's threshold via the finite-range\nverifications $|S(T)| \\le 1$ for $T \\le 280$ and $|S(T)| \\le 2$ for\n$T \\le 6.8\\times10^6$ \\cite[Eq.~(1.2)]{trudgian2014ii}.\n\\texttt{NoLowZeros} is logically separate\nfrom \\texttt{RHUpTo}: it asserts a location fact about the low zeros,\nnot RH on an initial segment. Its provenance is zero-location\ncomputation: Platt \\cite{platt2017isolating} rigorously isolates the\nnontrivial zeros with $0 < \\gamma \\le 3.06\\times10^{10}$ by interval\narithmetic (an independent verification of RH to that height), the\nlowest at $\\gamma_1 = 14.134725\\ldots$ --- a value classical since\nGram \\cite{gram1903} --- so no nontrivial zero has $|\\gamma| < 14$;\nthe Platt--Trudgian verification \\cite{platt2021riemann} extends the\non-line confirmation to height $3\\times10^{12}$ via Turing's method.\n\\texttt{MZeroProp} is a grid\nevaluation with a sampled-Lipschitz margin of safety $\\times 2$\n(E-023), in the same interval-arithmetic trust class.\n\nThe proof of \\texttt{SfBoundProp} contains the full complex-analytic\ncontent 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}\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 $F{+}S_b$-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\nits declared perimeter: the four computational certificates of the\ntable above (the Platt--Trudgian verifications, the Li tables, the\nzero-location certificate, and the interval constant) and the three\nexplicit zero-counting bounds derived from the Riemann--von Mangoldt\nformula with Rosser's $S(T)$ bound \\cite{rosser1941}. The\nformal reduction leaves exactly those seven inputs as trusted, which we\nregard as the honest formal target: every other step of the proof is\nmachine-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": 113,
      "oldLines": 8,
      "newStart": 113,
      "newLines": 9,
      "lines": [
        " $\\log^2$ denominator (Remark~(i)). The novelty claimed here is not the",
        " $T^2$ scale itself but the explicit, fully constant-traced,",
        " \\emph{strict}-positivity assembly --- Lagarias's contour argument",
        "-\\cite{lagarias2007li} with Rosser's explicit $S(T)$ bound",
        "-\\cite{rosser1941}, an elementary archimedean lower bound, a proved",
        "+\\cite{lagarias2007li} with Rosser's explicit Riemann--von Mangoldt",
        "+error bound \\cite[Thm~19]{rosser1941}, an elementary archimedean",
        "+lower bound, a proved",
        " margin convexity, the dog-leg repair of Section~\\ref{subsec:dogleg},",
        " and the finite verifications --- and its machine verification; that",
        " assembly we have found nowhere else in the literature."
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}