Odd-prime seeded construction implies Corollary 5.17
OpenHorizontalPadicL.seededHorizontalPadicLConstruction_implies_corollary_5_17_v3dirichlet-charactersmodular-formsnumber-theoryp-adic-l-functions
For d congruent to 2 modulo 4, a nonzero even quadratic seed and the uniform odd-prime seeded construction imply the logarithmic-power lower bound for nonvanishing primitive twists of exact order d. Since d/2 is odd, every prime-power propagation stage satisfies p not equal to 2.
Preamble
import Definitions.Def_KN_SeededHorizontalPadicLFunctionV3 set_option autoImplicit false
Formal statement
namespace HorizontalPadicL
/-- Odd-prime propagation from a nonzero even quadratic seed gives
Kriz--Nordentoft Corollary 5.17. -/
theorem seededHorizontalPadicLConstruction_implies_corollary_5_17_v3
{N k : ℕ} (hN : 0 < N) (hk : 2 ≤ k) (heven : Even k)
(ι : MTT.Qbar →+* ℂ) (f : MTT.Eigenform N k ι)
(hconstruction : HasSeededHorizontalPadicLConstructionV3 ι f)
(d : ℕ) (hcase1 : d % 4 = 2 ∧ 6 ≤ d)
(η : DirichletCharacterWithLevel)
(hηprim : η.2.IsPrimitive)
(hηorder : orderOf η.2 = 2)
(hηeven : η.2 (-1) = 1)
(hηcoprime : Nat.Coprime (N * d) η.2.conductor)
(hηnonzero :
@MTT.criticalLValue ι f.form
η.1.1 ⟨Nat.ne_of_gt η.1.2⟩ η.2 (k / 2 - 1) ≠ 0) :
∃ α : ℝ, 0 < α ∧
HasLogPowerLowerBound (eigenformNonvanishingCount ι f d) α := by
sorry
end HorizontalPadicLSource
Kriz--Nordentoft, Horizontal p-adic L-functions, https://arxiv.org/pdf/2310.20678, Corollary 3.6, Definition 5.3, Corollary 5.4, Theorem 5.9, Corollary 5.10 and Corollary 5.17.