8 Connection to the Riemann zeta function

The connection with the zeta function has three logically distinct layers. First, standard analytic facts about the completed Riemann zeta function and its finite-prime logarithmic derivative are available in Mathlib and are proved in Lean. Second, Connes–Consani’s published distributional trace formula identifies a geometric counting distribution for the scaling flow. Third, turning the explicit formula into the positivity needed for the Riemann hypothesis remains an open mathematical and formalization frontier. None of these layers should be conflated.

8.1 Analytic statements proved in Lean

Definition 8.1 label=def:complete_riemann_zeta

✓

The completed Riemann zeta function used by the project is Mathlib’s meromorphically continued function \(\operatorname {completedRiemannZeta}\). Away from the poles of the Gamma factor it agrees with

\[ \zeta _{\mathbb {Q}}(s) =\pi ^{-s/2}\Gamma (s/2)\zeta (s). \]

Using the continued function, rather than a totalized pointwise product, preserves the pole–zero cancellations at non-positive even integers.

Theorem 8.2 label=thm:complete_zeta_functional_equation, uses=def:complete_riemann_zeta

✓

The completed zeta function satisfies

\[ \zeta _{\mathbb {Q}}(1-s)=\zeta _{\mathbb {Q}}(s). \]

Theorem 8.3 label=thm:complete_zeta_residue, uses=def:complete_riemann_zeta

✓

In Mathlib’s normalization, the residue at \(s=1\) is \(1\):

\[ \lim _{s\to 1}(s-1)\zeta _{\mathbb {Q}}(s)=1, \]

with the limit taken off the pole.

Theorem 8.4 label=thm:complete_zeta_differentiable, uses=def:complete_riemann_zeta

✓

The completed zeta function is differentiable at every \(s\ne 0,1\).

Definition 8.5 label=def:finite_place_mellin

✓

Define the finite-place Mellin transform to be the Dirichlet series of the von Mangoldt function,

\[ M_f(s):=\sum _{n\ge 1}\frac{\Lambda (n)}{n^s}. \]

In Lean this is expressed using Mathlib’s \(L\)-series. This definition records only finite-prime weights; it does not construct a fixed-point distribution on the Arithmetic Site.

Theorem 8.6 label=thm:finite_place_mellin, uses=def:finite_place_mellin

If \(\operatorname {Re}(s){\gt}1\), then

