Challenge: rational points on the order-eighteen curve

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

theorem MazurTheorem.Challenge.xOneEighteen_no_noncuspidal_point (x y : ℚ) (hx0 : x ≠ 0) (hx1 : x ≠ 1) (hcurve : y ^ 2 = MazurTorsion.Kubert.orderEighteenHyperellipticPolynomial x) : False

The explicit order-eighteen genus-two model has no rational point away from its two cusp abscissas.