Dependencies

The finite adèle class space used here is the orbit quotient

Concretely, Lean combines the commuting actions of positive rational units and profinite-integer units into an action of their product and takes its orbit-relation quotient. At this stage this is a quotient type; no quotient topology is asserted.

The Arithmetic Site is the ringed topos \((\widehat{\mathbb {N}^{\times }}, \mathcal{O})\) consisting of the presheaf topos \(\widehat{\mathbb {N}^{\times }}\) together with its structure sheaf \(\mathcal{O} = \bar{\mathbb {N}}\). Since this Lean development fixes the ambient topos, arithmeticSite is the bundled commutative-semiring-valued presheaf on \((B\mathbb {N}^{\times })^{\mathrm{op}}\); forgetting its algebraic structure gives structureSheaf.

The classifying category \(B\mathbb {N}^{\times }\) of \(\mathbb {N}^{\times }\) is the one-object category whose single object is \(*\) and whose morphisms \(* \to *\) are the elements of \(\mathbb {N}^{\times }\), with composition given by multiplication.

The Boolean semifield \(\mathbb {B}\) is realized in Lean as the bottom subsemiring of the idempotent semiring \(\bar{\mathbb {N}}\). Its elements are the additive and multiplicative identities of \(\bar{\mathbb {N}}\).

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

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

The completed analytic counting transform is

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.

A covariant \(\mathbb {N}^{\times }\)-action satisfies the elementary flatness axioms when its underlying set is nonempty, every two elements have a common predecessor under two positive-integer actions, and the action is free. Explicitly, the latter two conditions are

The type \(\mathbb {A}^{f}\) of finite adèles of \(\mathbb {Q}\) is the restricted product of the finite completions of \(\mathbb {Q}\) with respect to their valuation subrings. In Lean this is Mathlib’s finite adèle ring for the Dedekind domain \(\mathbb {Z}\) and its fraction field \(\mathbb {Q}\).

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

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.

Let \(X\) carry an action of \(\mathbb {N}^{\times }\). In the Lean development the proposition \(X\) is a flat \(\mathbb {N}^{\times }\)-action means that the category of elements of the associated type-valued action functor is cofiltered. This is the category-of-elements formulation of flatness used for the points of the presheaf topos.

For \(\lambda \in \mathbb {R}_{+}^{\times }\), the published Frobenius correspondence is

obtained from \(F(\lambda ,q)\) and the two inclusions of the tensor factors. On geometric points over \(\mathbb {R}_{+}^{\max }\) it corresponds to the positive-real scaling action on the associated adèle-class description. This geometric correspondence is not the ordinary \(\mathbb {N}^{\times }\)-scaling action on the global semiring, although that action is one algebraic ingredient in its rational models.

The tropical semiring \(\bar{\mathbb {N}}\) is the set \(\mathbb {N} \cup \{ +\infty \} \) equipped with:

• Tropical addition: \(a \oplus b := \min (a, b)\), with identity element \(+\infty \).

• Tropical multiplication: \(a \odot b := a + b\) (ordinary addition), with identity element \(0\).

In Lean, \(\bar{\mathbb {N}}\) is represented as Tropical (WithTop \(\mathbb {N}\)), via the abbreviation NBar. The zero element is trop \(\top \) (i.e. \(+\infty \)) and the multiplicative identity is trop 0.

The raw structure semiring on the square is Mathlib’s semiring tensor product

Let \(\mathbb {N}^{\times }\) denote the set \(\{ 1, 2, 3, \ldots \} \) of strictly positive integers equipped with ordinary multiplication. This is a commutative monoid with unit \(1\). In Lean we represent this as PNat with its multiplicative structure, via the abbreviation NPos.

The presheaf topos \(\widehat{\mathbb {N}^{\times }}\) is the category of functors \(B{\mathbb {N}^{\times }}^{\mathrm{op}} \to \mathbf{Set}\), i.e. the category of sets equipped with a left \(\mathbb {N}^{\times }\)-action (using commutativity to exchange left and right actions). In Lean this is represented literally as the functor category BNplus^op \(\mathbin {\leadsto }\) Type.

Multiplication in \(\bar{\mathbb {N}}\) induces the \(\mathbb {B}\)-algebra homomorphism

The profinite integers \(\hat{\mathbb {Z}}\subset \mathbb {A}^{f}\) form the subring of finite adèles that are integral at every finite place. Its unit group is denoted \(\hat{\mathbb {Z}}^*\).

For \(n,m\in \mathbb {N}^{\times }\), the rational Frobenius evaluation formalized in Lean is the algebra homomorphism

The Lean identifier retains the historical name frobeniusCorrespondence, but its type correctly records that it is an evaluation out of the tensor product, not an endomorphism of \(\bar{\mathbb {N}}\) and not a reduced-correspondence triple. Lean does not impose coprimality on \(n,m\); lowest terms matter only when the ratio \(n/m\) is used as a normalized rational parameter.

For \(a\in \mathbb {A}^{f}\), define the additive subgroup

where \(q\) is embedded diagonally in the finite adèles. This subgroup, including its membership criterion at every finite place, is constructed in Lean.

A reduced correspondence in the sense of Connes–Consani is a triple \((R,\ell ,r)\), where \(R\) is a multiplicatively cancellative semiring and \(\ell ,r\) are semiring maps from the one-sided tropical semiring to \(R\), each with zero kernel, whose two images generate \(R\). Composition is defined from a tensor product over the middle semiring followed by multiplicatively cancellative reduction.

