This module defines the vocabulary of the two proved statements in LeanPool.LiCriterion.Comparator.Solution, using Mathlib alone. Mathlib's RiemannHypothesis supplies the RH side; the xi function and its analytic coefficients are defined below.

The definitions have the same bodies as their counterparts in Lc/LiCriterion/Basic.lean, so the solution can delegate to the library by definitional unfolding. Their separate LiChallenge namespace lets the solution import both copies without name clashes.

For the local statements and proofs, read Comparator/Solution.lean together with these definitions. The independent upstream statement and its comparator procedure are preserved at the pinned Challenge and audit guide. Those upstream audit assets are separate from this Lean Pool import.

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

The Riemann ξ function in entire form: ξ(s) = ½ · s · (s-1) · Λ₀(s) + ½, where Λ₀ = completedRiemannZeta₀ is Mathlib's entire completed zeta. This is an entire function whose zeros in the critical strip are exactly the nontrivial zeros of ζ. (Character-for-character LiCriterion.riemannXi.)

Equations

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

noncomputable def LiChallenge.phi (f : ℂ → ℂ) (z : ℂ) : ℂ

The Cayley-type change of variable z ↦ 1/(1-z), which carries the open unit disk onto the half-plane Re s > 1/2. Precomposing with it turns "all zeros on the critical line" into a statement about the unit disk, which is what makes the Li coefficients a positivity condition. (Character-for-character LiCriterion.phi.)

Equations

• LiChallenge.phi f z = f (1 / (1 - z))

noncomputable def LiChallenge.logDeriv (φ : ℂ → ℂ) (z : ℂ) : ℂ

The logarithmic derivative f' / f. (Character-for-character LiCriterion.logDeriv.)

Equations

• LiChallenge.logDeriv φ z = deriv φ z / φ z

noncomputable def LiChallenge.taylorCoeff (f : ℂ → ℂ) (n : ℕ) : ℂ

The zero-indexed analytic coefficient corresponding, for f = riemannXi, to Li's classical λ_{n+1}: the n-th Taylor coefficient at 0 of the logarithmic derivative of f precomposed with the Cayley map. These are the coefficients whose nonnegativity is Li's criterion for RH. (Character-for-character LiCriterion.taylorCoeff.)

Equations

• LiChallenge.taylorCoeff f n = deriv^[n] (LiChallenge.logDeriv (LiChallenge.phi f)) 0 / ↑n.factorial

def LiChallenge.NontrivialZero : Type

The nontrivial zeros of ζ: the zeros in the open critical strip 0 < re s < 1. (Character-for-character LiCriterion.NontrivialZero.)

Equations

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