Horizontal characters at an odd prime have even realizations

Proved

HorizontalPadicL.realizedHorizontalCharacter_even_of_odd_prime

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

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

The order of a realized horizontal character is a power of the odd prime p. Its value at -1 has order at most two, so that value is one.

Preamble

import Definitions.Def_KN_SeededInverseThetaSystem

set_option autoImplicit false
noncomputable section

Formal statement

namespace HorizontalPadicL

/-- A realized horizontal character is even when the horizontal prime is odd:
its order is a power of `p`, while its value at `-1` has order at most two. -/
theorem realizedHorizontalCharacter_even_of_odd_prime
    {N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    {ιp : MTT.Qbar →+* ℂ_[p]} {f : MTT.Eigenform N k ι}
    {η : DirichletCharacterWithLevel}
    {L : SeededHorizontalPrimeDataV3 p ιp f η B}
    (R : SeededHorizontalCharacterRealizationV3 L)
    (hR : R.HasExpectedProperties) (hpodd : p ≠ 2)
    (χ : HorizontalCharacter p L.exponent) :
    (R.realized χ).2 (-1) = 1 := 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