Reduction of a point of order thirteen

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

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

If P has exact order 13, then 7P = -6P; in particular, the two points have the same X-coordinate. The checked formulas for 6P and 7P turn this equality into

(b-c) B³ + bc A³ C = 0,

where

• A = c² + c - b,
• B = b² - bc - c³, and
• C = 2b² - bc² - 3bc + c².

All factors used as denominators are proved nonzero from exact order, rather than discarded during simplification.

The substitutions

r = b/c, s = c²/(b-c)

then give the affine plane model

r³ + (-s⁴ + 5s³ - 9s² + 4s - 2)r² + (-s³ + 6s² - 3s + 1)r - s³ = 0.

This file proves the forward reduction only. It does not classify the rational points of this genus-two modular curve.

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

The denominator-safe Tate-parameter polynomial forced by exact order 13.

It is obtained by equating the checked X-coordinates of 6P and 7P.

Equations

• MazurTorsion.Kubert.orderThirteenPolynomial b c = (b - c) * MazurTorsion.Kubert.tateSixNumerator b c ^ 3 + b * c * (c ^ 2 + c - b) ^ 3 * MazurTorsion.Kubert.tateSevenAux b c

def MazurTorsion.Kubert.orderThirteenReducedPolynomial (r s : ℚ) : ℚ

The reduced affine X₁(13) polynomial in the coordinates r = b/c and s = c²/(b-c).

Equations

• MazurTorsion.Kubert.orderThirteenReducedPolynomial r s = r ^ 3 + (-s ^ 4 + 5 * s ^ 3 - 9 * s ^ 2 + 4 * s - 2) * r ^ 2 + (-s ^ 3 + 6 * s ^ 2 - 3 * s + 1) * r - s ^ 3

theorem MazurTorsion.Kubert.orderThirteenPolynomial_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) = 13) : orderThirteenPolynomial b c = 0

Exact order 13 of the marked Tate point forces the denominator-safe X₁(13) parameter polynomial to vanish.

theorem MazurTorsion.Kubert.orderThirteenPolynomial_substitution (r s : ℚ) : orderThirteenPolynomial (r * s * (r - 1)) (s * (r - 1)) = s ^ 7 * (r - 1) ^ 11 * orderThirteenReducedPolynomial r s

Substituting b = rs(r-1) and c = s(r-1) factors the Tate polynomial as s⁷(r-1)¹¹ times the reduced polynomial.

theorem MazurTorsion.Kubert.exists_orderThirteen_reduced_certificate (b c : ℚ) (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (hA : c ^ 2 + c - b ≠ 0) (hB : tateSixNumerator b c ≠ 0) (hC : tateSevenAux b c ≠ 0) (hpoly : orderThirteenPolynomial b c = 0) : ∃ (r : ℚ) (s : ℚ), r = b / c ∧ s = c ^ 2 / (b - c) ∧ r ≠ 0 ∧ r ≠ 1 ∧ s ≠ 0 ∧ s ≠ 1 ∧ r ≠ s ∧ r * s - 2 * r + 1 ≠ 0 ∧ b = r * s * (r - 1) ∧ c = s * (r - 1) ∧ orderThirteenReducedPolynomial r s = 0

The forward rational change of variables from the Tate certificate to the reduced affine model, including the inverse identities needed to justify the substitution and the inherited noncuspidal conditions.

theorem MazurTorsion.Kubert.exists_tateOrderThirteen_certificate (E : WeierstrassCurve ℚ) [E.IsElliptic] (Q : (WeierstrassCurve.Affine.baseChange E ℚ).Point) (hQ : addOrderOf Q = 13) : ∃ (b : ℚ) (c : ℚ) (u : ℚ) (r : ℚ) (s : ℚ), u ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ b ≠ c ∧ c ^ 2 + c - b ≠ 0 ∧ tateSixNumerator b c ≠ 0 ∧ tateSevenAux b c ≠ 0 ∧ orderThirteenPolynomial b c = 0 ∧ u ^ 12 * E.Δ = tateNormalDiscriminant b c ∧ r = b / c ∧ s = c ^ 2 / (b - c) ∧ r ≠ 0 ∧ r ≠ 1 ∧ s ≠ 0 ∧ s ≠ 1 ∧ r ≠ s ∧ r * s - 2 * r + 1 ≠ 0 ∧ b = r * s * (r - 1) ∧ c = s * (r - 1) ∧ orderThirteenReducedPolynomial r s = 0

An exact rational point of order 13 produces both the denominator-safe Tate certificate and a noncuspidal rational point on the reduced affine X₁(13) model.