Exact bidegree of the weighted middle-game trace curve

Corvaja--Zannier Corollary 2 uses the two coordinate degrees of the affine torus curve. This module computes those degrees for the actual reduced weighted trace closure. The two-variable polynomial is transported through the explicit Fin 2 multivariate-to-iterated-polynomial equivalence already used in the irreducibility proof; swapping the two polynomial variables computes the second coordinate degree.

theorem BGS.Markoff.weightedTraceIteratedPolynomial_right_natDegree {K : Type u_1} [Field K] (alpha beta : K) : (weightedTraceIteratedPolynomial alpha beta).natDegree = 2

The weighted trace closure has degree two in the right trace coordinate.

theorem BGS.Markoff.weightedTraceIteratedPolynomial_left_natDegree {K : Type u_1} [Field K] (alpha beta : K) (halpha : alpha ≠ 0) : (Polynomial.Bivariate.swap (weightedTraceIteratedPolynomial alpha beta)).natDegree = 2

The weighted trace closure has degree two in the left weighted coordinate when its leading weight is nonzero.

theorem BGS.Markoff.weightedTraceTorusClosurePolynomial_iteratedBidegree {K : Type u_1} [Field K] (alpha beta : K) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) : have p := finTwoToIteratedPolynomial (weightedTraceTorusClosurePolynomial alpha beta); (p.natDegree, (Polynomial.Bivariate.swap p).natDegree) = (2, 2)

In the nonzero-weight branch used by the Markoff middle game, the reduced torus closure has exact bidegree (2, 2). The pair is expressed through the explicit iterated-polynomial presentation, so no informal support convention is hidden in the statement.