Interpolation of seeded central critical values

import Definitions.Def_KN_SeededThetaConstruction
import Theorems.Thm_MTT_birch_mellin_formula

set_option autoImplicit false
noncomputable section

namespace HorizontalPadicL

/-- Birch's formula identifies every character evaluation of the normalized
theta measure with the corresponding central critical value. At the trivial
horizontal character this is the original seeded twist by `η`. -/
theorem seededNormalizedThetaMeasure_interpolation
    {N k p B : ℕ} {ι : MTT.Qbar →+* ℂ} [Fact p.Prime]
    (hN : 0 < N) (hk : 2 ≤ k) (heven : Even k)
    (f : MTT.Eigenform N k ι) (hnew : IsNewEigenform f)
    (P : MTT.Periods k ι f.form) (η : DirichletCharacterWithLevel)
    (hηprim : η.2.IsPrimitive) (hηeven : η.2 (-1) = 1)
    (ιp : MTT.Qbar →+* ℂ_[p])
    (L : SeededHorizontalPrimeDataV2 p ιp f η B)
    (characters : SeededHorizontalCharacterRealization L)
    (μ : SeededNormalizedThetaMeasure L)
    (hcharacters : μ.characters = characters) :
    μ.InterpolatesSeededCriticalValues ∧
      (μ.measure.eval (trivialHorizontalCharacterV2 p L.exponent) ≠ 0 ↔
        @MTT.criticalLValue ι f.form
          η.1.1 ⟨Nat.ne_of_gt η.1.2⟩ η.2 (k / 2 - 1) ≠ 0) := by sorry

end HorizontalPadicL