This structure, its reduction operation, and its composition are not yet defined in Lean in this project.

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.

For each \(n \in \mathbb {N}^{\times }\), the scaling endomorphism \(\varphi _n : \bar{\mathbb {N}}\to \bar{\mathbb {N}}\) is defined by

where \(nx\) denotes ordinary multiplication in \(\mathbb {N}\). Equivalently, \(\varphi _n(x) = x^{\odot n}\), the \(n\)-fold tropical product of \(x\) with itself. In Lean, \(\varphi _n\) is defined as a semiring endomorphism NBar ->+* NBar via scalingEndomorphism.

Each scaling semiring endomorphism \(\varphi _n\) fixes the embedded Boolean semifield, and hence defines a \(\mathbb {B}\)-algebra endomorphism of \(\bar{\mathbb {N}}\).

The structure semiring \(\mathcal{O}\) of the Arithmetic Site is the commutative-semiring-valued presheaf whose value is \(\bar{\mathbb {N}}\) and whose restriction maps are the scaling endomorphisms \(n \cdot x := \varphi _n(x)=nx\).

The underlying Type-valued structure sheaf is obtained from \(\mathcal O\) by forgetting its commutative-semiring structure pointwise.

For \(n,m\in \mathbb {N}^{\times }\), functoriality of the tensor product defines

A point of a topos \(\mathcal{E}\) is a geometric morphism \(p : \mathbf{Set} \to \mathcal{E}\), i.e. an adjoint pair \(p^* \dashv p_*\) where \(p^*\) is left exact.

Two finite adèles \(a,b\) have the same image in the formalized orbit quotient if and only if there is an element \(g\) of the combined scaling group such that \(g\cdot b=a\).

Tropical addition on \(\bar{\mathbb {N}}\) is idempotent: \(a \oplus a = a\) for all \(a \in \bar{\mathbb {N}}\).

\(\bar{\mathbb {N}}\) is a commutative semiring.

\(\widehat{\mathbb {N}^{\times }}\) has a subobject classifier.

\(\widehat{\mathbb {N}^{\times }}\) is cartesian closed.

\(\widehat{\mathbb {N}^{\times }}\) has all small colimits.

\(\widehat{\mathbb {N}^{\times }}\) has all small limits.

On pure tensors the product map satisfies \(\mu (x\otimes y)=xy\).

The rational evaluation has the expected pure-tensor formula

If \(r\in \mathbb {Q}^{\times }_{+}\), \(a\in \mathbb {A}^{f}\), and \(x\in \mathbb {Q}\), then

Together with Lemma 6.12, this is the formalized orbit-invariance calculation needed on the adèlic side of the published point classification.

If \(u\in \hat{\mathbb {Z}}^*\) and \(a\in \mathbb {A}^{f}\), then multiplication by \(u\) does not change the associated rational subgroup:

The regular multiplication action of \(\mathbb {N}^{\times }\) on itself is flat.

The scaling endomorphisms compose multiplicatively:

for all \(m, n \in \mathbb {N}^{\times }\). In particular, the map \(n \mapsto \varphi _n\) is a monoid homomorphism from \((\mathbb {N}^{\times }, \times )\) into the semiring endomorphism monoid \(\mathrm{End}_{\mathrm{Semiring}}(\bar{\mathbb {N}})\).

If \(n{\gt}1\), the fixed points of \(\varphi _n\) on \(\bar{\mathbb {N}}\) are exactly the tropical zero \(+\infty \) and tropical one \(0\).

For each \(n \in \mathbb {N}^{\times }\), the map \(\varphi _n\) is a semiring endomorphism of \(\bar{\mathbb {N}}\): it preserves both operations and both identities.

The assignment \(n \mapsto \varphi _n\) defines a monoid homomorphism \((\mathbb {N}^{\times }, \times ) \to \mathrm{End}_{\mathrm{Semiring}}(\bar{\mathbb {N}})\), making \(\bar{\mathbb {N}}\) into a semiring object of \(\widehat{\mathbb {N}^{\times }}\) with \(\mathbb {N}^{\times }\) acting by multiplication.

On a pure tensor,

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

The completed zeta function satisfies

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

with the limit taken off the pole.

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

For an \(\mathbb {N}^{\times }\)-action, the elementary axioms are equivalent to cofilteredness of its category of elements, and hence to the flatness predicate used for points of the Arithmetic Site.

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

Let \(\lambda ,\lambda '\in \mathbb {R}_{+}^{\times }\). Composition of the published reduced Frobenius correspondences gives

when \(\lambda ,\lambda '\) are both rational, and also whenever \(\lambda \lambda '\) is irrational. If \(\lambda \) and \(\lambda '\) are both irrational but \(\lambda \lambda '\) is rational, the composite is instead the canonical tangential deformation of \(\Psi (\lambda \lambda ')\).

The space of isomorphism classes of points of \(\widehat{\mathbb {N}^{\times }}\) is canonically isomorphic to the double quotient

a piece of the adèle class space of \(\mathbb {Q}\). More precisely, the category of points of \(\widehat{\mathbb {N}^{\times }}\) is equivalent to the category of totally ordered groups isomorphic to non-trivial subgroups of \((\mathbb {Q}, \mathbb {Q}_+)\), with injective order-preserving homomorphisms as morphisms; the flat action associated to \(H\) uses \(H_{{\gt}0}\) as above.

The tensor Frobenius endomorphisms compose multiplicatively in each index:

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

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.