GPPVerify: Lean 4 Formalization of the ONON Framework

3 Functional Equation

3.1 Completed Riemann Zeta Function

Definition 3.1 Riemann Xi Function
#

\(\xi (s) = \tfrac {1}{2} s(s-1) \pi ^{-s/2} \Gamma (s/2) \zeta (s)\).

Theorem 3.2 Tate Functional Equation
#

For any Schwartz-Bruhat function \(\Phi \) on \(\mathbb {A}\): \(Z(\Phi , s) = Z(\hat\Phi , 1-s)\). Follows from Haar self-duality + Poisson summation over \(\mathbb {Q} \subset \mathbb {A}\).

Theorem 3.3 Functional Equation \(\xi (s) = \xi (1-s)\)
#

\(\xi (s) = \xi (1-s)\) for all \(s \in \mathbb {C}\) away from poles. This is the arithmetic shadow symmetry.

Lemma 3.4 Zeros Are Symmetric
#

If \(\xi (\rho ) = 0\) then \(\xi (1-\rho ) = 0\).

Lemma 3.5 Critical Line is Fixed Locus
#

\(s = 1-s \iff \mathrm{Re}(s) = \tfrac {1}{2}\).