Package a normalized theta measure as a seeded horizontal p-adic L-function

Proved

HorizontalPadicL.seededHorizontalPadicLFunction_assemble

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

modular-formsmodular-symbolsnumber-theoryp-adic-l-functions

A density-free normalized theta measure with interpolation and nonzero trivial evaluation can be packaged with the original positive-density prime system to give the required seeded horizontal p-adic L-function. No density argument is used in this packaging step.

Deprecated. It packages the false universal order bound from the retired interpolation contract. Use replacement node 52158e1e-6b23-453d-937c-45bcbca5548c.

Preamble

import Definitions.Def_KN_SeededThetaConstruction

set_option autoImplicit false
noncomputable section

Formal statement

namespace HorizontalPadicL

/-- Package a density-free normalized theta measure back together with the
original prime system. Density enters only through this final record field and
is not used in the construction. -/
theorem seededHorizontalPadicLFunction_assemble
    {N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    (f : MTT.Eigenform N k ι) (hnew : IsNewEigenform f)
    (η : DirichletCharacterWithLevel) (ιp : MTT.Qbar →+* ℂ_[p])
    (L : SeededHorizontalPrimeSystemV2 p ιp f η B)
    (μ : SeededNormalizedThetaMeasure L.toConstructionData)
    (hinterp : μ.InterpolatesSeededCriticalValues)
    (htrivial : μ.measure.eval
      (trivialHorizontalCharacterV2 p L.toConstructionData.exponent) ≠ 0) :
    ∃ ν : SeededHorizontalPadicLFunctionV2 (B := B) p ιp f η,
      ν.primes = L ∧ ν.InterpolatesSeededCriticalValues ∧
      ν.measure.eval (trivialHorizontalCharacterV2 p ν.primes.exponent) ≠ 0 := by sorry

end HorizontalPadicL

Source

Kriz--Nordentoft, https://arxiv.org/pdf/2310.20678, Sections 3 and 5.

View graph