The weighted trace curve is not a subtorus translate

This module proves the non-specialness condition needed by the Corvaja--Zannier torsion-point bound. The proof uses the two deck involutions of the weighted trace curve and keeps all degenerate parameters explicit.

theorem BGS.Markoff.weightedTraceCurve_notSubtorusTranslate_of_weights_ne_zero {K : Type u_1} [Field K] (alpha beta : K) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) : WeightedTraceCurveNotSubtorusTranslate alpha beta

If both weights are nonzero, the complete weighted trace curve is not a character fiber in the two-dimensional torus. No characteristic restriction is needed.

This deliberately does not assume alpha * beta ≠ 1. When the product is one the curve is reducible into two subtorus translates, but no single character is constant on their union. Thus this proposition is the correct non-specialness condition only when paired with the separate absolute irreducibility hypothesis, exactly as it is in WeightedTraceCurveIsCorvajaZannierAdmissible.

theorem BGS.Markoff.weightedTraceCurve_isCorvajaZannierAdmissible_of_absoluteIrreducible {K : Type u_1} [Field K] (alpha beta : K) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hnondegenerate : alpha * beta ≠ 1) (hirreducible : WeightedTraceCurveAbsolutelyIrreducible alpha beta) : WeightedTraceCurveIsCorvajaZannierAdmissible alpha beta

Once absolute irreducibility is supplied, all remaining geometric admissibility conditions are discharged by the explicit parameter hypotheses.