Reduction of a point of order nine

If the marked point P = (0, 0) on Tate normal form has exact order nine, then 5P = -4P. Comparing the already checked fourth- and fifth-multiple abscissas and clearing only the proved-nonzero denominators gives

c⁵ + c⁴ + (1-b)c³ - 3bc² + 3b²c - b³ = 0.

This is the common Tate-parameter certificate used by the order-eighteen and order-twenty-seven branches. No rational-point classification of the resulting parameter curve is asserted here.

def MazurTorsion.Kubert.orderNinePolynomial (b c : ℚ) : ℚ

The Tate-parameter equation forced by exact order nine of the marked point.

Equations

• MazurTorsion.Kubert.orderNinePolynomial b c = c ^ 5 + c ^ 4 + (1 - b) * c ^ 3 - 3 * b * c ^ 2 + 3 * b ^ 2 * c - b ^ 3

theorem MazurTorsion.Kubert.c_ne_zero_of_marked_order_nine (b c : ℚ) (hb : b ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) (horder : addOrderOf (WeierstrassCurve.Affine.Point.some 0 0 h00) = 9) : c ≠ 0

theorem MazurTorsion.Kubert.parameters_ne_of_marked_order_nine (b c : ℚ) (hb : b ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) (horder : addOrderOf (WeierstrassCurve.Affine.Point.some 0 0 h00) = 9) : b ≠ c

theorem MazurTorsion.Kubert.orderNinePolynomial_eq_zero_of_marked_order (b c : ℚ) (hb : b ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) (horder : addOrderOf (WeierstrassCurve.Affine.Point.some 0 0 h00) = 9) : orderNinePolynomial b c = 0

Exact order nine of the marked Tate point forces orderNinePolynomial b c = 0.

theorem MazurTorsion.Kubert.exists_tateOrderNine_certificate (E : WeierstrassCurve ℚ) [E.IsElliptic] (Q : (WeierstrassCurve.Affine.baseChange E ℚ).Point) (hQ : addOrderOf Q = 9) : ∃ (b : ℚ) (c : ℚ) (u : ℚ), u ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ b ≠ c ∧ orderNinePolynomial b c = 0 ∧ u ^ 12 * E.Δ = (tateNormalCurve b c).Δ

A rational point of exact order nine produces a denominator-safe point on the explicit Tate-parameter curve, retaining the twelfth-power discriminant scale of the original curve.