Reduction of a point of order fourteen

An exact rational point of order 14 can be put in Tate normal form. The checked addition recurrence computes its sixth and seventh multiples. Since the seventh multiple has order 2, its coordinates satisfy

2 * y(7P) + (1-c) * x(7P) - b = 0.

Clearing precisely the denominators introduced by the recurrence gives orderFourteenPolynomial. This file proves only this forward reduction, retaining all denominator conditions and the discriminant scale. It makes no assertion about the rational points of the resulting genus-one parameter curve.

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

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

Equations

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

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

An auxiliary numerator in the coordinates of 7P.

Equations

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

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

The numerator in the denominator-safe formula for y(7P).

Equations

• MazurTorsion.Kubert.tateSevenYNumerator b c = b ^ 3 - 3 * b ^ 2 * c + b * c ^ 3 + 3 * b * c ^ 2 - c ^ 5 - c ^ 4 - c ^ 3

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

The recurrence-defined X-coordinate of 7P.

Equations

• MazurTorsion.Kubert.tateSevenX b c = MazurTorsion.Kubert.tateNextX b c (MazurTorsion.Kubert.tateSixX b c) (MazurTorsion.Kubert.tateSixY b c)

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

The recurrence-defined Y-coordinate of 7P.

Equations

• MazurTorsion.Kubert.tateSevenY b c = MazurTorsion.Kubert.tateNextY b c (MazurTorsion.Kubert.tateSixX b c) (MazurTorsion.Kubert.tateSixY b c)

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

The affine Tate-parameter equation forced by exact order 14.

Writing

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

the equation is 2bA²D - (1-c)cACB - B³ = 0. It is the numerator of 2y(7P) + (1-c)x(7P) - b after multiplication by B³ / b.

Equations

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

theorem MazurTorsion.Kubert.tateSixX_eq_reduced (b c : ℚ) (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (hfiveNumerator : c ^ 2 + c - b ≠ 0) : tateSixX b c = (b - c) * tateSixNumerator b c / (c ^ 2 + c - b) ^ 2

theorem MazurTorsion.Kubert.tateSixY_eq_reduced (b c : ℚ) (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (hfiveNumerator : c ^ 2 + c - b ≠ 0) : tateSixY b c = -c * (b - c) ^ 2 * tateSevenAux b c / (c ^ 2 + c - b) ^ 3

theorem MazurTorsion.Kubert.tateSevenX_eq_reduced (b c : ℚ) (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (hfiveNumerator : c ^ 2 + c - b ≠ 0) (hsixNumerator : tateSixNumerator b c ≠ 0) : tateSevenX b c = -b * c * (c ^ 2 + c - b) * tateSevenAux b c / tateSixNumerator b c ^ 2

theorem MazurTorsion.Kubert.tateSevenY_eq_reduced (b c : ℚ) (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (hfiveNumerator : c ^ 2 + c - b ≠ 0) (hsixNumerator : tateSixNumerator b c ≠ 0) : tateSevenY b c = b ^ 2 * (c ^ 2 + c - b) ^ 2 * tateSevenYNumerator b c / tateSixNumerator b c ^ 3

theorem MazurTorsion.Kubert.seven_nsmul_origin_coordinates (b c : ℚ) (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (hfiveNumerator : c ^ 2 + c - b ≠ 0) (hsixNumerator : tateSixNumerator b c ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) : ∃ (h₇ : (tateNormalCurve b c).toAffine.Nonsingular (tateSevenX b c) (tateSevenY b c)), 7 • WeierstrassCurve.Affine.Point.some 0 0 h00 = WeierstrassCurve.Affine.Point.some (tateSevenX b c) (tateSevenY b c) h₇

Checked recurrence from 6P to 7P, with every denominator recorded.

theorem MazurTorsion.Kubert.orderFourteenPolynomial_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) = 14) : orderFourteenPolynomial b c = 0

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

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

An exact rational point of order 14 produces a point on the explicit Tate-parameter model of X₁(14). The four recurrence denominators, the next noncuspidal numerator, and the original discriminant scale are retained.

No classification of rational points on orderFourteenPolynomial b c = 0 is asserted here.