Reduction of a point of order eighteen

If Q has exact order eighteen, then 2Q has exact order nine and 9Q has exact order two. Normalize the order-nine point to the marked point on Tate normal form. The first fact gives orderNinePolynomial b c = 0; the transported order-two point supplies a rational root of the explicit two-division cubic.

This is the denominator-safe common entry to the usual genus-two model for X₁(18). The elimination and rational-point classification are kept as a separate boundary.

def MazurTorsion.Kubert.tateTwoDivisionPolynomial (b c r : ℚ) : ℚ

The duplication denominator on Tate normal form. Its rational roots are the abscissas of the nonzero rational points killed by two.

Equations

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

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

A rational point of exact order eighteen produces simultaneous order-nine and rational-two-torsion equations on one Tate normal form, with the original discriminant scale retained.