Challenge: exclude rational points of order forty-nine

The recommended route is to bridge the marked seven-isogeny tower to the already compiled rational-point classification of the explicit X_0(49) correspondence.

theorem MazurTheorem.Challenge.no_rational_point_of_order_fortyNine (E : WeierstrassCurve ℚ) [E.IsElliptic] (P : (WeierstrassCurve.Affine.baseChange E ℚ).Point) : addOrderOf P ≠ 49

An elliptic curve over the rationals has no rational point of exact additive order forty-nine.