1
The multiplicative monoid \(\mathbb {N}^{\times }\)
2
The tropical semiring \(\bar{\mathbb {N}}\)
3
The presheaf topos \(\widehat{\mathbb {N}^{\times }}\)
4
The structure sheaf
5
The Arithmetic Site
6
Points of the topos
▶
6.1
The finite adèlic side
7
The Frobenius correspondences
▶
7.1
The formalized tensor-algebra layer
7.2
Published reduced correspondences
8
Connection to the Riemann zeta function
▶
8.1
Analytic statements proved in Lean
8.2
The published distributional counting formula
8.3
The Riemann-hypothesis frontier
Dependency graph
ArithmeticSite
Jon Bannon
1
The multiplicative monoid \(\mathbb {N}^{\times }\)
2
The tropical semiring \(\bar{\mathbb {N}}\)
3
The presheaf topos \(\widehat{\mathbb {N}^{\times }}\)
4
The structure sheaf
5
The Arithmetic Site
6
Points of the topos
6.1
The finite adèlic side
7
The Frobenius correspondences
7.1
The formalized tensor-algebra layer
7.2
Published reduced correspondences
8
Connection to the Riemann zeta function
8.1
Analytic statements proved in Lean
8.2
The published distributional counting formula
8.3
The Riemann-hypothesis frontier