{
  "file_path": "D:\\Python\\Quantum\\STATE.md",
  "old_string": "# STATE.md \u2014 NGUYEN-RH-1 RESUME POINT\n# \u2b50 READ THIS FIRST at the start of every session.\nLast updated: 2026-08-23 | Session 028 COMPLETE \u2014 **ii\u2032-5e-iii\nCOMPLETE** (the zero-side partial-fraction series: summability,\nanalyticity off the zeros, isolation + the reduced series;\nLiSeries.lean, 22 decls, 3 standard axioms only, build GREEN 8765).\nTIER ii\u2032 in progress (user decision: option (a) \u2014 close SfBoundProp\nin Lean BEFORE submission; Paper A frozen/submittable throughout).",
  "new_string": "# STATE.md \u2014 NGUYEN-RH-1 RESUME POINT\n# \u2b50 READ THIS FIRST at the start of every session.\nLast updated: 2026-08-23 | Session 029 COMPLETE \u2014 **ii\u2032-5e-iv\nCOMPLETE** (F ENTIRE: the punctured-limit extension Gentire of Fexpr\nis everywhere analytic and agrees with Fexpr at every good point;\nLiFEntire.lean, 30 decls, 3 standard axioms only, build GREEN 8766).\nTIER ii\u2032 in progress (user decision: option (a) \u2014 close SfBoundProp\nin Lean BEFORE submission; Paper A frozen/submittable throughout)."
}