\[ M_f(s)=-\operatorname {logDeriv}(\zeta )(s) =-\frac{\zeta '(s)}{\zeta (s)}. \]

Proof ▶

This is Mathlib’s Dirichlet-series identity for the von Mangoldt function, rewritten using the project’s definition. The half-plane hypothesis supplies convergence and excludes zeros and the pole from the quotient in question.

Definition 8.7 label=def:completed_counting_mellin, uses=def:finite_place_mellin

✓

The completed analytic counting transform is

\[ M_{\mathrm{comp}}(s) :=M_f(s)-\operatorname {logDeriv}(\Gamma _{\mathbb {R}})(s), \]

where \(\Gamma _{\mathbb {R}}\) is Deligne’s real Gamma factor. This adds the archimedean analytic contribution, but by definition alone it does not construct a counting distribution.

Theorem 8.8 label=thm:completed_counting_mellin, uses=def:completed_counting_mellin, def:complete_riemann_zeta

If \(\operatorname {Re}(s){\gt}1\), then

\[ M_{\mathrm{comp}}(s) =-\operatorname {logDeriv}(\zeta _{\mathbb {Q}})(s). \]

Proof ▶

On the right half-plane Lean proves \(\zeta _{\mathbb {Q}}=\Gamma _{\mathbb {R}}\zeta \). The logarithmic derivative of this product, together with Theorem 8.6, gives the identity.

Remark 8.9

Theorem 8.6 is the finite-place analytic term only; Theorem 8.8 adds the archimedean Gamma contribution and identifies the resulting analytic expression with the completed logarithmic derivative. Neither theorem constructs a distributional trace, a geometric fixed-point count, or the claimed Hasse–Weil interpretation. The functional equation by itself likewise gives no proof of the Riemann hypothesis.

8.2 The published distributional counting formula

Let \(G=\mathbb {A}_{\mathbb {Q}}^\times /\mathbb {Q}^\times \) be the idèle class group and let \(\vartheta _u\xi (x)=\xi (u^{-1}x)\) denote its scaling representation on the relevant quotient of the adèle class space. In the published trace formula, the geometric side is schematically

\[ \operatorname {Tr}_{\mathrm{distr}} \! \left(\int _G h(u)\vartheta _u\, d^*u\right) =\sum _{v\in \Sigma _{\mathbb {Q}}} \int _{\mathbb {Q}_v^\times }^{\prime } \frac{h(u^{-1})}{|1-u|_v}\, d^*u. \]

The prime is essential: the local expression at \(u=1\) is a normalized principal-value distribution, not an ordinary absolutely convergent integral. Haar measures, additive characters, and the normalization of the principal value must be fixed compatibly. The resulting “counting function” \(N(u)\) is therefore a distribution paired with test functions, not a pointwise finite cardinality of fixed points.

Theorem 8.10 label=thm:zeta_counting, uses=thm:frobenius_are_correspondences

With the normalizations of Connes–Consani, the zeta function \(\zeta _N\) associated to the published counting distribution by the prescribed distributional Mellin relation

\[ \frac{\partial _s\zeta _N(s)}{\zeta _N(s)} =-\int _1^\infty N(u)u^{-s}\, d^*u \]

is the completed Riemann zeta function \(\zeta _{\mathbb {Q}}(s)=\pi ^{-s/2}\Gamma (s/2)\zeta (s)\). The integral notation denotes the distributional pairing and its stated regularization, not an ordinary integral of a pointwise function.

Proof ▶

This is the published counting-distribution result summarized as Theorem 2.7 of Connes–Consani (2014), using their preceding distributional trace formula and earlier computation of the counting distribution. Since a logarithmic derivative determines a meromorphic function only up to a nonzero multiplicative constant, the stated exact equality also uses their chosen normalization.

Formalization status. The project has not yet defined \(N\) as a distribution, formalized the principal-value local terms or the global trace formula, or proved that their Mellin transform equals completeRiemannZeta. Thus this published theorem deliberately has no Lean declaration link. Theorem 8.8 is a rigorous analytic bridge, not a construction or identification of the geometric distribution appearing here.

8.3 The Riemann-hypothesis frontier

Definition 8.11 label=def:riemann_hypothesis

✓

The project exposes ArithmeticSite.RiemannHypothesis as an alias for Mathlib’s standard proposition asserting that the non-trivial zeros of the Riemann zeta function lie on the critical line. The Lean marker here certifies only that this target proposition is defined; it does not provide a term proving it.

Remark 8.12

No theorem in this repository proves the Riemann hypothesis, and the published Arithmetic-Site results quoted above do not themselves prove it. The present formal frontier consists of several substantial steps:

prove the classification of flat \(\mathbb {N}^{\times }\)-actions by ordered subgroups and finite adèle classes;
construct reduced correspondences, their cancellative composition, real slopes, and the tangential deformation;
build the relevant distribution spaces, normalized local principal values, and the global trace formula;
identify the resulting counting distribution with the completed zeta function, including the archimedean term and normalization;
establish the positivity statement in the explicit formula (or an adequate cohomological or intersection-theoretic substitute) that is equivalent to the Weil criterion for the Riemann hypothesis.

The current Lean results rigorously reach the tensor Frobenius action, the adèlic subgroup invariance calculations, and the completed analytic logarithmic derivative on \(\operatorname {Re}(s){\gt}1\). The geometric distributional bridge and, above all, the final positivity mechanism remain unformalized and mathematically decisive.