Almost all primes are partially regular

Abstract

For odd primes $p$, we let $K_p:=\mathbb{Q}(\hat{I}{\P }_p)$ be the $p$th cyclotomic field and let $\ddot{I}‰$ denote its Teichmuller character. For $\hat{I}\pm >1/2$, we say that an odd prime $p$ is partially regular if the eigenspaces of the $p$-Sylow subgroup of $\mathrm{Cl}(K_p)$ under the Galois action vanish for all characters $\ddot{I}{‰}^{p-2k}$ with \[ 2\le 2k \le \frac{\sqrt{p}}{(\log p)^α}. \] Equivalently, $p\nmid \mathrm{num}(B_{2k})$ throughout this range. We prove that a density-one subset of primes is partially regular in this sense. By Leopoldt reflection, this yields a partial Vandiver Theorem: for a density-one set of primes $p$, the even eigenspaces $A_p(\ddot{I}{‰}^{2k})$ vanish for all even $2k$ satisfying the inequality above. This result has consequences for Kubota-Leopoldt $p$-adic $L$-functions, congruences between cusp forms and Eisenstein series, and $p$-torsion in algebraic $K$-groups. The theorem proving partial regularity for almost all $p$ is fully formalized in Lean/Mathlib and was produced automatically by AxiomProver from a natural-language statement of the conjecture.