Weil Positivity Criterion

Stream: maths

[Swami Kevala]

Hi,

New member here! I'm a beginner in Lean. I'm exploring using AI for a few ideas and I wanted a proper (human validated) formalization of the Weil Positivity Criterion (to RH) but I couldn't find anything in the existing Mathlib.

I came up with something and wanted to know if I'm using the appropriate level of abstraction, and if this is correctly formulated. (I want to explore equivalences to other criteria).

Thanks!

import Mathlib.NumberTheory.LSeries.RiemannZeta
import Mathlib.Data.Complex.Basic
import Mathlib.Algebra.Star.Basic

open Complex Function

/-!
# Abstract Interface for Weil's Positivity Criterion (WPC)
This interface defines the components of WPC abstractly using opaque types,
isolating the structural properties from the analytical details.
-/

namespace WPCInterface

noncomputable section

/-! ## Abstract Components -/

/-- Class of admissible test functions (Weil tests). Abstractly represents C_c^∞((0, ∞); ℂ). -/
opaque IsWeilTestFunction : (ℝ → ℂ) → Prop

/-- The set of nontrivial zeros of ζ as an abstract index type. -/
opaque NonTrivialZero : Type

/-- Coercion giving the complex value of a zero. -/
opaque zval : NonTrivialZero → ℂ

/-- The Mellin transform symbol. -/
opaque Mellin : (ℝ → ℂ) → (ℂ → ℂ)

/-- Abstract "sum over nontrivial zeros". Think: `∑_{ρ} F(ρ)`. Implicitly handles summability. -/
opaque ZeroSum : (NonTrivialZero → ℂ) → ℂ

/-! ## Definitions -/

/-- The Hermitian kernel `Φ_g(s) = Mellin(g,s) * Mellin(g̅, 1 - s)`. -/
def Phi (g : ℝ → ℂ) (s : ℂ) : ℂ :=
  Mellin g s * Mellin (star g) (1 - s)

/-- Weil functional `W(g) = Σ_ρ Φ_g(ρ)`. -/
def WeilFunctional (g : ℝ → ℂ) : ℂ :=
  ZeroSum (fun ρ : NonTrivialZero => Phi g (zval ρ))

/-- Weil Positivity Condition (WPC): positivity for all nonzero tests. -/
def WPC : Prop :=
  ∀ g : ℝ → ℂ, IsWeilTestFunction g → g ≠ 0 → 0 < (WeilFunctional g).re

/-! ## The Criterion Statement -/

/-- Weil's Criterion: RH ↔ WPC. We take this as the defining axiom connecting the interface to RH. -/
axiom WeilsCriterion : RiemannHypothesis ↔ WPC

end

end WPCInterface

[Matt Diamond]

A few points:

1) I wouldn't recommend writing opaque definitions. If you need temporary placeholders for certain functions that you'd prefer to define later, you can use sorry as the definition.

2) It's likely that some of these definitions are already in Mathlib (e.g. docs#mellin, docs#tsum). Others shouldn't be too hard to define... for example, here's one way to define NonTrivialZero:

def NonTrivialZero : Type := { s : ℂ // riemannZeta s = 0 ∧ (¬∃ (n : ℕ), s = -2 * (n + 1)) ∧ s ≠ 1 }

In this case, you wouldn't need zval... you could simply write ρ.val.

3) Don't define the criterion as an axiom. Rather, define it as a Prop, like so:

def WeilsCriterion : Prop := RiemannHypothesis ↔ WPC

If you want to assume it in a theorem, you can include it as an argument.

[Yan Yablonovskiy 🇺🇦]

Just out of curiosity, did you use any AI assistance for this? It is fine either way, but am curious.

[Matt Diamond]

he mentions AI in the third sentence so I assume it was involved somehow

[Yan Yablonovskiy 🇺🇦]

Matt Diamond said:

he mentions AI in the third sentence so I assume it was involved somehow

I was too busy looking for subtler signs in the code :face_in_clouds:

[Matt Diamond]

it happens!

[Swami Kevala]

Thanks @Matt Diamond that was helpful.

@Yan Yablonovskiy 🇺🇦 - Yes I used AI (GPT5) to generate the file, and did some minor tweaking