Faithful odd-prime theta measure using nonzero moduli

import Definitions.Def_KN_SeededThetaConstructionV2
import Theorems.Thm_MTT_birch_mellin_formula

set_option autoImplicit false
noncomputable section

namespace HorizontalPadicL

/-- For odd `p`, normalization of the faithful theta system gives a plus
horizontal measure interpolating every horizontal character.  Symbol comparison
is requested only at the positive, hence nonzero, conductors occurring in the
construction. -/
theorem seededNormalizedThetaMeasure_exists_with_interpolation_v3
    {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]) (hpodd : p ≠ 2)
    (L : SeededHorizontalPrimeDataV2 p ιp f η B)
    (characters : SeededHorizontalCharacterRealizationV2 L)
    (hcharacters : characters.HasExpectedProperties)
    (scale : IntegralPeriodScale f ιp P)
    (hcomparison : ∀ s j a m, j ≤ k - 2 → m ≠ 0 →
      ι (MTT.algebraicSymbol P s j a m) * P.omega s =
        signedModularSymbol f.form s j a m) :
    ∃ μ : SeededNormalizedThetaMeasureV2 L,
      μ.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