{
  "file_path": "D:\\Python\\Quantum\\research\\results\\R-004-finite-height-li-theorem.md",
  "offset": 1,
  "limit": 30
}

{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\Quantum\\research\\results\\R-004-finite-height-li-theorem.md",
    "content": "# 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",
    "numLines": 30,
    "startLine": 1,
    "totalLines": 90
  }
}