Reduction of a point of order fifteen

An exact rational point of order 15 can be put in Tate normal form. Its fifth multiple then has exact order 3, so the X-coordinate of that multiple is a root of the third division polynomial. Clearing the two honest Tate denominators produces the polynomial orderFifteenPolynomial below.

This file proves only the forward modular reduction. In particular, it makes no assertion about the rational points of the resulting affine parameter curve.

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

A compact polynomial equation for the Tate-parameter image of X₁(15).

Writing A = c² + c - b and d = b - c, this is the third division polynomial at x(5P) = bcA/d², after multiplication by d⁸ and removal of the nonzero factor b³.

Equations

• One or more equations did not get rendered due to their size.

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

The discriminant of the two-parameter Tate normal form, in a factored presentation useful for retaining the twelfth-power scale supplied by Tate normalization.

Equations

• MazurTorsion.Kubert.tateNormalDiscriminant b c = b ^ 3 * (16 * b ^ 2 - 8 * b * c ^ 2 - 20 * b * c + b + c ^ 4 - 3 * c ^ 3 + 3 * c ^ 2 - c)

theorem MazurTorsion.Kubert.tateNormalCurve_discriminant (b c : ℚ) : (tateNormalCurve b c).Δ = tateNormalDiscriminant b c

theorem MazurTorsion.Kubert.orderFifteenPolynomial_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) = 15) : orderFifteenPolynomial b c = 0

Exact order 15 of the marked Tate point forces the compact parameter polynomial to vanish. The proof records the fifth multiple explicitly and uses its exact order 3.

theorem MazurTorsion.Kubert.exists_tateOrderFifteen_certificate (E : WeierstrassCurve ℚ) [E.IsElliptic] (Q : (WeierstrassCurve.Affine.baseChange E ℚ).Point) (hQ : addOrderOf Q = 15) : ∃ (b : ℚ) (c : ℚ) (u : ℚ), u ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ b ≠ c ∧ c ^ 2 + c - b ≠ 0 ∧ orderFifteenPolynomial b c = 0 ∧ u ^ 12 * E.Δ = tateNormalDiscriminant b c

A rational point of exact order 15 produces a point on the explicit Tate-parameter curve, with every denominator condition and the original discriminant scale retained.

The additional condition c²+c-b ≠ 0 follows from the displayed polynomial and b-c ≠ 0; it is useful when continuing the checked multiple recurrence from 5P to 6P.