LiClosed.lean

Declarations

Source

/-
LiClosed.lean — tier ii′-7: THE CLOSED finite-height Li theorem (R-004
endpoint, D-062 §4). `lambda_pos_finite_height_closed`: λ_n > 0 for all
1 ≤ n ≤ N₁ = (3×10¹²−1)² ≈ 9×10²⁴ from the SEVEN declared hypotheses:
the two computational certificates (Platt–Trudgian `RHUpTo`; the finite
Li verification `LiVerifiedUpTo` — E-011/E-015 to 3000 + Johansson 2015
§ 4.2 to 10⁵) and the five analytic perimeter Props (Trudgian N(T)/S(T):
`ZeroCountProp` unit-window, `ZeroCountProp2` two-unit,
`ZeroCountGlobalProp` global; the Platt-class zero-location certificate
`NoLowZeros`; the M₀ interval certificate `MZeroProp`) — the session-012
named analytic hypothesis `SfBoundProp` is now PROVED (tier ii′-6,
LiSideBounds).
-/
import Mathlib
import NguyenRH1.LiBasePoints
import NguyenRH1.LiSideBounds

open Zeta23 Complex Filter Topology

namespace NguyenRH1

/-- **THE CLOSED FINITE-HEIGHT LI THEOREM** (R-004, ii′-7 endpoint):
λ_n > 0 for ALL 1 ≤ n ≤ N₁ = (3×10¹²−1)² ≈ 9×10²⁴, from the SEVEN
declared hypotheses (two computational certificates + five analytic
perimeter Props). The session-012 named analytic hypothesis
`SfBoundProp` is discharged by ii′-6's `sfBoundProp`. -/
theorem lambda_pos_finite_height_closed
    (hRH : RHUpTo (3 * 10 ^ 12)) (hfinite : LiVerifiedUpTo (10 ^ 5))
    (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2) (hZCG : ZeroCountGlobalProp)
    (hNLZ : NoLowZeros) (hMZ : MZeroProp) :
    ∀ n : ℕ, 1 ≤ n → (n : ℝ) ≤ (3 * 10 ^ 12 - 1 : ℝ) ^ 2 →
      0 < (liCoeff n).re :=
  lambda_pos_finite_height_verified hRH hfinite
    (sfBoundProp hRH hZC hZC2 hZCG hNLZ hMZ)

end NguyenRH1