Reduction of a point of order eleven

Let P = (0, 0) on the Tate normal form

y² + (1-c)xy - by = x³ - bx².

The checked addition recurrence gives explicit coordinates for 5P and 6P. If P has exact order eleven, then 6P = -5P, so their X-coordinates agree. Put

• A = c² + c - b,
• B = b² - bc - c³, and
• d = b-c.

Clearing only the already proved nonzero denominators gives the compact parameter equation

d³ B - bc A³ = 0.

This file proves the exact-order reduction and retains all factors needed by the birational model map. It does not classify the rational points of the parameter curve.

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

The numerator in the denominator-safe formula for x(6P).

Equations

• MazurTorsion.Kubert.orderElevenSixNumerator b c = b ^ 2 - b * c - c ^ 3

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

The compact Tate-parameter equation for exact order eleven.

Equations

• MazurTorsion.Kubert.orderElevenPolynomial b c = (b - c) ^ 3 * MazurTorsion.Kubert.orderElevenSixNumerator b c - b * c * (c ^ 2 + c - b) ^ 3

theorem MazurTorsion.Kubert.tateSixX_eq_orderEleven_reduced (b c : ℚ) (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (hA : c ^ 2 + c - b ≠ 0) : tateSixX b c = (b - c) * orderElevenSixNumerator b c / (c ^ 2 + c - b) ^ 2

Denominator-safe reduced formula for the abscissa of 6P.

theorem MazurTorsion.Kubert.orderElevenPolynomial_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) = 11) : orderElevenPolynomial b c = 0

Exact order eleven of the marked Tate point forces the compact parameter polynomial to vanish.

theorem MazurTorsion.Kubert.orderElevenSixNumerator_ne_zero {b c : ℚ} (hb : b ≠ 0) (hc : c ≠ 0) (hA : c ^ 2 + c - b ≠ 0) (hpoly : orderElevenPolynomial b c = 0) : orderElevenSixNumerator b c ≠ 0

On an admissible solution of the compact equation, the numerator of x(6P) is also nonzero.

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

A rational point of exact order eleven produces an admissible point on the explicit Tate-parameter curve, with the discriminant scale retained.