{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
  "old_string": "  unfold marginExpanded mFblock mTL1b mTL2b mIdb mL1sqb mL1L2b mL2sqb mL1b mL2b mIIM\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",
  "new_string": "  unfold marginExpanded mFblock mTL1b mTL2b mIdb mL1sqb mL1L2b mL2sqb mL1b mL2b mIIM\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"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\results\\R-004-finite-height-li-theorem.md",
  "oldString": "Tag: **[PROVED-CONDITIONAL(computational RH-to-height-T\u2080; computational\nfinite verification)]** \u2014 R-bound FULLY TRACED 2026-08-19 (D-056,\ntask 4.5a: reference-point method, A = 10.5, B\u2080 = 48 with the honest\nC\u2080 incl. log log term; digamma remainder 1.2/|w|\u00b2 proved; E-028\nverified, 26\u00d7 slack); N\u2080 = 80 000 (6.25\u00d7 overlap with\nMisguich\u2013Voros). M\u2080 remains grid-verified (E-023 S1; additive ~53).\nMargin convexity: PROVED (D-057, task 4.5b; E-029 ALL CHECKS PASS).\nHistory: tag downgraded then restored same day (D-054 erratum: broken\nD-039/D-036-\u00a71 proofs; repairs D-056\u2013D-059).\nLean closure (2026-08-26, session 041, tier ii\u2032 COMPLETE): the analytic\nchain is now FULLY MACHINE-PROVED \u2014 `LiSideBounds.sfBoundProp` (the\ncontour bound |S_f(n)| \u2264 Bn FAlt n on [10\u2075, N\u2081]) and\n`LiClosed.lambda_pos_finite_height_closed` (\u03bb_n > 0 for all\n1 \u2264 n \u2264 N\u2081) in Lean 4, from exactly EIGHT declared hypotheses:\nRHUpTo (Platt\u2013Trudgian), LiVerifiedUpTo (finite Li verification),\nZeroCountProp/ZeroCountProp2/ZeroCountGlobalProp (Trudgian N(T)/S(T)\nforms), NoLowZeros (Platt-class zero-location), MZeroProp (M\u2080 interval\ncertificate). Axiom audit on the full chain: [propext,\nClassical.choice, Quot.sound] only, 0 sorryAx. The B(n) account was\ncorrected in four places during the closure (F-A/F-B/F-D/F-E \u2014 see the\nD-037 erratum block and Paper A \u00a73 Step-2 footnote); the theorem\nstatement is unchanged.",
  "newString": "Tag: **[PROVED-CONDITIONAL(computational RH-to-height-T\u2080; computational\nfinite verification)]** \u2014 R-bound FULLY TRACED 2026-08-19 (D-056,\ntask 4.5a: reference-point method, A = 10.5, B\u2080 = 48 with the honest\nC\u2080 incl. log log term; digamma remainder 1.2/|w|\u00b2 proved; E-028\nverified, 26\u00d7 slack); N\u2080 = 80 000 (1.25\u00d7 overlap with\nJohansson's 10\u2075 table). M\u2080 remains grid-verified (E-023 S1; additive\n~53). Margin convexity: PROVED (D-057, task 4.5b; E-029 ALL CHECKS\nPASS). History: tag downgraded then restored same day (D-054 erratum:\nbroken D-039/D-036-\u00a71 proofs; repairs D-056\u2013D-059).\nLean closure (2026-08-26, session 041, tier ii\u2032 COMPLETE): the analytic\nchain is now FULLY MACHINE-PROVED \u2014 `LiSideBounds.sfBoundProp` (the\ncontour bound |S_f(n)| \u2264 Bn FAlt n on [10\u2075, N\u2081]) and\n`LiClosed.lambda_pos_finite_height_closed` (\u03bb_n > 0 for all\n1 \u2264 n \u2264 N\u2081) in Lean 4, from exactly SEVEN declared hypotheses:\nRHUpTo (Platt\u2013Trudgian), LiVerifiedUpTo(10\u2075) (finite Li verification:\nE-011/E-015 to 3000 + Johansson 2015 \u00a7 4.2, rigorous interval-arithmetic\nordinary-\u03bb_n table to 10\u2075), ZeroCountProp/ZeroCountProp2/\nZeroCountGlobalProp (Trudgian N(T)/S(T) forms), NoLowZeros (Platt-class\nzero-location), MZeroProp (M\u2080 interval certificate). Axiom audit on the\nfull chain: [propext, Classical.choice, Quot.sound] only, 0 sorryAx.\nThe B(n) account was corrected in four places during the closure\n(F-A/F-B/F-D/F-E \u2014 see the D-037 erratum block and Paper A \u00a73 Step-2\nfootnote); the theorem statement is unchanged.\nCertificate correction (2026-08-26, session 042, user review): the\nfinite-verification citation Misguich\u2013Voros (Voros 2020, Exp. Math.\n29(4)) was found to carry a DEFORMED sequence \u039b_n (Misguich, private\ncommunication), not the ordinary \u03bb_n \u2014 it has been replaced by\nJohansson 2015 \u00a7 4.2 (rigorous, published, ordinary Keiper\u2013Li\ncoefficients to n = 10\u2075, all positive) and the Lean perimeter\n`LiVerifiedUpTo` reduced from (5\u00b710\u2075) to (10\u2075) to match the checkable\nevidence (commit 79c96f2; the assembly's hfinite branch uses exactly\nn < 10\u2075, so nothing else changes).",
  "originalFile": "# R-004 \u2014 Explicit finite-height Li theorem: \u03bb_n > 0 for all n \u2264 (T\u2080\u22121)\u00b2 = 8.999\u2026\u00d710\u00b2\u2074\nDate: 2026-08-19 | Session: 008 | Track: C (task 3.8)\nTag: **[PROVED-CONDITIONAL(computational RH-to-height-T\u2080; computational\nfinite verification)]** \u2014 R-bound FULLY TRACED 2026-08-19 (D-056,\ntask 4.5a: reference-point method, A = 10.5, B\u2080 = 48 with the honest\nC\u2080 incl. log log term; digamma remainder 1.2/|w|\u00b2 proved; E-028\nverified, 26\u00d7 slack); N\u2080 = 80 000 (6.25\u00d7 overlap with\nMisguich\u2013Voros). M\u2080 remains grid-verified (E-023 S1; additive ~53).\nMargin convexity: PROVED (D-057, task 4.5b; E-029 ALL CHECKS PASS).\nHistory: tag downgraded then restored same day (D-054 erratum: broken\nD-039/D-036-\u00a71 proofs; repairs D-056\u2013D-059).\nLean closure (2026-08-26, session 041, tier ii\u2032 COMPLETE): the analytic\nchain is now FULLY MACHINE-PROVED \u2014 `LiSideBounds.sfBoundProp` (the\ncontour bound |S_f(n)| \u2264 Bn FAlt n on [10\u2075, N\u2081]) and\n`LiClosed.lambda_pos_finite_height_closed` (\u03bb_n > 0 for all\n1 \u2264 n \u2264 N\u2081) in Lean 4, from exactly EIGHT declared hypotheses:\nRHUpTo (Platt\u2013Trudgian), LiVerifiedUpTo (finite Li verification),\nZeroCountProp/ZeroCountProp2/ZeroCountGlobalProp (Trudgian N(T)/S(T)\nforms), NoLowZeros (Platt-class zero-location), MZeroProp (M\u2080 interval\ncertificate). Axiom audit on the full chain: [propext,\nClassical.choice, Quot.sound] only, 0 sorryAx. The B(n) account was\ncorrected in four places during the closure (F-A/F-B/F-D/F-E \u2014 see the\nD-037 erratum block and Paper A \u00a73 Step-2 footnote); the theorem\nstatement is unchanged.\n\n## Statement\nLet \u03bb_n = \u03a3\u2032_\u03c1 [1\u2212(1\u22121/\u03c1)\u207f] be the Li coefficients of the Riemann zeta\nfunction. Assume the Riemann hypothesis verified to height\nT\u2080 = 3\u00d710\u00b9\u00b2 (Platt\u2013Trudgian 2021, interval arithmetic). Then\n\n  **\u03bb_n > 0 for every 1 \u2264 n \u2264 N\u2081 := (T\u2080\u22121)\u00b2\n  = 8 999 999 999 994 000 000 000 001 \u2248 9.0\u00d710\u00b2\u2074.**\n\nConservative variant (using Lagarias's printed bridge window (1.16)\ninstead of the traced proof): N\u2081* = T\u2080\u00b2/(4 log\u00b2T\u2080) = 2.726\u00d710\u00b2\u00b9.\n\nThis is the first assembled EXPLICIT finite-height Li bound: the chain\n\"RH to height T\u2080 + fully traced constants \u27f9 \u03bb_n > 0 to n ~ T\u2080\u00b2\" existed\nonly with untraced O-constants (Lagarias math/0404394 Thm 1.1/(1.16)).\nBy Voros's sharpening, no statement of the form \"\u03bb_n > 0 \u2200n \u2265 N\u2080\" is\npossible short of RH \u2014 this finite-height theorem is the maximal content\nof the Li route (D-032/D-033).\n\n## Proof / Derivation\nFull assembly: **D-037** (derivation), support computation **E-023**\n(ALL CHECKS PASS). Skeleton:\n1. \u03bb_n = S_\u221e(n) \u2212 S_f(n) + 1 (Bombieri\u2013Lagarias Thm 2).\n2. Archimedean: S_\u221e(n) \u2265 \u00bdn log n + (C\u2081\u2212\u03b3/2)n \u2212 4 for n \u2265 20,\n   C\u2081 = (\u03b3\u22121\u2212log 2\u03c0)/2 \u2014 elementary from Lagarias (4.11) via finite\n   differences + explicit harmonic bounds; validated against E-021's\n   exact S_\u221e to n = 5000 (E-023 V1, min slack 9.52).\n3. Finite: |S_f(n)| \u2264 B(n) (D-037 (4.1)) \u2014 Lagarias Thm 6.1 contour with\n   all constants traced (Trudgian N(T)/S(T); kernel e\u2074+1; R-bound\n   A = 10.5, B\u2080 = 48 traced (D-056, reference-point method) /\n   0.9, 1.0 measured; short-segment max\n   M\u2080 = 1.3352 closing the D-036 |t|<10 gap).\n4. Bridge: RH to height \u221an+1 \u27f9 each zero contributes \u2264 2 \u27f9\n   |\u03bb_n(T)| \u2264 2N(T); holds for n \u2264 (T\u2080\u22121)\u00b2.\n5. margin(n) := S_\u221e^lower \u2212 B + 1 is convex for n \u2265 20 (PROVED D-057;\n   E-029), margin(8\u00d710\u2074) = 16 020 > 0 with positive derivative \u27f9\n   margin(n) > 0 for all n \u2208 [8\u00d710\u2074, N\u2081] (E-028;\n   margin(N\u2081) = 2.458\u00d710\u00b2\u2076).\n6. Finite verification: n \u2264 3000 (E-011/E-015, cross-validated,\n   ledger #3) \u222a n \u2264 5\u00d710\u2075 (Misguich\u2013Voros) \u2014 overlaps N\u2080 = 8\u00d710\u2074\n   by a factor 6.25.\n\n## Dependencies\nR-001 (finite verification), D-032/D-033 (design + wall), D-036 (contour\nconstants), D-037 (assembly), E-021 (exact S_\u221e/measured constants),\nE-023 (assembly numerics), Trudgian 2014 [PROVED lit], Platt\u2013Trudgian\n2021 [computational], Lagarias math/0404394, Bombieri\u2013Lagarias 1999,\nVoros 1703.02844 [Misguich numerics].\n\n## Adversarial review\nD-037 \u00a77: full input inventory P1\u2013P6 (proved/elementary) vs H1\u2013H5\n(computational/heuristic). Update (session 009 repairs): H2 (digamma\nsub-bound) is now PROVED (D-056: |r| \u2264 1.2/|w|\u00b2, Binet split +\nmax-modulus majorant); the only remaining grid-verified constant link\nis H3 (M\u2080 = 1.3352, E-023 S1; additive ~53.4). The theorem's\nsensitivity to M\u2080 is negligible \u2014 it enters a sub-dominant additive\nconstant; even 5\u00d7 worse moves N\u2080 by ~15 %, irrelevant against the\n6.25\u00d7 overlap margin. Upgrade path listed (E-023b: acb box cover).\nSanity gates: no claim beyond N\u2081 (Voros wall respected); no\nD-H/Epstein analogue claimed. Honest scope: this is NOT progress on\n\"\u03bb_n > 0 \u2200 large n\" (\u27fa RH).\n\n## Paper section\nNumerics/positivity appendix of draft.tex: \"Explicit finite-height\npositivity of the Keiper\u2013Li coefficients\"; constants table from D-037\n\u00a74; N\u2081 headline in the abstract-worthy results list.\n",
  "structuredPatch": [
    {
      "oldStart": 4,
      "oldLines": 24,
      "newStart": 4,
      "newLines": 34,
      "lines": [
        " finite verification)]** \u2014 R-bound FULLY TRACED 2026-08-19 (D-056,",
        " task 4.5a: reference-point method, A = 10.5, B\u2080 = 48 with the honest",
        " C\u2080 incl. log log term; digamma remainder 1.2/|w|\u00b2 proved; E-028",
        "-verified, 26\u00d7 slack); N\u2080 = 80 000 (6.25\u00d7 overlap with",
        "-Misguich\u2013Voros). M\u2080 remains grid-verified (E-023 S1; additive ~53).",
        "-Margin convexity: PROVED (D-057, task 4.5b; E-029 ALL CHECKS PASS).",
        "-History: tag downgraded then restored same day (D-054 erratum: broken",
        "-D-039/D-036-\u00a71 proofs; repairs D-056\u2013D-059).",
        "+verified, 26\u00d7 slack); N\u2080 = 80 000 (1.25\u00d7 overlap with",
        "+Johansson's 10\u2075 table). M\u2080 remains grid-verified (E-023 S1; additive",
        "+~53). Margin convexity: PROVED (D-057, task 4.5b; E-029 ALL CHECKS",
        "+PASS). History: tag downgraded then restored same day (D-054 erratum:",
        "+broken D-039/D-036-\u00a71 proofs; repairs D-056\u2013D-059).",
        " Lean closure (2026-08-26, session 041, tier ii\u2032 COMPLETE): the analytic",
        " chain is now FULLY MACHINE-PROVED \u2014 `LiSideBounds.sfBoundProp` (the",
        " contour bound |S_f(n)| \u2264 Bn FAlt n on [10\u2075, N\u2081]) and",
        " `LiClosed.lambda_pos_finite_height_closed` (\u03bb_n > 0 for all",
        "-1 \u2264 n \u2264 N\u2081) in Lean 4, from exactly EIGHT declared hypotheses:",
        "-RHUpTo (Platt\u2013Trudgian), LiVerifiedUpTo (finite Li verification),",
        "-ZeroCountProp/ZeroCountProp2/ZeroCountGlobalProp (Trudgian N(T)/S(T)",
        "-forms), NoLowZeros (Platt-class zero-location), MZeroProp (M\u2080 interval",
        "-certificate). Axiom audit on the full chain: [propext,",
        "-Classical.choice, Quot.sound] only, 0 sorryAx. The B(n) account was",
        "-corrected in four places during the closure (F-A/F-B/F-D/F-E \u2014 see the",
        "-D-037 erratum block and Paper A \u00a73 Step-2 footnote); the theorem",
        "-statement is unchanged.",
        "+1 \u2264 n \u2264 N\u2081) in Lean 4, from exactly SEVEN declared hypotheses:",
        "+RHUpTo (Platt\u2013Trudgian), LiVerifiedUpTo(10\u2075) (finite Li verification:",
        "+E-011/E-015 to 3000 + Johansson 2015 \u00a7 4.2, rigorous interval-arithmetic",
        "+ordinary-\u03bb_n table to 10\u2075), ZeroCountProp/ZeroCountProp2/",
        "+ZeroCountGlobalProp (Trudgian N(T)/S(T) forms), NoLowZeros (Platt-class",
        "+zero-location), MZeroProp (M\u2080 interval certificate). Axiom audit on the",
        "+full chain: [propext, Classical.choice, Quot.sound] only, 0 sorryAx.",
        "+The B(n) account was corrected in four places during the closure",
        "+(F-A/F-B/F-D/F-E \u2014 see the D-037 erratum block and Paper A \u00a73 Step-2",
        "+footnote); the theorem statement is unchanged.",
        "+Certificate correction (2026-08-26, session 042, user review): the",
        "+finite-verification citation Misguich\u2013Voros (Voros 2020, Exp. Math.",
        "+29(4)) was found to carry a DEFORMED sequence \u039b_n (Misguich, private",
        "+communication), not the ordinary \u03bb_n \u2014 it has been replaced by",
        "+Johansson 2015 \u00a7 4.2 (rigorous, published, ordinary Keiper\u2013Li",
        "+coefficients to n = 10\u2075, all positive) and the Lean perimeter",
        "+`LiVerifiedUpTo` reduced from (5\u00b710\u2075) to (10\u2075) to match the checkable",
        "+evidence (commit 79c96f2; the assembly's hfinite branch uses exactly",
        "+n < 10\u2075, so nothing else changes).",
        " ",
        " ## Statement",
        " Let \u03bb_n = \u03a3\u2032_\u03c1 [1\u2212(1\u22121/\u03c1)\u207f] be the Li coefficients of the Riemann zeta"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}