Key Identity: ξ(s) = (1/2) s(s-1) Λ(s)

We prove that our definition of ξ using Λ₀ is equivalent to the standard definition using Λ = completedRiemannZeta.

The relationship is: Λ₀(s) = Λ(s) + 1/s + 1/(1-s)

Substituting: ξ(s) = (1/2) s(s-1) Λ₀(s) + 1/2 = (1/2) s(s-1) [Λ(s) + 1/s + 1/(1-s)] + 1/2 = (1/2) s(s-1) Λ(s) + (1/2)(s-1) - (1/2)s + 1/2 = (1/2) s(s-1) Λ(s) + 0 = (1/2) s(s-1) Λ(s)

def XiZeros.NontrivialZero : Type

Nontrivial zeros of ζ: zeros in the critical strip 0 < Re(s) < 1

Equations

• XiZeros.NontrivialZero = { ρ : ℂ // riemannZeta ρ = 0 ∧ 0 < ρ.re ∧ ρ.re < 1 }

noncomputable def XiZeros.riemannXi (s : ℂ) : ℂ

Definition of ξ (matching LiCriterion.lean)

Equations

• XiZeros.riemannXi s = 1 / 2 * s * (s - 1) * completedRiemannZeta₀ s + 1 / 2

theorem XiZeros.xi_eq_half_s_sm1_Lambda {s : ℂ} (hs0 : s ≠ 0) (hs1 : s ≠ 1) : riemannXi s = 1 / 2 * s * (s - 1) * completedRiemannZeta s

ξ(s) equals (1/2) s(s-1) Λ(s) when s ≠ 0 and s ≠ 1.

This is the standard form of the xi function.

theorem XiZeros.xi_ne_zero_at_trivial_points : riemannXi 0 ≠ 0 ∧ riemannXi 1 ≠ 0

ξ has no zeros at s=0 or s=1

Zeros of ξ in the Critical Strip

In the critical strip 0 < Re(s) < 1:

• s ≠ 0 and s ≠ 1, so s(s-1) ≠ 0
• ξ(s) = (1/2) s(s-1) Λ(s), so ξ(s) = 0 ↔ Λ(s) = 0

And Λ(s) = π^(-s/2) Γ(s/2) ζ(s) where:

• π^(-s/2) ≠ 0 always (exponential)
• Γ(s/2) ≠ 0 for Re(s/2) > 0, i.e., Re(s) > 0 (Γ has no zeros, only poles at ≤ 0)

Therefore: ξ(s) = 0 ↔ ζ(s) = 0 in the critical strip.

theorem XiZeros.zeta_zero_implies_Lambda_zero {s : ℂ} (hs_re_pos : 0 < s.re) (_hs_re_lt : s.re < 1) (hzeta : riemannZeta s = 0) : completedRiemannZeta s = 0

In the critical strip, ζ(s) = 0 implies Λ(s) = 0.

theorem XiZeros.Lambda_zero_implies_zeta_zero {s : ℂ} (_hs_re_pos : 0 < s.re) (_hs_re_lt : s.re < 1) (hs0 : s ≠ 0) (_hs1 : s ≠ 1) (hLambda : completedRiemannZeta s = 0) : riemannZeta s = 0

In the critical strip, Λ(s) = 0 implies ζ(s) = 0.

theorem XiZeros.mul_eq_zero_of_ne_zero_left {a b : ℂ} (ha : a ≠ 0) (hab : a * b = 0) : b = 0

If a product is zero and the first factor is nonzero, then the second factor is zero.

theorem XiZeros.xi_zeros_are_nontrivial_zeros (s : ℂ) : riemannXi s = 0 ↔ ∃ (ρ : NontrivialZero), s = ↑ρ

AXIOM 1: Zeros of ξ are exactly nontrivial zeros of ζ