Applying general Corvaja--Zannier to the weighted trace curve

theorem BGS.Markoff.weightedTraceTorusClosurePolynomial_pderiv_first_ne_zero {K : Type u_1} [Field K] (alpha beta : K) (hbeta : beta ≠ 0) : (MvPolynomial.pderiv 0) (weightedTraceTorusClosurePolynomial alpha beta) ≠ 0

theorem BGS.Markoff.weightedTraceTorusClosurePolynomial_pderiv_second_ne_zero {K : Type u_1} [Field K] (alpha beta : K) (hbeta : beta ≠ 0) : (MvPolynomial.pderiv 1) (weightedTraceTorusClosurePolynomial alpha beta) ≠ 0

theorem BGS.Markoff.weightedTraceCurveNotSubtorusTranslate_general {K : Type u_1} [Field K] (alpha beta : K) (hbeta : beta ≠ 0) (hnot : WeightedTraceCurveNotSubtorusTranslate alpha beta) : External.TorusCurveNotSubtorusTranslate (weightedTraceTorusClosurePolynomial alpha beta)

theorem BGS.Markoff.weightedTraceTorusClosurePolynomial_hasBidegreeAtMost {K : Type u_1} [Field K] (alpha beta : K) (hbeta : beta ≠ 0) : External.HasBidegreeAtMost (weightedTraceTorusClosurePolynomial alpha beta) 2 2

theorem BGS.Markoff.weightedTraceCurve_isGeneralCorvajaZannierPlaneCurve {K : Type u_1} [Field K] (alpha beta : K) (hadmissible : WeightedTraceCurveIsCorvajaZannierAdmissible alpha beta) : External.IsCorvajaZannierPlaneCurve (weightedTraceTorusClosurePolynomial alpha beta)

theorem BGS.Markoff.generalTorusTorsionIntersection_weightedTrace_eq {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (alpha beta : K) (leftOrder rightOrder : ℕ) : External.torusCurveTorsionIntersection K (weightedTraceTorusClosurePolynomial alpha beta) rightOrder leftOrder = weightedTraceCurveTorsionIntersection alpha beta leftOrder rightOrder

theorem BGS.Markoff.corvajaZannierWeightedTraceBound_of_generalTheorem (hGeneral : External.GeneralCorvajaZannierPlaneCurveTheorem) (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [Fintype K] [CharP K p] : WeightedTraceTorsionIntersectionBound p K

The weighted-trace estimate is a proved application of the one general Corvaja--Zannier plane-curve theorem.

theorem BGS.Markoff.corvajaZannierWeightedTraceBound (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [Fintype K] [CharP K p] : WeightedTraceTorsionIntersectionBound p K

The weighted-trace Corvaja--Zannier estimate, obtained by instantiating the unconditional general plane-curve theorem proved in this repository.