An explicit genus-two model attached to order eighteen

The order-nine Tate-parameter equation admits the rational parameter

d = c² / (b - c).

Away from the nondegenerate loci already supplied by exists_tateOrderEighteen_certificate, it gives

c = d²(d - 1) and b = c(d² - d + 1).

Combining this parametrization with the rational root of the Tate two-division polynomial gives the auxiliary equation

(2s + 1)(d²(d - 1)s² - (d² - d + 1)) = s².

The displayed rational change of variables then produces a point on

Y² = X⁶ - 4X⁵ + 10X⁴ - 10X³ + 5X² - 2X + 1.

This file proves only these algebraic reductions. In particular, it does not assert the rational-point classification of this genus-two curve.

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

The rational parameter on the nondegenerate order-nine Tate curve.

Equations

• MazurTorsion.Kubert.orderNineParameterD b c = c ^ 2 / (b - c)

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

The auxiliary coordinate obtained from a root of the Tate two-division polynomial.

Equations

• MazurTorsion.Kubert.orderEighteenAuxiliaryS b c r = ((1 - c) * r - b) / (2 * r * c)

def MazurTorsion.Kubert.orderEighteenAuxiliaryPolynomial (d s : ℚ) : ℚ

The equation in the order-nine parameter and the auxiliary two-division coordinate.

Equations

• MazurTorsion.Kubert.orderEighteenAuxiliaryPolynomial d s = (2 * s + 1) * (d ^ 2 * (d - 1) * s ^ 2 - (d ^ 2 - d + 1)) - s ^ 2

def MazurTorsion.Kubert.orderEighteenModelX (d s : ℚ) : ℚ

The abscissa in the standard genus-two model for X₁(18).

Equations

• MazurTorsion.Kubert.orderEighteenModelX d s = (d - s + 2 * d * s) / (1 + d * s)

def MazurTorsion.Kubert.orderEighteenModelY (d s : ℚ) : ℚ

The ordinate in the standard genus-two model for X₁(18).

Equations

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

def MazurTorsion.Kubert.orderEighteenHyperellipticPolynomial (X : ℚ) : ℚ

The sextic defining the standard genus-two model for X₁(18).

Equations

• MazurTorsion.Kubert.orderEighteenHyperellipticPolynomial X = X ^ 6 - 4 * X ^ 5 + 10 * X ^ 4 - 10 * X ^ 3 + 5 * X ^ 2 - 2 * X + 1

theorem MazurTorsion.Kubert.orderNinePolynomial_eq_difference_form (b c : ℚ) : orderNinePolynomial b c = c ^ 5 - (b - c) * c ^ 3 - (b - c) ^ 3

theorem MazurTorsion.Kubert.orderNineParameterD_ne_zero (b c : ℚ) (hc : c ≠ 0) (hbc : b ≠ c) : orderNineParameterD b c ≠ 0

theorem MazurTorsion.Kubert.orderNine_parameterization (b c : ℚ) (hc : c ≠ 0) (hbc : b ≠ c) (hnine : orderNinePolynomial b c = 0) : c = orderNineParameterD b c ^ 2 * (orderNineParameterD b c - 1) ∧ b = c * (orderNineParameterD b c ^ 2 - orderNineParameterD b c + 1)

The nondegenerate order-nine Tate equation has the claimed rational parametrization.

theorem MazurTorsion.Kubert.orderNineParameterD_ne_one (b c : ℚ) (hc : c ≠ 0) (hbc : b ≠ c) (hnine : orderNinePolynomial b c = 0) : orderNineParameterD b c ≠ 1

theorem MazurTorsion.Kubert.root_ne_zero_of_tateTwoDivisionPolynomial (b c r : ℚ) (hb : b ≠ 0) (htwo : tateTwoDivisionPolynomial b c r = 0) : r ≠ 0

theorem MazurTorsion.Kubert.orderEighteenAuxiliaryPolynomial_eq_zero (b c r d : ℚ) (hc : c ≠ 0) (hr : r ≠ 0) (hcparam : c = d ^ 2 * (d - 1)) (hbparam : b = c * (d ^ 2 - d + 1)) (htwo : tateTwoDivisionPolynomial b c r = 0) : orderEighteenAuxiliaryPolynomial d (orderEighteenAuxiliaryS b c r) = 0