{
  "filePath": "D:\\Python\\Quantum\\research\\paper\\paperA.tex",
  "oldString": "\\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--013). 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}), the numerical\nexperiment suite (E-001--E-029), and adversarial self-audit (D-060:\nfour independent audit instances, $\\sim$55 claims checked, 10\ncorrections filed). 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.",
  "newString": "\\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.",
  "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-20}\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, with every\nconstant traced. This is the first assembled explicit chain of its\nkind; by Voros's sharpening it is the maximal content of the Li route\nshort of RH. Moreover the full reduction is machine-verified in Lean~4\n(package \\texttt{NguyenRH1}): the theorem is proved from exactly eight\nnamed hypotheses --- the two computational certificates above and six\ndeclared analytic inputs (Trudgian's explicit zero-counting bounds in\ntheir unit-window, two-unit, and global forms, a Platt-class\nzero-location certificate, and one short-segment interval constant),\nwith the traced contour bound $|S_f(n)| \\le B(n)$ on $10^5 \\le n \\le\n(T_0-1)^2$ itself machine-proved from those six --- with axiom profile\nexactly the three standard axioms (\\texttt{propext},\n\\texttt{Classical.choice}, \\texttt{Quot.sound}) and no \\texttt{sorry}\nanywhere in the development'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 the Riemann hypothesis verified to height\n$T_0 = 3\\times 10^{12}$ (Platt--Trudgian \\cite{platt2021riemann},\ninterval arithmetic). Then the Keiper--Li coefficients 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 no infinite-range partial statement exists, so\nthis is the maximal content of the Li route short of RH; the explicit\nchain --- Lagarias's contour argument \\cite{lagarias2007li} with\nTrudgian's explicit zero-counting bounds \\cite{trudgian2014}, an\nelementary archimedean lower bound, a proved margin convexity, and the\nfinite verifications --- appears not to have been assembled before.\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 the machinery behind the state-of-the-art density theorem\n\\cite{anthropic2026riemann}, which is the launchpad and the sanity\ngate for everything below; details and notation follow that paper.\n\n\\emph{The Weil explicit formula} \\cite{weil1952fonctions} expresses,\nfor a test function $\\psi$ supported in $[-\\tfrac12,\\tfrac12]$ (the\n\\emph{bandwidth-one} class), a quadratic form on the zeros as a\nfunctional of the primes. Compressing it via a Gabor (Gaussian\nwindowed exponential) frame at the critical density $h = 2\\pi/L$\nyields a finite matrix identity $\\tilde G = P + Q$: a zero-side\nmatrix $\\tilde G$ built from the zeros in a window of size $L$\ndecomposes into a prime-side matrix $P$ (computed unconditionally\nfrom Montgomery's second moment / pair-correlation input\n\\cite{montgomery1973pair}) and a controlled remainder $Q$.\n\n\\emph{The rank--trace inequality.} Writing $\\tilde G$ in inertia form,\na rank--trace comparison between the positive eigenspace of $\\tilde G$\nand the positive part of $P$ converts the second-moment input\n$\\|\\tilde G\\|_{HS}^2 = (R(\\psi) + o(1))\\,N$ into a lower bound on the\nnumber of simple on-line zeros in the window. The strength of the\ncertificate is governed by the \\emph{window ratio}\n\\[\nR(\\psi) \\;=\\; \\frac{\\int \\psi^2 \\;+\\;\n\\iint |u-v|\\,\\psi(u)\\psi(v)\\,du\\,dv}{\\bigl(\\int \\psi\\bigr)^2}\n\\qquad (\\psi \\in C([-\\tfrac12,\\tfrac12]) \\text{ even}, \\ \\psi > 0),\n\\]\nwith $R(\\psi_0) = 4/3$ for the flat window\n$\\psi_0 = \\mathbf 1_{[-1/2,1/2]}$ and\n$R(\\psi_{MT}) = \\tfrac12 + \\tfrac{1}{\\sqrt2}\\cot\\tfrac{1}{\\sqrt2}\n= 1.32749\\ldots$ for the Montgomery--Taylor window (both verified\nsymbolically and against $60$-digit reference values in this project,\nE-001), giving the certified fractions $2 - R(\\psi)$: $0.6725$ of\nzeros simple and on the line, $0.83625$ distinct. A sharpness analysis\nlocates the bandwidth-one ceiling of the method at $\\approx 0.682$,\nand shows the obstructions to going further are structural\n(Section~4).\n\nOne feature of this machinery matters here: the certificate fails, as\nit must, for the Davenport--Heilbronn and Epstein zeta functions\n(which violate the RH-analogue); the main theorem of this paper has\nbeen required to pass this 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 the Riemann hypothesis verified to height\n$T_0 = 3\\times 10^{12}$ (Platt--Trudgian \\cite{platt2021riemann},\ninterval arithmetic). Then\n\\[\n\\lambda_n > 0 \\qquad \\text{for all } 1 \\le n \\le N_1 := (T_0-1)^2\n= 8\\,999\\,999\\,999\\,994\\,000\\,000\\,000\\,001 \\approx 9.0\\times 10^{24}.\n\\]\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\\[\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\\]\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/D-072/D-074 with E-031/E-032): four adjustments to this\n$B(n)$ account 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-tail charge ``$3.3$''\ninherited from Lagarias's Thm~6.1 is broken at $T = \\sqrt n$: the\n(6.12) stepping product ratio is $e/2 > 1$, so the horizontal\nright-tail envelope grows like $e^{0.066\\sqrt n}$ (measured\n$\\sim 6\\times 10^{10}$ at $n = 10^5$); the repaired proof replaces\nthat segment by a zero-free dog-leg at height $\\tfrac32\\sqrt n$ (where\nthe repaired stepping applies), keeping $T = \\sqrt n$ and hence the\nendpoint $N_1 = (T_0-1)^2$ unchanged. (iv) The right-vertical kernel\nis charged honestly as $e^{1/3} I_{\\mathrm{Maj}}(n)$ (the uniform\nbound is $e^{\\sqrt n/2+1/3}+1$), the factor $e^{1/3} \\le 1.4$ being\nabsorbed by the $2\\pi$ normalization of the residue theorem. All four\ncorrections are machine-verified in \\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).} $\\lambda_n > 0$ for $n \\le 3000$\nby exact high-precision computation (this project, two independent\nmethods, agreement to $4.8\\times10^{-25}$ relative), and for\n$n \\le 5\\times10^5$ by Misguich--Voros \\cite{voros2017li}. The ranges\noverlap the $n = 10^5$ split by a factor $5$ (and the crossover\n$N_0 = 8\\times 10^4$ by $6.25$).\n\\end{proof}\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: Platt--Trudgian's\ninterval-arithmetic verification, and the finite Li-coefficient\nverifications.\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 \\texttt{lambda\\_pos\\_finite\\_height\\_closed} is\nmachine-proved from exactly eight named hypotheses: the two\ncomputational-perimeter inputs of Theorem~\\ref{thm:finite-height-li}\n(Platt--Trudgian; the Li verifications) and six declared analytic\ninputs --- Trudgian's explicit zero-counting bounds \\cite{trudgian2014}\nin their unit-window, two-unit, and global forms\n(\\texttt{ZeroCountProp}, \\texttt{ZeroCountProp2},\n\\texttt{ZeroCountGlobalProp}), a Platt-class zero-location certificate\n(\\texttt{NoLowZeros}), and the short-segment constant $M_0 = 1.3352$\n(\\texttt{MZeroProp}, an interval-arithmetic certificate in the same\ntrust class). The proof of \\texttt{SfBoundProp} contains the full\ncomplex-analytic content of Step 2: meromorphic residue machinery on\nrectangles (\\texttt{rectInt'\\_Jlag}), the partial-fraction identity\nfor $\\zeta'/\\zeta$ (\\texttt{partialFraction\\_identity}), the\nreference-point bound $|R(s)| \\le 10.5\\log(|t|{+}2) + 48$\n(\\texttt{logDeriv\\_riemannZeta\\_sub\\_nearZeros\\_le\\_tight}), the exact\nidentity $S_f(n) = \\mathrm{Res}_1(n)$ (\\texttt{sf\\_eq\\_resW1}), the\nzero-free dog-leg repair of the right tail\n(\\texttt{upper\\_right\\_horizontal\\_eq\\_dogleg} and the\n\\texttt{LiDogLeg} bounds), the four side bounds\n(\\texttt{LiSideBounds}), and the fold (\\texttt{sfBoundProp}). The two\nelementary evaluations of the explicit margin function that the\nassembly consumes ($\\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 six 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--013). 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}), the numerical\nexperiment suite (E-001--E-029), and adversarial self-audit (D-060:\nfour independent audit instances, $\\sim$55 claims checked, 10\ncorrections filed). 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": 417,
      "oldLines": 14,
      "newStart": 417,
      "newLines": 17,
      "lines": [
        " This research was conducted with substantial assistance from two AI",
        " systems: Kimi K3 (Moonshot AI), operated through the Claude Code",
        " harness (Anthropic), over an archived series of research sessions",
        "-(project ledger: sessions 001--013). Machine contributions included:",
        "+(project ledger: sessions 001--041). Machine contributions included:",
        " derivation drafting and constant-tracing (D-036/D-037/D-056/D-057),",
        " the Lean~4 formalization of the Li chain (package \\texttt{NguyenRH1}:",
        " \\texttt{sInfty\\_lower\\_bound}, \\texttt{marginTilde\\_convex},",
        "-\\texttt{lambda\\_pos\\_finite\\_height\\_verified}), the numerical",
        "-experiment suite (E-001--E-029), and adversarial self-audit (D-060:",
        "-four independent audit instances, $\\sim$55 claims checked, 10",
        "-corrections filed). All research direction, verification decisions,",
        "+\\texttt{lambda\\_pos\\_finite\\_height\\_verified},",
        "+\\texttt{sfBoundProp}, \\texttt{lambda\\_pos\\_finite\\_height\\_closed}),",
        "+the numerical experiment suite (E-001--E-034), and adversarial",
        "+self-audit (D-060: four independent audit instances, $\\sim$55 claims",
        "+checked, 10 corrections filed; D-071/D-072/D-074: four further",
        "+$B(n)$-account corrections found and repaired during the machine",
        "+closure). All research direction, verification decisions,",
        " perimeter declarations, and final approval are the responsibility of",
        " the human author, who serves as guarantor of the work. All",
        " machine-produced mathematics was validated by machine-checked proof"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}