{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
  "old_string": "/-- [PROVED session 011] The full margin is C\u00b2 on (20, \u221e). -/",
  "new_string": "/-- [PROVED session 011] The margin is continuous on [20, \u221e) (endpoint\nincluded \u2014 the C\u00b2 regularity on (20, \u221e) does not give the endpoint). -/\ntheorem continuousOn_marginExpanded (F : \u211d \u2192 \u211d) (hF : ContDiff \u211d 2 F) :\n    ContinuousOn (marginExpanded F) (Set.Ici 20) := by\n  have hsqrt : ContinuousOn Real.sqrt (Set.Ici 20) := Real.continuous_sqrt.continuousOn\n  have hT : ContinuousOn (fun m => Real.sqrt m + 1) (Set.Ici 20) :=\n    hsqrt.add continuousOn_const\n  have hmaps : Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ici 20) (Set.Ioi (-1)) := by\n    intro x hx\n    have h : 20 \u2264 x := hx\n    have hnn := Real.sqrt_nonneg x\n    exact Set.mem_Ioi.mpr (by linarith)\n  have hlog : ContinuousOn Real.log (Set.Ici 20) :=\n    Real.continuousOn_log.mono (fun x hx => by\n      have h : 20 \u2264 x := hx\n      exact ne_of_gt (by linarith : (0 : \u211d) < x))\n  have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=\n    funext fun m => IIMaj_eq_psiTilde_sqrt m\n  unfold marginExpanded\n  refine (((((((((((contDiffOn_mS _).continuousOn.add\n    (hF.continuous.continuousOn.comp hT (Set.mapsTo_univ _ _) |>.const_mul (-2)) |>.add\n    (contDiffOn_TL1.continuousOn.comp hT hmaps).const_mul _) |>.add\n    (contDiffOn_TL2.continuousOn.comp hT hmaps).const_mul _) |>.add\n    (hT.const_mul _)) |>.add\n    (contDiffOn_L1sq.continuousOn.comp hT hmaps).const_mul _) |>.add\n    (contDiffOn_L1L2.continuousOn.comp hT hmaps).const_mul _) |>.add\n    (contDiffOn_L2sq.continuousOn.comp hT hmaps).const_mul _) |>.add\n    (contDiffOn_L1.continuousOn.comp hT hmaps).const_mul _) |>.add\n    (contDiffOn_L2.continuousOn.comp hT hmaps).const_mul _) |>.add\n    ((by rw [hId]; exact (psiTilde_contDiff.continuous.continuousOn).comp hsqrt\n      (Set.mapsTo_univ _ _) : ContinuousOn IIMaj (Set.Ici 20)).const_mul (-1))) |>.add\n    continuousOn_const\n\n/-- [PROVED session 011] The full margin is C\u00b2 on (20, \u221e). -/"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\paper\\cover-letter.md",
  "oldString": "The 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,",
  "newString": "The 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 (Johansson's rigorous interval-arithmetic\ntable of the ordinary \u03bb_n to n = 10\u2075; this project to n = 3000, by two\nindependent methods agreeing to 4.8\u00d710\u207b\u00b2\u2075 relative). By Voros's\nsharpening, positivity of all sufficiently large \u03bb_n would itself\nimply RH, so no result short of RH can assert an infinite positive\ntail; an explicit finite-height statement is the natural form of\npartial progress on this route. To our knowledge this is the first\nexplicit, machine-verified assembly of the full chain \u2014 Lagarias's\ncontour argument with Trudgian's explicit zero-counting bounds, an\nelementary archimedean lower bound,",
  "originalFile": "# 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": [
    {
      "oldStart": 26,
      "oldLines": 13,
      "newStart": 26,
      "newLines": 16,
      "lines": [
        " \u03be-function satisfy \u03bb_n > 0 for all 1 \u2264 n \u2264 (T\u2080\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074,",
        " conditional on the interval-arithmetic verification of the Riemann",
        " hypothesis to height T\u2080 = 3\u00d710\u00b9\u00b2 (Platt\u2013Trudgian) and on finite",
        "-Li-coefficient computations (this project to n = 3000, by two",
        "-independent methods agreeing to 4.8\u00d710\u207b\u00b2\u2075 relative; Misguich\u2013Voros to",
        "-n = 5\u00d710\u2075). 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 \u2014 Lagarias's contour argument with Trudgian's",
        "-explicit zero-counting bounds, an elementary archimedean lower bound,",
        "+Li-coefficient computations (Johansson's rigorous interval-arithmetic",
        "+table of the ordinary \u03bb_n to n = 10\u2075; this project to n = 3000, by two",
        "+independent methods agreeing to 4.8\u00d710\u207b\u00b2\u2075 relative). By Voros's",
        "+sharpening, positivity of all sufficiently large \u03bb_n would itself",
        "+imply RH, so no result short of RH can assert an infinite positive",
        "+tail; an explicit finite-height statement is the natural form of",
        "+partial progress on this route. To our knowledge this is the first",
        "+explicit, machine-verified assembly of the full chain \u2014 Lagarias's",
        "+contour argument with Trudgian's explicit zero-counting bounds, an",
        "+elementary archimedean lower bound,",
        " a proved margin convexity, and the finite verifications \u2014 has been",
        " assembled with every constant traced.",
        " "
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}