Enumerating a positive-density orderly-prime set

Proved

HorizontalPadicL.positiveDensityOrderlySet_to_primeSystem

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

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

Let $A$ be a positive-density set of rational primes, all orderly with the same exponent $m>0$ , and all avoiding a fixed modulus $B$ . Then $A$ admits an injective enumeration which, together with its density certificate and local properties, defines a seeded horizontal prime system of order exponent $m$ .

This is the set-theoretic passage from the Chebotarev prime set to the sequence required by the horizontal measure construction.

Preamble

import Definitions.Def_KN_SeededPrimeGaloisData

set_option autoImplicit false

Formal statement

namespace HorizontalPadicL

theorem positiveDensityOrderlySet_to_primeSystem
    {N k p m B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    {f : MTT.Eigenform N k ι} {η : DirichletCharacterWithLevel}
    {V : SeededEigenformPadicPlaceData (p := p) f η}
    (hm : 0 < m)
    (D : SeededOrderlyFrobeniusClassData f η m B V)
    (δ : ℝ) (hδ : 0 < δ)
    (hdensity : HasPrimeNaturalDensity D.primes δ)
    (horderly : ∀ ⦃ℓ : ℕ⦄, ℓ ∈ D.primes →
      IsOrderlyPrimeForSeededEigenformV2 p m V.embedding f η ℓ) :
    ∃ L : SeededHorizontalPrimeSystemV2 p V.embedding f η B,
      L.orderExponent = m := 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