Paper & Sources

paperA.tex — first 80 lines

% ============================================================
% NGUYEN-RH-1 — PAPER A (split 2026-08-20, session 013, from draft.tex)
% An explicit finite-height Li-positivity theorem, machine-verified.
% Self-contained artifact per the session-012-end-notes review:
% §3.1 + Appendices A.1/B of the combined draft, retargeted.
% The spectral-line material lives in paperB.tex (in preparation).
% Session 045 (2026-09-01, expert-review revision): focused-note form —
% the certificate-method background and the obstruction analysis were
% removed (Paper B material); the density-theorem framing dropped;
% Appendix C (derivations of the three zero-counting bounds) added.
% ============================================================
\documentclass[11pt]{article}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{microtype}
\usepackage[colorlinks=true,linkcolor=blue,citecolor=blue]{hyperref}

% The prose is dense with unhyphenatable compounds (Li-positivity,
% [proved, ...] tags). Give TeX room to spread the slack instead of
% running past the right margin.
\emergencystretch=2em

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\title{An explicit finite-height Li-positivity theorem\\
with a machine-verified assembly\thanks{This work was produced with
substantial machine assistance; see the AI Contribution Statement.}}
\author{Dan T Nguyen\thanks{Independent researcher}}
\date{Started: 2026-08-17; revised 2026-09-01}

\begin{document}
\maketitle

\begin{abstract}
[proved, conditional on computation] The Keiper--Li coefficients of the
Riemann $\xi$-function satisfy $\lambda_n > 0$ for all
$1 \le n \le (T_0-1)^2 \approx 9\times10^{24}$, conditional on the
interval-arithmetic verification of RH to height $T_0 = 3\times10^{12}$
(Platt--Trudgian) and on finite Li-coefficient computations
(Johansson's rigorous table to $10^5$ and this project's to $3000$),
with every constant traced. We have found no previous explicit assembly
of this chain in the literature; by Voros's sharpening, positivity of
all sufficiently large $\lambda_n$ would itself imply RH, so no result
short of RH can assert an infinite positive tail. Moreover the full
reduction is machine-verified in Lean~4 (package \texttt{NguyenRH1}):
the theorem is proved from exactly seven explicit perimeter inputs,
itemized with provenance in Appendix~B --- three explicit
zero-counting bounds, derived in Appendix~C from the explicit
Riemann--von Mangoldt error bounds of Rosser and Trudgian, and four
computational certificates
(the Platt--Trudgian RH verification, Johansson's rigorous
Keiper-coefficient table to $10^5$ transferred to the Li normalization,
a zero-location certificate for the low zeros, and one short-segment
interval constant) --- with the traced contour bound
$|S_f(n)| \le B(n)$ on $10^5 \le n \le (T_0-1)^2$ itself machine-proved
from six of the seven (all but the Li table), and with axiom profile
exactly the three standard
axioms (\texttt{propext}, \texttt{Classical.choice},
\texttt{Quot.sound}) and no \texttt{sorry} anywhere in the
development's Li chain.
\end{abstract}

\section{Introduction}

The Riemann hypothesis (RH) asserts that every nontrivial zero of
$\zeta(s)$ has real part $1/2$. \emph{Li's criterion} reformulates it
as a positivity statement: the Keiper--Li coefficients
$\lambda_n = \sum_\rho{}'\,[1 - (1 - 1/\rho)^n]$ of the Riemann
$\xi$-function satisfy $\lambda_n > 0$ for all $n \ge 1$ if and only
if RH holds \cite{li1997, bombieri1999lagarias}, and by Voros's
sharpening the positivity of any tail $\{\lambda_n\}_{n \ge N_0}$
already implies RH \cite{voros2006sharpenings}.

This note proves an explicit \emph{transfer theorem} on this route:
the interval-arithmetic verification of RH to height $T_0$ transfers

Source library