Applying the general affine Hasse--Weil theorem to split trace covers

theorem BGS.Markoff.splitTraceCoverPolynomial_degreeOf_first_le {K : Type u_1} [Field K] (alpha beta : K) (d e : ℕ) : MvPolynomial.degreeOf 0 (splitTraceCoverPolynomial alpha beta d e) ≤ 2 * d

theorem BGS.Markoff.splitTraceCoverPolynomial_degreeOf_second_le {K : Type u_1} [Field K] (alpha beta : K) (d e : ℕ) : MvPolynomial.degreeOf 1 (splitTraceCoverPolynomial alpha beta d e) ≤ 2 * e

theorem BGS.Markoff.splitTraceCoverPolynomial_hasBidegreeAtMost {K : Type u_1} [Field K] (alpha beta : K) (d e : ℕ) : External.HasBidegreeAtMost (splitTraceCoverPolynomial alpha beta d e) (2 * d) (2 * e)

theorem BGS.Markoff.weightedSplitTraceWeilBoundAssumption_of_bivariateAffineHasseWeilBound (generalCoefficient : ℕ) (hgeneral : External.BivariateAffineHasseWeilBound generalCoefficient) : WeightedSplitTraceWeilBoundAssumption (4 * generalCoefficient + 1)

A fixed-coefficient affine Hasse--Weil bound supplies the correspondingly fixed split trace estimate.

theorem BGS.Markoff.exists_weightedSplitTraceWeilBoundAssumption_of_generalHasseWeil (hHasse : External.GeneralBivariateAffineHasseWeilTheorem) : ∃ (coefficient : ℕ), WeightedSplitTraceWeilBoundAssumption coefficient

The general affine Hasse--Weil theorem supplies the uniform split trace estimate. Absolute irreducibility remains an explicit premise of the target interface and the unique affine boundary point is absorbed into the uniform coefficient.