Finiteness of primitive characters of bounded conductor

Proved

HorizontalPadicL.primitiveCharacters_boundedConductor_finite

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

dirichlet-charactersnumber-theoryp-adic-l-functions

There are only finitely many primitive algebraic Dirichlet characters with conductor bounded by a fixed real number. Primitivity prevents duplicate presentations at unbounded levels.

Preamble

import Definitions.Def_KN_PrimePowerPropagation

set_option autoImplicit false
noncomputable section
open scoped BigOperators

Formal statement

namespace HorizontalPadicL

/-- There are only finitely many primitive algebraic Dirichlet characters
with conductor bounded by a fixed real number. Primitivity prevents duplicate
presentations at unbounded levels. -/
theorem primitiveCharacters_boundedConductor_finite (X : ℝ) :
    {χ : DirichletCharacterWithLevel |
      χ.2.IsPrimitive ∧ (χ.2.conductor : ℝ) ≤ X}.Finite := by
  sorry

end HorizontalPadicL

Source

Kriz--Nordentoft, Horizontal p-adic L-functions, https://arxiv.org/pdf/2310.20678, Section 2.3.3, Lemma 5.7, Theorem 5.9 and Corollary 5.10.

View graph