AINTLIB blueprints

Verso blueprints for the projects in AINTLIB, an AI-reviewed number-theory library.

• p-adic L-functions Formalisation of Rodrigues Jacinto–Williams, An introduction to p-adic L-functions: measures on Z_p, the Kubota–Leopoldt p-adic L-function, and Iwasawa theory.
• Modular forms — the valence formula The complex-analytic toolkit behind the valence formula: generalised winding numbers, the multi-point Cauchy principal value, and the Hungerbühler–Wasem generalised residue theorem.
• Strong multiplicity one Strong multiplicity one for cusp forms (Miyake 4.6.8 / 4.6.12), via the abstract GL(2) Hecke ring, eigenforms, and the old/new decomposition — the axiom-clean theorem that a newform is determined by almost all its Hecke eigenvalues.
• Chebotarev density theorem Dirichlet density, decomposition/inertia/Frobenius, the zeta factorisation for abelian extensions, and the cyclotomic and abelian cases building to the full Chebotarev density theorem.
• Kummer's criterion & regular primes Generalised Bernoulli numbers, Gauss sums and Stickelberger, the relative class number formula for h⁻, cyclotomic units, and Kummer's criterion — applied to Fermat's Last Theorem for exponent 37 and the infinitude of irregular primes.
• The Hasse bound Hasse's theorem for elliptic curves over a finite field — the unconditional, sorry-free bound |#E(F_q) − q − 1| ≤ 2√q, via the positive-definite degree form on End(E) and the Frobenius trace.
• Adic spaces Huber's theory of adic spaces (Wedhorn): Huber and Tate rings, the valuation spectrum, rings of integral elements, the adic spectrum Spa, Tate algebras, and the structure sheaf.