The seeded Frobenius class consists of orderly primes

Proved

HorizontalPadicL.seededFrobeniusClass_isOrderly

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

galois-representationsmodular-formsnumber-theoryp-adic-l-functions

Assume the seed character has order at least two and its order is prime to $p$ . Every prime $\ell$ in the simultaneous Frobenius class is orderly of exponent $m$ . The local expression is a $p$ -adic unit because modulo the maximal ideal it is

2\eta(\ell)-1-\eta(\ell)^2=-(\eta(\ell)-1)^2,

and a nontrivial root of unity of order prime to $p$ remains nontrivial after reduction.

Preamble

import Definitions.Def_KN_SeededPrimeGaloisData

set_option autoImplicit false

Formal statement

namespace HorizontalPadicL

theorem seededFrobeniusClass_isOrderly
    {N k p m B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    {f : MTT.Eigenform N k ι} {η : DirichletCharacterWithLevel}
    {V : SeededEigenformPadicPlaceData (p := p) f η}
    (D : SeededOrderlyFrobeniusClassData f η m B V)
    (hηorder : 2 ≤ orderOf η.2)
    (horderCoprime : Nat.Coprime (orderOf η.2) p) :
    ∀ ⦃ℓ : ℕ⦄, ℓ ∈ D.primes →
      IsOrderlyPrimeForSeededEigenformV2 p m V.embedding f η ℓ := by sorry

end HorizontalPadicL

Source

Kriz–Nordentoft, Horizontal p-adic L-functions, arXiv:2310.20678v3, §4.3, Lemma 4.14 and Corollary 4.15, pp. 30–31.

View graph