Exact heights of powered plane-curve coordinates

The two rational-function-field models of a plane curve identify the base variable RatFunc.X with the corresponding coordinate function. Combining those models with the polynomial-height formula computes the positive degree of the principal divisor of x ^ m - 1 and y ^ n - 1 exactly.

theorem BGS.CorvajaZannier.finiteExtensionPositiveDegree_planeCurveFirstCoordinate_pow_sub_one {K : Type u_1} [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) : have hx := ⋯; finiteExtensionPositiveDegree K (PlaneCurveFunctionField f) (planeCurveFunction f 0 ^ m - 1) = MvPolynomial.degreeOf 1 f * m

In the first-coordinate RatFunc K model, the positive principal-divisor degree of x ^ m - 1 is m times the degree of the curve equation in the second coordinate.

theorem BGS.CorvajaZannier.finiteExtensionPositiveDegree_planeCurveSecondCoordinate_pow_sub_one {K : Type u_1} [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (n : ℕ) (hn : 0 < n) : have hy := ⋯; finiteExtensionPositiveDegree K (PlaneCurveFunctionField f) (planeCurveFunction f 1 ^ n - 1) = MvPolynomial.degreeOf 0 f * n

In the second-coordinate RatFunc K model, the positive principal-divisor degree of y ^ n - 1 is n times the degree of the curve equation in the first coordinate.