Full-support inverse-seed theta evaluation as an algebraic-symbol sum

Proved

HorizontalPadicL.seededInverseTheta_eval_ne_zero_iff_algebraicSymbol_sum

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

dirichlet-charactersmodular-formsmodular-symbolsp-adic-l-functions

Expand the explicit theta coefficients, interchange the finite sums, and use faithful character realization. For a full-support character, theta evaluation is nonzero exactly when the corresponding primitive-product weighted algebraic modular-symbol sum is nonzero.

Preamble

import Definitions.Def_KN_SeededInverseThetaSystem

set_option autoImplicit false
noncomputable section
open scoped BigOperators

Formal statement

namespace HorizontalPadicL

/-- Evaluation of an inverse-seed theta element at a full-support horizontal
character has the same zero set as the corresponding algebraic modular-symbol
sum.  The supplied equality is the small level-change bridge identifying the
full-level character with its primitive realization. -/
theorem seededInverseTheta_eval_ne_zero_iff_algebraicSymbol_sum
    {N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    (hk : 2 ≤ k) (heven : Even k)
    (f : MTT.Eigenform N k ι)
    (P : MTT.Periods k ι f.form) (η : DirichletCharacterWithLevel)
    (hηprim : η.2.IsPrimitive)
    (ιp : MTT.Qbar →+* ℂ_[p])
    (L : SeededHorizontalPrimeDataV3 p ιp f η B)
    (scale : IntegralPeriodScale f ιp P)
    (Θ : SeededFiniteThetaDataV3 L)
    (hΘ : Θ.IsInverseSeedThetaSystem P scale)
    (χ : HorizontalCharacter p L.exponent)
    (hfull : (Θ.characters.realized χ).2.conductor =
      L.supportModulus χ.support)
    (hatLevel : ∀ u : (ZMod (L.supportModulus χ.support))ˣ,
      Θ.characters.atLevel χ u.val.val =
        (Θ.characters.realized χ).2 u.val.val) :
    ∃ s : Bool, (MTT.sign s : ℤ) = (-1 : ℤ) ^ (k / 2 - 1) ∧
      (Θ.eval χ ≠ 0 ↔
        let θ := primitiveProductV2 η (Θ.characters.realized χ)
        letI : NeZero θ.1.1 := ⟨Nat.ne_of_gt θ.1.2⟩
        (∑ a : ZMod θ.1.1,
          θ.2 a * MTT.algebraicSymbol P s
            (k / 2 - 1) a.val θ.1.1) ≠ 0) := by
  sorry

end HorizontalPadicL

Source

Kriz--Nordentoft, Horizontal p-adic L-functions, https://arxiv.org/pdf/2310.20678, Corollary 3.6 and Corollary 5.4; standard Dirichlet-character and modular-symbol identities.

View graph