[{"type":"thinking","thinking":"Committed. Now print both in the response (the user asked \"provide me\"). They're saved at research/paper/cover-letter.md and referee-list.md. Present them in full — the cover letter text and the referee list. Keep the surrounding commentary minimal.","signature":""},{"type":"text","text":"Both saved to the archive (`research/paper/cover-letter.md`, `referee-list.md`) and committed (`0d5ee7c`). Full text below.\n\n---\n\n## Cover letter\n\n> [Dan T Nguyen] — Research Ai — [contact email] — ORCID: [register at orcid.org]\n>\n> [Date]\n>\n> To the Editors, *Experimental Mathematics*\n>\n> **Subject: submission of \"An explicit finite-height Li-positivity theorem with a machine-verified assembly\"**\n>\n> Dear Editors,\n>\n> Please consider the enclosed manuscript for publication in *Experimental Mathematics*.\n>\n> The paper proves that the Keiper–Li coefficients of the Riemann ξ-function satisfy λ_n > 0 for all 1 ≤ n ≤ (T₀−1)² ≈ 9×10²⁴, conditional on the interval-arithmetic verification of the Riemann hypothesis to height T₀ = 3×10¹² (Platt–Trudgian) and on finite Li-coefficient computations (this project to n = 3000, by two independent methods agreeing to 4.8×10⁻²⁵ relative; Misguich–Voros to n = 5×10⁵). By Voros's sharpening, no infinite-range partial statement exists, so an explicit finite-height statement is the maximal content of the Li route short of RH. To our knowledge this is the first time the full explicit chain — Lagarias's contour argument with Trudgian's explicit zero-counting bounds, an elementary archimedean lower bound, a proved margin convexity, and the finite verifications — has been assembled with every constant traced.\n>\n> Two features may be of particular interest to the journal's readers. First, the result sits squarely in the journal's tradition of rigorous computation in analytic number theory — the finite verification this paper builds on (Voros, Exp. Math. 29(4): 452–469, 2020) appeared in these pages. Second, the entire reduction is machine-verified in Lean 4: the theorem is proved from exactly three named hypotheses — the two computational certificates above and a single named analytic hypothesis (the traced contour bound |S_f(n)| ≤ B(n) on the relevant range) — with the axiom profile restricted to the three standard axioms and no sorry placeholders anywhere in the Li chain; even the two elementary margin evaluations are discharged inside the development by certified rational interval bounds. The formalization process itself contributed to the mathematics: it caught a hypothesis-falsifying sign flaw in the informal zero-count majorant (the ψ-functional of the Trudgian F + S_b crosses zero near T ≈ 16), repaired by a documented majorant swap at a traced cost of 256 in a margin of 15 764.\n>\n> The manuscript is original, is not under consideration elsewhere, and has no competing interests or external funding. All numerical inputs are produced by deterministic, archived scripts; the complete project archive (Lean 4 development, experiment scripts, CSV/JSON data, audit trails) will be publicly available at [repository URL — inserted at submission]. The manuscript carries an AI Contribution Statement disclosing substantial machine assistance in the research process; the human author takes full responsibility as guarantor of the work, and all machine-produced mathematics is machine-checked, cross-validated by deterministic computation, or explicitly tagged otherwise in the text.\n>\n> Suggested referees are listed in the accompanying document.\n>\n> Sincerely,\n> Dan T Nguyen, Research Ai\n\n---\n\n## Referee list (6)\n\n1. **David J. Platt** — University of Bristol. Explicit zero computations; co-author of the RH-to-3×10¹² certificate the theorem is built on. Positioned to judge the bridge window N₁ = (T₀−1)².\n2. **Timothy S. Trudgian** — UNSW Canberra (ADFA). Author of the N(T)/S(T) bounds used as the declared trusted perimeter; can check the traced constants (A = 10.5, B₀ = 48, the honest C₀) at a glance.\n3. **André Voros** — CEA-Saclay. Li-criterion sharpening (the maximality frame) and the λ_n verification to 5×10⁵ with Misguich — the direct predecessor computation this paper overlaps.\n4. **Jeffrey C. Lagarias** — University of Michigan. Author of the contour argument (Thm 6.1) the paper traces; senior Keiper–Li figure for the assembly-level judgment.\n5. **Andrew R. Booker** — University of Bristol. Computational NT, rigorous high-precision numerics, certified-computation methodology.\n6. **Alex Kontorovich** — Rutgers. Analytic number theory with active engagement in computation and formal methods — bridges the number theory and the Lean novelty.\n\n**Notes:** 1–3's published work is *used* as inputs, never criticized — no conflict (no collaborations, shared institutions, or personal ties). If the venue caps the list at 4: Platt, Trudgian, Voros, Booker. If you submit to a formal-verification venue instead, swap #4 for a Lean/Mathlib number theorist. Verify current affiliations and emails on institutional pages at submission time — they drift.\n\n---\n\nTwo placeholders to fill when you submit: the **repository URL** (cover letter) and your **ORCID/contact details**. Whenever you're ready, I can do the repo-publication prep (README, Lean build instructions, license) so the archive link in the letter resolves to something real."}]