The Euler-seven weighted trace bound above the elementary range

This module converts the exact χ≤7 Proposition Two result into its numerical torsion-intersection estimate when 48 < p.

theorem BGS.Markoff.weightedTraceTorsionIntersection_card_cast_le_eulerSeven_of_largeChar {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] (alpha beta : K) (hadmissible : WeightedTraceCurveIsCorvajaZannierAdmissible alpha beta) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmPrime : ¬p ∣ m) (hnPrime : ¬p ∣ n) (hlarge : 48 < p) : ↑(External.torusCurveTorsionIntersection K (weightedTraceTorusClosurePolynomial alpha beta) m n).card ≤ corvajaZannierCorollaryTwoNumericalBound p m n 2 2 7