The vocabulary of the main results

Every notion appearing in the statements of the headline theorems: the zero counts, the Hilbert-space objects of the key proposition, the pair-correlation apparatus, and the two classical analytic inputs.

These are kept in one module, in the order Challenge/Basic.lean repeats them, and should stay that way. Elaboration lifts a nested proof out of a definition's body into an auxiliary theorem named after whichever definition in the module first needed it, so splitting these across modules gives them names a single self-contained file cannot reproduce.

def ZetaZeros.nontrivialZeros (T : ℝ) : Set ℂ

The non-trivial zeros of the Riemann zeta function with imaginary part in (0, T]: the zeros lying in the critical strip 0 < re s < 1, as a set, so without multiplicity.

Equations

• ZetaZeros.nontrivialZeros T = {ρ : ℂ | riemannZeta ρ = 0 ∧ 0 < ρ.re ∧ ρ.re < 1 ∧ 0 < ρ.im ∧ ρ.im ≤ T}

noncomputable def ZetaZeros.zeroMultiplicity (ρ : ℂ) : ℕ

The multiplicity of ρ as a zero of the Riemann zeta function, i.e. its order of vanishing there.

Equations

• ZetaZeros.zeroMultiplicity ρ = analyticOrderNatAt riemannZeta ρ

noncomputable def ZetaZeros.zeroCount (T : ℝ) : ℕ

The number of non-trivial zeros with imaginary part in (0, T], counted with multiplicity. This is N T in the source.

Equations

• ZetaZeros.zeroCount T = ∑ᶠ (ρ : ℂ) (_ : ρ ∈ ZetaZeros.nontrivialZeros T), ZetaZeros.zeroMultiplicity ρ

noncomputable def ZetaZeros.simpleOnLineCount (T : ℝ) : ℕ

The number of non-trivial zeros with imaginary part in (0, T] that are simple and lie on the critical line re s = 1/2. This is N₀ˢ T in the source.

Equations

• ZetaZeros.simpleOnLineCount T = {ρ : ℂ | ρ ∈ ZetaZeros.nontrivialZeros T ∧ ρ.re = 1 / 2 ∧ ZetaZeros.zeroMultiplicity ρ = 1}.ncard

noncomputable def ZetaZeros.distinctZeroCount (T : ℝ) : ℕ

The number of distinct non-trivial zeros with imaginary part in (0, T]. This is N_d T in the source.

Equations

• ZetaZeros.distinctZeroCount T = (ZetaZeros.nontrivialZeros T).ncard

noncomputable def ZetaZeros.fourierC (f : ℝ → ℝ) (ξ : ℂ) : ℂ

The Fourier transform of a compactly supported real function, at a complex argument.

Equations

• ZetaZeros.fourierC f ξ = ∫ (u : ℝ), ↑(f u) * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ξ * ↑u)

structure ZetaZeros.IsAdmissible (lam : ℝ) (eta : ℝ → ℝ) : Prop

eta is lam-admissible: square-integrable, real-valued, even, supported in (-lam, lam), and normalised so that its square has Fourier transform 1 at 0.

• memLp : MeasureTheory.MemLp eta 2 MeasureTheory.volume

  eta is square-integrable.

• even (x : ℝ) : eta (-x) = eta x

  eta is even.

• support (x : ℝ) : lam ≤ |x| → eta x = 0

  eta vanishes off (-lam, lam).

• fourier_sq_zero : fourierC (eta ^ 2) 0 = 1

  eta is normalised: its square has Fourier transform 1 at 0.

noncomputable def ZetaZeros.testKernel (eta : ℝ → ℝ) : ℂ → ℂ

The kernel of a test function, K_eta = fourier transform of eta squared.

Equations

• ZetaZeros.testKernel eta = ZetaZeros.fourierC (eta ^ 2)

structure ZetaZeros.IsConjInvariant (Z : Finset ℂ) (m : ℂ → ℕ) : Prop

The support Z with multiplicities m is conjugation-invariant: every multiplicity is at least one, and conjugation permutes Z preserving multiplicity.

• one_le (z : ℂ) : z ∈ Z → 1 ≤ m z

  Every point of the support has multiplicity at least one.

• conj_mem (z : ℂ) : z ∈ Z → (starRingEnd ℂ) z ∈ Z

  Conjugation maps the support to itself.

• mult_conj (z : ℂ) : z ∈ Z → m ((starRingEnd ℂ) z) = m z

  Conjugation preserves multiplicity.

noncomputable def ZetaZeros.simpleRealPart (Z : Finset ℂ) (m : ℂ → ℕ) : Finset ℂ

The simple real part of the support: real points of multiplicity one.

Equations

• ZetaZeros.simpleRealPart Z m = {x ∈ Z | x.im = 0 ∧ m x = 1}

noncomputable def ZetaZeros.pairWeight (z : ℂ) : ℂ

The weight 4 / (4 - z²) carried by the unconditional pair-correlation formula.

Equations

• ZetaZeros.pairWeight z = 4 / (4 - z ^ 2)

noncomputable def ZetaZeros.rescaledDiff (T : ℝ) (ρ ρ' : ℂ) : ℂ

The rescaled difference i(ρ - ρ') log T / (2π) of two zeros.

Equations

• ZetaZeros.rescaledDiff T ρ ρ' = Complex.I * (ρ - ρ') * ↑(Real.log T / (2 * Real.pi))

noncomputable def ZetaZeros.pairCorrelationSum (f : ℝ → ℝ) (T : ℝ) : ℂ

The weighted sum of fourierC f over ordered pairs of non-trivial zeros with imaginary part in (0, T], each zero counted with multiplicity.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ZetaZeros.pairMainTerm (f : ℝ → ℝ) : ℝ

The main term f 0 + 2 ∫₀¹ α f α of the pair-correlation formula.

Equations

• ZetaZeros.pairMainTerm f = f 0 + 2 * ∫ (α : ℝ) in 0..1, α * f α

def ZetaZeros.IsPairTestFunction (f : ℝ → ℝ) : Prop

A test function admissible in the pair-correlation formula: even, integrable, supported in [-1, 1], and Lipschitz at the origin.

The Lipschitz condition is imposed globally rather than only at 0. That makes this predicate stronger, hence PairCorrelation weaker and safer to assume — and the cited lemma still supplies it.

Equations

• One or more equations did not get rendered due to their size.

The two external inputs

The classical analytic results cited rather than proved here: the Riemann--von Mangoldt formula and the unconditional pair-correlation formula. Each is a Prop, carried as a hypothesis, so every result depending on it names it in its own statement.

def ZetaZeros.RiemannVonMangoldt : Prop

Riemann--von Mangoldt (lem_rvm, external input). N T ∼ (T / 2π) log T.

Equations

• ZetaZeros.RiemannVonMangoldt = ∀ ε > 0, ∃ (T₀ : ℝ), ∀ T ≥ T₀, |↑(ZetaZeros.zeroCount T) / (T / (2 * Real.pi) * Real.log T) - 1| < ε

def ZetaZeros.PairCorrelation : Prop

Unconditional pair correlation (lem_bgst, external input). For every admissible test function the weighted pair-correlation sum is (T / 2π) log T times its main term, with an error O(1 / √log T). Lemma 5 of Baluyot--Goldston--Suriajaya--Turnage-Butterbaugh, An unconditional Montgomery theorem for pair correlation of zeros of the Riemann zeta-function, Acta Arith. 214 (2024), 357--376.

Equations

• One or more equations did not get rendered due to their size.