Challenge: rational points on the order-thirteen curve

The compiled Tate-normal-form reduction sends a point of exact order thirteen to a rational point on this sextic with abscissa different from zero and negative one. Thus this statement is exactly the missing rational-point classification needed by that branch.

theorem MazurTheorem.Challenge.xOneThirteen_no_noncuspidal_point (x y : ℚ) (hx0 : x ≠ 0) (hxnegOne : x ≠ -1) (hcurve : y ^ 2 = MazurTorsion.Kubert.orderThirteenHyperellipticPolynomial x) : False

The explicit X₁(13) sextic has no rational point away from its two rational affine cusp abscissas.