The exact Euler-seven weighted trace bound

Above the elementary range this is the χ≤7 Proposition Two endpoint. Below that range the roots-of-unity count lands directly in the unchanged quotient-by-characteristic branch.

theorem BGS.Markoff.weightedTraceTorsionIntersection_card_cast_le_eulerSeven {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) : ↑(External.torusCurveTorsionIntersection K (weightedTraceTorusClosurePolynomial alpha beta) m n).card ≤ corvajaZannierCorollaryTwoNumericalBound p m n 2 2 7

The χ≤7 weighted trace estimate in every characteristic.