Motivation

Central values of twists of elliptic-curve and modular-form $L$-functions govern arithmetic questions ranging from Mordell--Weil ranks to the distribution of nonvanishing twists. Classical Iwasawa theory organizes twists whose conductors grow vertically through powers of one prime. Kriz and Nordentoft introduce a horizontal analogue in which the order of the character is fixed while its conductor acquires new prime factors. Their paper Horizontal p-adic L-functions constructs measures encoding these twists and proves a structure theorem that forces quantitative nonvanishing.

The mission formalizes the paper's common mechanism behind its nonvanishing theorems: Fourier theory of horizontal measures, norm-compatible modular-symbol theta elements, interpolation of central values, and propagation from nonzero measures to logarithmic-power lower bounds. The elliptic-curve statements in Theorems 1.1 and 1.2 are obtained in the paper by specializing this mechanism to weight-two newforms and adding the stated Galois-representation hypotheses.

Setting

Fix a prime $p$. The digit group is the compact product

$$G_p=\prod_{n\ge 0}\mathbf Z/p\mathbf Z.$$

A continuous character of $G_p$ has finite image and factors through a finite product. For a complete algebraically closed nonarchimedean field $K$ of residue characteristic $p$, a horizontal measure is represented in Lean by a continuous $K$-linear functional on the Banach space $C(G_p,K)$. Its Fourier transform is

$$\widehat\nu(\chi)=\int_{G_p}\chi\,d\nu.$$

The integral measures arising from the digit Iwasawa algebra have Fourier norms in a discrete geometric lattice. This is recorded explicitly by HasDiscreteFourierNorm; it is the norm-language counterpart of the discrete valuation hypothesis used in Corollary 2.9.

On the arithmetic side, modular symbols produce theta elements at finite squarefree conductors. Their projection maps do not initially form a compatible inverse system: an Euler factor appears each time a prime is removed. At an orderly prime this factor is a unit, so normalization produces a compatible system and hence a horizontal $p$-adic $L$-function. Evaluation at a character gives the modified central $L$-value of the corresponding twist.

Formalization targets

Finite-correction structure and interpolation

For every nonzero integral horizontal measure $\nu$, there is a finite set $M_\nu$ of characters and a constant $c>0$ such that

$$\lvert\widehat\nu(\chi\chi_0)\rvert_p=c$$

for some $\chi_0\in M_\nu$, for every continuous character $\chi$. If $\nu$ interpolates modified central values, these corrected values are nonzero and have optimal $p$-adic size. This is Theorem 1.6, equivalently the digit-algebra case of Corollary 2.9, combined with Corollary 5.4.

Elliptic-curve specialization

For a modular elliptic curve over $\mathbf Q$, the normalized theta system is assembled into the horizontal $p$-adic $L$-function of Definition 5.3 and shown to satisfy Corollary 5.4. The final milestones then specialize the structure and propagation theorems to prove Theorems 1.1 and 1.2 (assuming modularity), retaining the three alternative hypotheses of Theorem 1.1 and the jointly-good hypothesis for simultaneous nonvanishing in Theorem 1.2.

Quantitative propagation

If a fixed-order family has counting function bounded below by $X/(\log X)^{1-\alpha}$ and every character is related to a nonvanishing one by one of finitely many conductor-bounded corrections, the same lower bound holds for the nonvanishing subfamily. This isolates the formal content of Theorem 5.9 used in the applications of Section 5.4.

Significance

The structure theorem replaces one-variable Weierstrass preparation in an infinite-dimensional, non-noetherian Iwasawa algebra. It shows that the zero set of a nonzero horizontal measure is rigid enough that finitely many translations detect an optimal Fourier value everywhere. Through interpolation, this converts a single nonzero horizontal $p$-adic $L$-function into infinitely many nonzero complex central values with a quantitative lower bound.

A formal proof will add reusable infrastructure for nonarchimedean Fourier analysis on profinite products, finite group rings, inverse systems of theta elements, and character-counting asymptotics. None of these results currently has a machine-checked proof in Mathlib. The development is arranged so the analytic structure theorem and the modular-symbol construction can be attacked independently.

Difficulty

The central obstacle is that the horizontal Iwasawa algebra is neither noetherian nor reduced. A direct compactness or finite-generation argument on its spectrum is unavailable. At finite level, Fourier inversion introduces the group order into the valuation estimates; globally, one must control compatible finite quotients while keeping the exceptional correcting set finite. The arithmetic half has a separate normalization problem: raw theta elements satisfy norm relations only up to Euler factors, and interpolation must track imprimitive characters and the removed Euler factors exactly.

Formalization scope

The first version works with the exponent-$p$ digit group $G_p$, which is the setting of Theorem 1.6. Characters take values in the unit group of a complete algebraically closed ultrametric field $K$. Measures are continuous linear functionals on $C(G_p,K)$, and discreteness of integral Fourier values is an explicit hypothesis. The definition does not assume the finite-correction conclusion.

The modular-form layer is exposed through RawThetaSystem, ThetaSystem, and InterpolationDatum. Milestones must construct these data from genuine modular symbols and prove their norm and interpolation fields; merely postulating the desired nonvanishing values does not satisfy the goal. The quantitative statement uses an explicit eventual lower bound rather than asymptotic notation hidden behind an uninterpreted predicate.

Selected references

• Daniel Kriz and Asbjørn Christian Nordentoft, Horizontal p-adic L-functions, arXiv:2310.20678v3, 2025. https://arxiv.org/abs/2310.20678
• Yuri Manin, Periods of parabolic forms and p-adic Hecke series, Mathematics of the USSR-Sbornik 21 (1973). https://doi.org/10.1070/SM1973v021n03ABEH002016
• Glenn Stevens, The cuspidal group and special values of L-functions, Transactions of the AMS 291 (1985). https://doi.org/10.1090/S0002-9947-1985-0797057-3

Current proof decomposition

The new definition node isolates the horizontal Iwasawa algebra and the interpolation interface. The first new milestone constructs a nonzero horizontal $2$-adic $L$-function $\nu_E$. The second milestone assumes such a pair $(\nu_E,\nu_E\ne0)$ and combines the horizontal-measure structure theorem, the Friedberg--Hoffstein quadratic seed, Corollary 5.10, and fixed-order character counting to obtain the lower bound in Theorem 1.1(1). The mission goal then follows immediately by applying the existence milestone and passing its witness to the implication milestone.