After the order-nine parametrization, a root of the two-division polynomial gives the displayed auxiliary equation.

theorem MazurTorsion.Kubert.one_add_mul_ne_zero_of_orderEighteenAuxiliary (d s : ℚ) (hd : d ≠ 0) (hd1 : d ≠ 1) (haux : orderEighteenAuxiliaryPolynomial d s = 0) : 1 + d * s ≠ 0

The denominator in the genus-two change of variables cannot vanish on the nondegenerate auxiliary curve.

theorem MazurTorsion.Kubert.orderEighteenModel_equation (d s : ℚ) (hden : 1 + d * s ≠ 0) (haux : orderEighteenAuxiliaryPolynomial d s = 0) : orderEighteenModelY d s ^ 2 = orderEighteenHyperellipticPolynomial (orderEighteenModelX d s)

The rational change of variables sends the auxiliary equation to the standard sextic model.

theorem MazurTorsion.Kubert.orderEighteenModelX_ne_zero (d s : ℚ) (hd1 : d ≠ 1) (hden : 1 + d * s ≠ 0) (haux : orderEighteenAuxiliaryPolynomial d s = 0) : orderEighteenModelX d s ≠ 0

A nondegenerate point of the auxiliary curve does not map to the affine point with abscissa zero.

theorem MazurTorsion.Kubert.orderEighteenModelX_ne_one (d s : ℚ) (hd : d ≠ 0) (hd1 : d ≠ 1) (hden : 1 + d * s ≠ 0) (haux : orderEighteenAuxiliaryPolynomial d s = 0) : orderEighteenModelX d s ≠ 1

A nondegenerate point of the auxiliary curve does not map to the affine point with abscissa one.

theorem MazurTorsion.Kubert.exists_orderEighteen_genusTwo_certificate (E : WeierstrassCurve ℚ) [E.IsElliptic] (Q : (WeierstrassCurve.Affine.baseChange E ℚ).Point) (hQ : addOrderOf Q = 18) : ∃ (b : ℚ) (c : ℚ) (u : ℚ) (r : ℚ) (d : ℚ) (s : ℚ), u ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ b ≠ c ∧ r ≠ 0 ∧ d = orderNineParameterD b c ∧ d ≠ 0 ∧ d ≠ 1 ∧ c = d ^ 2 * (d - 1) ∧ b = c * (d ^ 2 - d + 1) ∧ s = orderEighteenAuxiliaryS b c r ∧ orderNinePolynomial b c = 0 ∧ tateTwoDivisionPolynomial b c r = 0 ∧ orderEighteenAuxiliaryPolynomial d s = 0 ∧ 1 + d * s ≠ 0 ∧ orderEighteenModelX d s ≠ 0 ∧ orderEighteenModelX d s ≠ 1 ∧ orderEighteenModelY d s ^ 2 = orderEighteenHyperellipticPolynomial (orderEighteenModelX d s) ∧ u ^ 12 * E.Δ = (tateNormalCurve b c).Δ

A point of exact order eighteen supplies a nondegenerate rational point on the explicit genus-two model, together with all Tate parameters, denominator conditions, source equations, and the original discriminant scale.

This is only a reduction theorem. It does not classify the rational points of the genus-two curve.

theorem MazurTorsion.Kubert.rationalPoint_addOrderOf_ne_eighteen_of_noNoncuspidalPoint (E : WeierstrassCurve ℚ) [E.IsElliptic] (Q : (WeierstrassCurve.Affine.baseChange E ℚ).Point) (hNoNoncuspidal : ∀ (x y : ℚ), x ≠ 0 → x ≠ 1 → y ^ 2 = orderEighteenHyperellipticPolynomial x → False) : addOrderOf Q ≠ 18

A route-neutral exclusion of noncuspidal rational points on the hyperelliptic model rules out exact rational order eighteen.