Finite theta system with norm relations and critical-value zero set

Open

HorizontalPadicL.seededFiniteThetaSystem_exists_with_normRelations_and_criticalZeroSet

by davidloeffler · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

modular-formsmodular-symbolsnumber-theoryp-adic-l-functions

For an odd prime and a faithful horizontal-character realization, the scaled algebraic modular symbols define one finite theta system that simultaneously satisfies the Hecke norm relations and the finite-level Birch--Stevens zero-set formula. Thus the theta family cannot be chosen independently of the critical L-values.

Preamble

import Definitions.Def_KN_SeededFiniteThetaCriticalZeroSet
import Theorems.Thm_MTT_birch_mellin_formula

set_option autoImplicit false
noncomputable section

Formal statement

namespace HorizontalPadicL

/-- The faithfully pushed-forward theta elements constructed from the scaled
algebraic modular symbols simultaneously satisfy their Hecke norm relations
and the finite-level Birch--Stevens zero-set formula.  Keeping both properties
on the same witness rules out spurious systems such as the identically-zero
theta family. -/
theorem seededFiniteThetaSystem_exists_with_normRelations_and_criticalZeroSet
    {N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    (hN : 0 < N) (hk : 2 ≤ k) (heven : Even k)
    (f : MTT.Eigenform N k ι) (hnew : IsNewEigenform f)
    (P : MTT.Periods k ι f.form) (η : DirichletCharacterWithLevel)
    (hηprim : η.2.IsPrimitive) (hηeven : η.2 (-1) = 1)
    (ιp : MTT.Qbar →+* ℂ_[p]) (hpodd : p ≠ 2)
    (L : SeededHorizontalPrimeDataV2 p ιp f η B)
    (characters : SeededHorizontalCharacterRealizationV2 L)
    (hcharacters : characters.HasExpectedProperties)
    (scale : IntegralPeriodScale f ιp P)
    (hcomparison : ∀ s j a m, j ≤ k - 2 → m ≠ 0 →
      ι (MTT.algebraicSymbol P s j a m) * P.omega s =
        signedModularSymbol f.form s j a m) :
    ∃ Θ : SeededFiniteThetaDataV2 L,
      Θ.characters = characters ∧
      Θ.SatisfiesNormRelations ∧
      Θ.HasSeededCriticalZeroSet := by
  sorry

end HorizontalPadicL

Source

Kriz--Nordentoft, Horizontal p-adic L-functions, https://arxiv.org/pdf/2310.20678, Sections 3.3 and 5.1, especially Corollary 3.6, Corollary 5.2 and Corollary 5.4.

View graph