Faithful odd-prime theta elements using nonzero moduli

Open

HorizontalPadicL.seededFiniteThetaElements_exist_with_normRelation_v3

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

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

For odd p, the faithfully pushed-forward plus theta elements are integral after uniform period scaling and satisfy the horizontal norm relations. The algebraic/classical symbol comparison is required only for nonzero moduli, which are the only moduli occurring in the construction.

Deprecated. The conclusion is too weak to characterize the modular-symbol theta system: the theta family may be identically zero, making the norm relations automatic, and no finite-level character-evaluation formula ties it to critical L-values. A replacement should construct the same theta elements together with both their norm relations and their explicit evaluation formula.

Preamble

import Definitions.Def_KN_SeededThetaConstructionV2

set_option autoImplicit false
noncomputable section

Formal statement

namespace HorizontalPadicL

/-- For odd `p`, the plus modular-symbol theta elements push forward along the
chosen quotient maps and satisfy the horizontal norm relations.  The comparison
with algebraic symbols is required only at the nonzero moduli used here. -/
theorem seededFiniteThetaElements_exist_with_normRelation_v3
    {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)
    (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 := by
  sorry

end HorizontalPadicL

Source

Mazur--Tate--Teitelbaum modular-symbol period formalism; the analytic binomial-collapse argument formalized in the MTT distribution-relation development; Kriz--Nordentoft, https://arxiv.org/pdf/2310.20678, Section 3.

View graph