Current task: —

← Session 18 — Lean tier (ii): finite-height proof + certified base points

#812 assistant 2026-08-20 21:13:37.427 UTC · 413319→2817 tok open ⤢
thinking (8772 chars)
The user wants: (1) a cover letter, (2) a referee list. For Paper A, targeting *Experimental Mathematics* (my top-ranked venue). Cover letter should be one page, honest, and in the project's voice. Key content: - What's submitted: title, one-line description - What's new: first assembled explicit finite-height Li chain; machine-verified assembly (Lean 4, three named hypotheses) - Why this venue: computational/experimental number theory with full rigor; the Voros precedent (Exp. Math. published the λ_n verification to 5×10⁵ that this paper uses) - Conditional-on-computation honesty stated up front - AI disclosure already in the paper - Data/code availability (repo — currently being prepared for public release; I should phrase it carefully since the repo isn't public yet: "the full project archive (Lean development, deterministic scripts, CSV data) will be made publicly available at submission" — hmm, or write it as available. Better: write the letter with a placeholder for the repo URL.) - Suggested referees are a separate list. Referee list: I need to be careful and honest. I should suggest real people whose expertise matches, based on my knowledge of the field. I should NOT fabricate contact details. I can name people with their relevant expertise; the user can find current emails from their institutional pages. People: 1. **David J. Platt** (University of Bristol, UK) — co-author of the Platt–Trudgian RH-to-3×10¹² computation the paper relies on; expert in explicit computations of zeros. Direct interest: the paper's height T₀ is his result. 2. **Timothy S. Trudgian** (UNSW Canberra / Australian National University?) — Trudgian is at UNSW Canberra (ADFA). His explicit N(T)/S(T) bounds are the paper's perimeter. (Note: some editors consider citing someone's work heavily a reason they're a good referee, though there's a mild COI consideration — they're not collaborators, just cited; that's standard and fine.) 3. **André Voros** (CEA Saclay) — author of the Misguich–Voros λ_n verification to 5×10⁵ (Exp. Math. 2020); the direct predecessor. Also Voros's sharpening theorem is used. 4. **Jeffrey C. Lagarias** (University of Michigan) — author of the contour argument (Lagarias Thm 6.1) the paper traces; Li-criterion expert. He might be an obvious referee; senior figure. 5. **Enrico Bombieri** (IAS Princeton) — Bombieri–Lagarias Thm 2 author. Very senior; maybe too senior but legitimate. 6. **Formal verification angle**: someone in the Lean/Mathlib number-theory community — e.g., **Kevin Buzzard** (Imperial) — high-profile Lean advocate; or **Alex Kontorovich** (Rutgers) — number theorist who uses formal verification/computation and is an editor-ish figure in experimental NT circles. Kontorovich is a strong suggestion: computational NT + harmonic analysis + active in formal methods awareness. 7. **Andrew Booker** (Bristol) — computational number theory, zeros computations, also has formal-verification awareness. For a referee list, 4–6 names with one-line expertise rationale. I should add honest caveats: no current collaborations known; verify current affiliations/emails yourself. Also note who to EXCLUDE (none needed). Also be careful: I must not fabricate emails. I'll give names + institutions + why. And add a note: check each journal's conflict rules. Cover letter format: - Date, To the Editors of Experimental Mathematics - Submission title - 3 paragraphs: what it is / what's new / why this journal + disclosures - Statements: originality, not under consideration elsewhere, no conflicts, no external funding, data availability, AI-use disclosure pointer. Where to put these? The user asked to "provide" them — I could print in the response AND save to files (research/paper/cover-letter.md or .tex?). Given the archive discipline (everything saved), I'll write both to files: research/paper/submission/cover-letter.md and referee-list.md. Wait — new directories... the instructions say verify parent dir exists before creating. research/paper/ exists; a submission/ subfolder is new. I can create it (the Bash instruction says check parent exists first — research/paper exists ✓). Or just put cover-letter.md directly in research/paper/. Simpler: research/paper/cover-letter.md + referee-list.md. Hmm — these are paper-related; keeping them in research/paper/ is fine. Also should print the full text in my response since the user asked "provide me". Yes — print both fully, save both, commit. Cover letter draft: --- Date: 2026-08-20 (leave as [Date]) To the Editors, Experimental Mathematics Subject: Submission of "An explicit finite-height Li-positivity theorem with a machine-verified assembly" Dear Editors, Please consider the enclosed manuscript for publication in Experimental Mathematics. The paper proves that the Keiper–Li coefficients 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 (ours to n = 3000, cross-validated by two independent methods; Misguich–Voros to n = 5×10⁵). By Voros's sharpening, no infinite-range partial statement of this kind 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. 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; indeed the finite verification we build on (Voros, Exp. Math. 29(4), 2020) appeared in this journal. 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. The 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, repaired at a traced cost of 256 in a margin of 15 764. The manuscript is original, is not under consideration elsewhere, and has no competing interests or external funding. All numerical inputs are produced by deterministic scripts; the complete project archive (Lean development, scripts, data, audit trails) will be publicly available at [repository URL — to be inserted before submission]. The manuscript contains 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, or explicitly tagged. Suggested referees are listed separately. Sincerely, Dan T Nguyen (Research Ai) [contact email] --- Referee list draft: 1. David J. Platt (University of Bristol) — explicit zero computations; author of the RH-to-3×10¹² interval-arithmetic certificate the theorem builds on. 2. Timothy S. Trudgian (UNSW Canberra) — explicit analytic number theory; author of the N(T)/S(T) bounds used as the declared trusted perimeter. 3. André Voros (CEA-Saclay) — Li-criterion theory and the λ_n > 0 verification to n = 5×10⁵ (Exp. Math. 2020), the direct predecessor computation; also the sharpening theorem framing the result's maximality. 4. Jeffrey C. Lagarias (University of Michigan) — author of the contour argument (Thm 6.1) traced by the paper; Li/Keiper expert. 5. Andrew R. Booker (University of Bristol) — computational number theory, zeros of L-functions, rigorous numerics. 6. Alex Kontorovich (Rutgers University) — analytic number theory with strong computational and formal-methods engagement. Notes: no known collaborations/conflicts with the author; verify current affiliations and emails on institutional pages before submission; if the journal allows, Platt/Trudgian/Voros are the three most directly engaged with the paper's inputs (their work is used, not criticized). Hmm — one consideration: is it appropriate to suggest people whose work is used? Yes — standard practice; using published work doesn't create a COI. Only collaborations/institutional/personal ties do. Add that note. Also add an "oppose" note: none. Keep responses concise-ish but complete. Save files + commit. Also print both in the reply.
Saving both to the archive and printing them here.
tool: Write ok
input
{
  "file_path": "D:\\Python\\Quantum\\research\\paper\\cover-letter.md",
  "content": "# Cover letter \u2014 Paper A submission\nTarget venue: Experimental Mathematics (first choice; adapt salutation if rerouted)\nDraft date: 2026-08-20. Bracketed items to fill at submission.\n\n---\n\n[Dan T Nguyen]\nResearch Ai\n[postal address optional]\n[contact email] | ORCID: [0000-xxxx \u2014 register at orcid.org]\n\n[Date]\n\nTo the Editors\n*Experimental Mathematics*\n\n**Subject: submission of \"An explicit finite-height Li-positivity\ntheorem with a machine-verified assembly\"**\n\nDear Editors,\n\nPlease consider the enclosed manuscript for publication in\n*Experimental Mathematics*.\n\nThe paper proves that the Keiper\u2013Li coefficients of the Riemann\n\u03be-function satisfy \u03bb_n > 0 for all 1 \u2264 n \u2264 (T\u2080\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074,\nconditional on the interval-arithmetic verification of the Riemann\nhypothesis to height T\u2080 = 3\u00d710\u00b9\u00b2 (Platt\u2013Trudgian) and on finite\nLi-coefficient computations (this project to n = 3000, by two\nindependent methods agreeing to 4.8\u00d710\u207b\u00b2\u2075 relative; Misguich\u2013Voros to\nn = 5\u00d710\u2075). By Voros's sharpening, no infinite-range partial statement\nexists, so an explicit finite-height statement is the maximal content\nof the Li route short of RH. To our knowledge this is the first time\nthe full explicit chain \u2014 Lagarias's contour argument with Trudgian's\nexplicit zero-counting bounds, an elementary archimedean lower bound,\na proved margin convexity, and the finite verifications \u2014 has been\nassembled with every constant traced.\n\nTwo features may be of particular interest to the journal's readers.\nFirst, the result sits squarely in the journal's tradition of rigorous\ncomputation in analytic number theory \u2014 the finite verification this\npaper builds on (Voros, Exp. Math. 29(4): 452\u2013469, 2020) appeared in\nthese pages. Second, the entire reduction is machine-verified in\nLean 4: the theorem is proved from exactly three named hypotheses \u2014\nthe two computational certificates above and a single named analytic\nhypothesis (the traced contour bound |S_f(n)| \u2264 B(n) on the relevant\nrange) \u2014 with the axiom profile restricted to the three standard\naxioms and no sorry placeholders anywhere in the Li chain; even the\ntwo elementary margin evaluations are discharged inside the\ndevelopment by certified rational interval bounds. The formalization\nprocess itself contributed to the mathematics: it caught a\nhypothesis-falsifying sign flaw in the informal zero-count majorant\n(the \u03c8-functional of the Trudgian F + S_b crosses zero near T \u2248 16),\nrepaired by a documented majorant swap at a traced cost of 256 in a\nmargin of 15 764.\n\nThe manuscript is original, is not under consideration elsewhere, and\nhas no competing interests or external funding. All numerical inputs\nare produced by deterministic, archived scripts; the complete project\narchive (Lean 4 development, experiment scripts, CSV/JSON data, audit\ntrails) will be publicly available at [repository URL \u2014 inserted at\nsubmission, see the repo-prep checklist]. The manuscript carries an AI\nContribution Statement disclosing substantial machine assistance in\nthe research process; the human author takes full responsibility as\nguarantor of the work, and all machine-produced mathematics is\nmachine-checked, cross-validated by deterministic computation, or\nexplicitly tagged otherwise in the text.\n\nSuggested referees are listed in the accompanying document.\n\nSincerely,\n\nDan T Nguyen\nResearch Ai\n"
}
result 2026-08-20 21:13:37Z → 2026-08-20 21:13:37Z
{
  "type": "create",
  "filePath": "D:\\Python\\Quantum\\research\\paper\\cover-letter.md",
  "content": "# Cover letter \u2014 Paper A submission\nTarget venue: Experimental Mathematics (first choice; adapt salutation if rerouted)\nDraft date: 2026-08-20. Bracketed items to fill at submission.\n\n---\n\n[Dan T Nguyen]\nResearch Ai\n[postal address optional]\n[contact email] | ORCID: [0000-xxxx \u2014 register at orcid.org]\n\n[Date]\n\nTo the Editors\n*Experimental Mathematics*\n\n**Subject: submission of \"An explicit finite-height Li-positivity\ntheorem with a machine-verified assembly\"**\n\nDear Editors,\n\nPlease consider the enclosed manuscript for publication in\n*Experimental Mathematics*.\n\nThe paper proves that the Keiper\u2013Li coefficients of the Riemann\n\u03be-function satisfy \u03bb_n > 0 for all 1 \u2264 n \u2264 (T\u2080\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074,\nconditional on the interval-arithmetic verification of the Riemann\nhypothesis to height T\u2080 = 3\u00d710\u00b9\u00b2 (Platt\u2013Trudgian) and on finite\nLi-coefficient computations (this project to n = 3000, by two\nindependent methods agreeing to 4.8\u00d710\u207b\u00b2\u2075 relative; Misguich\u2013Voros to\nn = 5\u00d710\u2075). By Voros's sharpening, no infinite-range partial statement\nexists, so an explicit finite-height statement is the maximal content\nof the Li route short of RH. To our knowledge this is the first time\nthe full explicit chain \u2014 Lagarias's contour argument with Trudgian's\nexplicit zero-counting bounds, an elementary archimedean lower bound,\na proved margin convexity, and the finite verifications \u2014 has been\nassembled with every constant traced.\n\nTwo features may be of particular interest to the journal's readers.\nFirst, the result sits squarely in the journal's tradition of rigorous\ncomputation in analytic number theory \u2014 the finite verification this\npaper builds on (Voros, Exp. Math. 29(4): 452\u2013469, 2020) appeared in\nthese pages. Second, the entire reduction is machine-verified in\nLean 4: the theorem is proved from exactly three named hypotheses \u2014\nthe two computational certificates above and a single named analytic\nhypothesis (the traced contour bound |S_f(n)| \u2264 B(n) on the relevant\nrange) \u2014 with the axiom profile restricted to the three standard\naxioms and no sorry placeholders anywhere in the Li chain; even the\ntwo elementary margin evaluations are discharged inside the\ndevelopment by certified rational interval bounds. The formalization\nprocess itself contributed to the mathematics: it caught a\nhypothesis-falsifying sign flaw in the informal zero-count majorant\n(the \u03c8-functional of the Trudgian F + S_b crosses zero near T \u2248 16),\nrepaired by a documented majorant swap at a traced cost of 256 in a\nmargin of 15 764.\n\nThe manuscript is original, is not under consideration elsewhere, and\nhas no competing interests or external funding. All numerical inputs\nare produced by deterministic, archived scripts; the complete project\narchive (Lean 4 development, experiment scripts, CSV/JSON data, audit\ntrails) will be publicly available at [repository URL \u2014 inserted at\nsubmission, see the repo-prep checklist]. The manuscript carries an AI\nContribution Statement disclosing substantial machine assistance in\nthe research process; the human author takes full responsibility as\nguarantor of the work, and all machine-produced mathematics is\nmachine-checked, cross-validated by deterministic computation, or\nexplicitly tagged otherwise in the text.\n\nSuggested referees are listed in the accompanying document.\n\nSincerely,\n\nDan T Nguyen\nResearch Ai\n",
  "structuredPatch": [],
  "originalFile": null
}
raw content_json (database row)
[{"type":"thinking","thinking":"The user wants: (1) a cover letter, (2) a referee list. For Paper A, targeting *Experimental Mathematics* (my top-ranked venue).\n\nCover letter should be one page, honest, and in the project's voice. Key content:\n- What's submitted: title, one-line description\n- What's new: first assembled explicit finite-height Li chain; machine-verified assembly (Lean 4, three named hypotheses)\n- Why this venue: computational/experimental number theory with full rigor; the Voros precedent (Exp. Math. published the λ_n verification to 5×10⁵ that this paper uses)\n- Conditional-on-computation honesty stated up front\n- AI disclosure already in the paper\n- Data/code availability (repo — currently being prepared for public release; I should phrase it carefully since the repo isn't public yet: \"the full project archive (Lean development, deterministic scripts, CSV data) will be made publicly available at submission\" — hmm, or write it as available. Better: write the letter with a placeholder for the repo URL.)\n- Suggested referees are a separate list.\n\nReferee list: I need to be careful and honest. I should suggest real people whose expertise matches, based on my knowledge of the field. I should NOT fabricate contact details. I can name people with their relevant expertise; the user can find current emails from their institutional pages. People:\n\n1. **David J. Platt** (University of Bristol, UK) — co-author of the Platt–Trudgian RH-to-3×10¹² computation the paper relies on; expert in explicit computations of zeros. Direct interest: the paper's height T₀ is his result.\n2. **Timothy S. Trudgian** (UNSW Canberra / Australian National University?) — Trudgian is at UNSW Canberra (ADFA). His explicit N(T)/S(T) bounds are the paper's perimeter. (Note: some editors consider citing someone's work heavily a reason they're a good referee, though there's a mild COI consideration — they're not collaborators, just cited; that's standard and fine.)\n3. **André Voros** (CEA Saclay) — author of the Misguich–Voros λ_n verification to 5×10⁵ (Exp. Math. 2020); the direct predecessor. Also Voros's sharpening theorem is used. \n4. **Jeffrey C. Lagarias** (University of Michigan) — author of the contour argument (Lagarias Thm 6.1) the paper traces; Li-criterion expert. He might be an obvious referee; senior figure.\n5. **Enrico Bombieri** (IAS Princeton) — Bombieri–Lagarias Thm 2 author. Very senior; maybe too senior but legitimate.\n6. **Formal verification angle**: someone in the Lean/Mathlib number-theory community — e.g., **Kevin Buzzard** (Imperial) — high-profile Lean advocate; or **Alex Kontorovich** (Rutgers) — number theorist who uses formal verification/computation and is an editor-ish figure in experimental NT circles. Kontorovich is a strong suggestion: computational NT + harmonic analysis + active in formal methods awareness. \n7. **Andrew Booker** (Bristol) — computational number theory, zeros computations, also has formal-verification awareness.\n\nFor a referee list, 4–6 names with one-line expertise rationale. I should add honest caveats: no current collaborations known; verify current affiliations/emails yourself. Also note who to EXCLUDE (none needed).\n\nAlso be careful: I must not fabricate emails. I'll give names + institutions + why. And add a note: check each journal's conflict rules.\n\nCover letter format:\n- Date, To the Editors of Experimental Mathematics\n- Submission title\n- 3 paragraphs: what it is / what's new / why this journal + disclosures\n- Statements: originality, not under consideration elsewhere, no conflicts, no external funding, data availability, AI-use disclosure pointer.\n\nWhere to put these? The user asked to \"provide\" them — I could print in the response AND save to files (research/paper/cover-letter.md or .tex?). Given the archive discipline (everything saved), I'll write both to files: research/paper/submission/cover-letter.md and referee-list.md. Wait — new directories... the instructions say verify parent dir exists before creating. research/paper/ exists; a submission/ subfolder is new. I can create it (the Bash instruction says check parent exists first — research/paper exists ✓). Or just put cover-letter.md directly in research/paper/. Simpler: research/paper/cover-letter.md + referee-list.md. Hmm — these are paper-related; keeping them in research/paper/ is fine.\n\nAlso should print the full text in my response since the user asked \"provide me\". Yes — print both fully, save both, commit.\n\nCover letter draft:\n\n---\nDate: 2026-08-20 (leave as [Date])\n\nTo the Editors, Experimental Mathematics\n\nSubject: Submission of \"An explicit finite-height Li-positivity theorem with a machine-verified assembly\"\n\nDear Editors,\n\nPlease consider the enclosed manuscript for publication in Experimental Mathematics.\n\nThe paper proves that the Keiper–Li coefficients 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 (ours to n = 3000, cross-validated by two independent methods; Misguich–Voros to n = 5×10⁵). By Voros's sharpening, no infinite-range partial statement of this kind 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\nTwo 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; indeed the finite verification we build on (Voros, Exp. Math. 29(4), 2020) appeared in this journal. 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. The 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, repaired at a traced cost of 256 in a margin of 15 764.\n\nThe manuscript is original, is not under consideration elsewhere, and has no competing interests or external funding. All numerical inputs are produced by deterministic scripts; the complete project archive (Lean development, scripts, data, audit trails) will be publicly available at [repository URL — to be inserted before submission]. The manuscript contains 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, or explicitly tagged.\n\nSuggested referees are listed separately.\n\nSincerely,\nDan T Nguyen (Research Ai)\n[contact email]\n---\n\nReferee list draft:\n\n1. David J. Platt (University of Bristol) — explicit zero computations; author of the RH-to-3×10¹² interval-arithmetic certificate the theorem builds on.\n2. Timothy S. Trudgian (UNSW Canberra) — explicit analytic number theory; author of the N(T)/S(T) bounds used as the declared trusted perimeter.\n3. André Voros (CEA-Saclay) — Li-criterion theory and the λ_n > 0 verification to n = 5×10⁵ (Exp. Math. 2020), the direct predecessor computation; also the sharpening theorem framing the result's maximality.\n4. Jeffrey C. Lagarias (University of Michigan) — author of the contour argument (Thm 6.1) traced by the paper; Li/Keiper expert.\n5. Andrew R. Booker (University of Bristol) — computational number theory, zeros of L-functions, rigorous numerics.\n6. Alex Kontorovich (Rutgers University) — analytic number theory with strong computational and formal-methods engagement.\n\nNotes: no known collaborations/conflicts with the author; verify current affiliations and emails on institutional pages before submission; if the journal allows, Platt/Trudgian/Voros are the three most directly engaged with the paper's inputs (their work is used, not criticized).\n\nHmm — one consideration: is it appropriate to suggest people whose work is used? Yes — standard practice; using published work doesn't create a COI. Only collaborations/institutional/personal ties do. Add that note.\n\nAlso add an \"oppose\" note: none.\n\nKeep responses concise-ish but complete. Save files + commit. Also print both in the reply.","signature":""},{"type":"text","text":"Saving both to the archive and printing them here."},{"type":"tool_use","id":"Write_254","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\paper\\cover-letter.md","content":"# Cover letter — Paper A submission\nTarget venue: Experimental Mathematics (first choice; adapt salutation if rerouted)\nDraft date: 2026-08-20. Bracketed items to fill at submission.\n\n---\n\n[Dan T Nguyen]\nResearch Ai\n[postal address optional]\n[contact email] | ORCID: [0000-xxxx — register at orcid.org]\n\n[Date]\n\nTo the Editors\n*Experimental Mathematics*\n\n**Subject: submission of \"An explicit finite-height Li-positivity\ntheorem with a machine-verified assembly\"**\n\nDear Editors,\n\nPlease consider the enclosed manuscript for publication in\n*Experimental Mathematics*.\n\nThe paper proves that the Keiper–Li coefficients of the Riemann\nξ-function satisfy λ_n > 0 for all 1 ≤ n ≤ (T₀−1)² ≈ 9×10²⁴,\nconditional on the interval-arithmetic verification of the Riemann\nhypothesis to height T₀ = 3×10¹² (Platt–Trudgian) and on finite\nLi-coefficient computations (this project to n = 3000, by two\nindependent methods agreeing to 4.8×10⁻²⁵ relative; Misguich–Voros to\nn = 5×10⁵). By Voros's sharpening, no infinite-range partial statement\nexists, so an explicit finite-height statement is the maximal content\nof the Li route short of RH. To our knowledge this is the first time\nthe full explicit chain — Lagarias's contour argument with Trudgian's\nexplicit zero-counting bounds, an elementary archimedean lower bound,\na proved margin convexity, and the finite verifications — has been\nassembled with every constant traced.\n\nTwo features may be of particular interest to the journal's readers.\nFirst, the result sits squarely in the journal's tradition of rigorous\ncomputation in analytic number theory — the finite verification this\npaper builds on (Voros, Exp. Math. 29(4): 452–469, 2020) appeared in\nthese pages. Second, the entire reduction is machine-verified in\nLean 4: the theorem is proved from exactly three named hypotheses —\nthe two computational certificates above and a single named analytic\nhypothesis (the traced contour bound |S_f(n)| ≤ B(n) on the relevant\nrange) — with the axiom profile restricted to the three standard\naxioms and no sorry placeholders anywhere in the Li chain; even the\ntwo elementary margin evaluations are discharged inside the\ndevelopment by certified rational interval bounds. The formalization\nprocess itself contributed to the mathematics: it caught a\nhypothesis-falsifying sign flaw in the informal zero-count majorant\n(the ψ-functional of the Trudgian F + S_b crosses zero near T ≈ 16),\nrepaired by a documented majorant swap at a traced cost of 256 in a\nmargin of 15 764.\n\nThe manuscript is original, is not under consideration elsewhere, and\nhas no competing interests or external funding. All numerical inputs\nare produced by deterministic, archived scripts; the complete project\narchive (Lean 4 development, experiment scripts, CSV/JSON data, audit\ntrails) will be publicly available at [repository URL — inserted at\nsubmission, see the repo-prep checklist]. The manuscript carries an AI\nContribution Statement disclosing substantial machine assistance in\nthe research process; the human author takes full responsibility as\nguarantor of the work, and all machine-produced mathematics is\nmachine-checked, cross-validated by deterministic computation, or\nexplicitly tagged otherwise in the text.\n\nSuggested referees are listed in the accompanying document.\n\nSincerely,\n\nDan T Nguyen\nResearch Ai\n"},"extra_content":null}]