Formal Verification — Lean 4

Axiom policy — the transparency guarantee

Every proved declaration in the chain depends on exactly the three standard axioms: propext, Classical.choice, Quot.sound — the same axioms any Mathlib proof uses. Zero sorryAx (no skipped proofs) anywhere in the proved chain; the 5 sorries below are confined to the two skeleton files (Suzuki / valley — future tiers, not used by the closed theorem). The audit transcripts at the bottom of this page are the raw #print axioms output verifying this, per declaration.

The closed theorem — LiClosed.lean (verbatim)

/-
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

The declared perimeter — 7 hypotheses

The theorem is conditional on these seven statements (two published computational certificates + five analytic perimeter Props from the declared literature). Each is shown verbatim from source; click to expand.

def RHUpTo (T₀ : ℝ) : Prop :=
  ∀ ρ : ℂ, IsNontrivialZero ρ → |ρ.im| ≤ T₀ → ρ.re = 1 / 2

def LiVerifiedUpTo (N : ℕ) : Prop :=
  ∀ n : ℕ, 1 ≤ n → n ≤ N → 0 < (liCoeff n).re

def ZeroCountProp : Prop :=
  ∀ t : ℝ, 2 ≤ t →
    (((zeroWindow_finite t).toFinset.sum fun ρ => zeroMult ρ) : ℝ) ≤ C0hat (t + 1)

def ZeroCountProp2 : Prop :=
  ∀ t : ℝ, 10 ≤ t →
    (((zeroAbsWindow_finite t).toFinset.sum fun ρ => zeroMult ρ) : ℝ) ≤
      0.6 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.7

def ZeroCountGlobalProp : Prop :=
  ∀ T : ℝ, 2 ≤ T →
    (((zeroGlobalWindow_finite T).toFinset.sum fun ρ => zeroMult ρ) : ℝ) ≤ FAlt T

def NoLowZeros : Prop :=
  ∀ ρ : ℂ, IsNontrivialZero ρ → 14 ≤ |ρ.im|

def MZeroProp : Prop :=
  ∀ t : ℝ, |t| ≤ 10 →
    ‖logDeriv riemannZeta ((-5 / 2 : ℂ) + (t : ℝ) * Complex.I)‖ ≤ 1.3352

Source files

Axiom audits (#print axioms transcripts)

The session-013 audit predates the tier-ii′ closure: its 5 sorryAx lines are the intended skeleton statements (1 Suzuki + 4 valley — future tiers, not used by the closed theorem). Every later audit is fully clean.