Explicit descent interfaces for X₁(13)

The order-thirteen parameter curve is the genus-two sextic

y² = x⁶ + 2x⁵ + x⁴ + 2x³ + 6x² + 4x + 1.

This file records algebraic inputs to the classical Mazur--Tate 19-isogeny descent which can be checked without a genus-two Jacobian implementation.

The rational transformation

(x,y) ↦ (-1/(x+1), y/(x+1)³)

preserves the sextic and has cube equal to the hyperelliptic involution. The quotient by its order-three square is the conic

v² = u² + 2u + 5.

We parameterize this conic, identify the cyclic cubic fiber, and homogenize its square discriminant. The discriminant factor is an explicit norm in the quadratic order generated by a primitive sixth root. In that order, 19=(3+2ρ)(5-2ρ); coordinate divisibility criteria for both primes above 19 are proved below.

We also give an explicit polynomial Pell identity of degrees 19 and 16. It is the algebraic function-field certificate underlying the order-19 difference of the two rational points at infinity.

The file does not construct the Jacobian, divisor classes, the induced endomorphism π, fppf cohomology, or the Abel--Jacobi embedding. Consequently it does not assert rank zero or a classification of rational points.

The rational order-six symmetry

def MazurTorsion.XOneThirteenDescent.diamondX (x : ℚ) : ℚ

The abscissa of the diamond-operator symmetry.

Equations

• MazurTorsion.XOneThirteenDescent.diamondX x = -1 / (x + 1)

def MazurTorsion.XOneThirteenDescent.diamondY (x y : ℚ) : ℚ

The corresponding ordinate transformation.

Equations

• MazurTorsion.XOneThirteenDescent.diamondY x y = y / (x + 1) ^ 3

theorem MazurTorsion.XOneThirteenDescent.diamond_sextic_covariance (x : ℚ) (hxneg : x ≠ -1) : (x + 1) ^ 6 * Kubert.orderThirteenHyperellipticPolynomial (diamondX x) = Kubert.orderThirteenHyperellipticPolynomial x

Covariance of the sextic under the fractional-linear abscissa transformation.

theorem MazurTorsion.XOneThirteenDescent.diamond_preserves_curve (x y : ℚ) (hxneg : x ≠ -1) (hcurve : y ^ 2 = Kubert.orderThirteenHyperellipticPolynomial x) : diamondY x y ^ 2 = Kubert.orderThirteenHyperellipticPolynomial (diamondX x)

The diamond operator preserves the affine sextic away from the chart boundary x=-1.

theorem MazurTorsion.XOneThirteenDescent.diamondX_sq (x : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) : diamondX (diamondX x) = -(x + 1) / x

The second abscissa iterate in denominator-safe form.

theorem MazurTorsion.XOneThirteenDescent.diamondX_cube (x : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) : diamondX (diamondX (diamondX x)) = x

The fractional-linear abscissa has order three.

theorem MazurTorsion.XOneThirteenDescent.diamondY_sq (x y : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) : diamondY (diamondX x) (diamondY x y) = y / x ^ 3

The second ordinate iterate in denominator-safe form.

theorem MazurTorsion.XOneThirteenDescent.diamondY_cube (x y : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) : diamondY (diamondX (diamondX x)) (diamondY (diamondX x) (diamondY x y)) = -y

The cube of the lifted symmetry is the hyperelliptic involution.

theorem MazurTorsion.XOneThirteenDescent.diamondY_cube_ne (x y : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) (hy : y ≠ 0) : diamondY (diamondX (diamondX x)) (diamondY (diamondX x) (diamondY x y)) ≠ y

At a point with nonzero ordinate, the third iterate is not the identity; together with the preceding formulas this certifies the order-six lift.

Quotient conic and cyclic cubic fiber

def MazurTorsion.XOneThirteenDescent.quotientU (x : ℚ) : ℚ

The trace invariant of the three-element abscissa orbit.

Equations

• MazurTorsion.XOneThirteenDescent.quotientU x = (x ^ 3 - 3 * x - 1) / (x * (x + 1))

def MazurTorsion.XOneThirteenDescent.quotientV (x y : ℚ) : ℚ

The ordinate invariant for the order-three square.

Equations

• MazurTorsion.XOneThirteenDescent.quotientV x y = y / (x * (x + 1))

theorem MazurTorsion.XOneThirteenDescent.quotientU_diamond (x : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) : quotientU (diamondX x) = quotientU x

The abscissa invariant is fixed by the order-six symmetry.

theorem MazurTorsion.XOneThirteenDescent.quotientV_diamond (x y : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) : quotientV (diamondX x) (diamondY x y) = -quotientV x y

The ordinate invariant changes sign under the order-six lift and is therefore fixed by its square.

theorem MazurTorsion.XOneThirteenDescent.quotient_conic_equation (x y : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) (hcurve : y ^ 2 = Kubert.orderThirteenHyperellipticPolynomial x) : quotientV x y ^ 2 = quotientU x ^ 2 + 2 * quotientU x + 5

On the sextic, the two invariant functions lie on a rational conic.

def MazurTorsion.XOneThirteenDescent.conicU (t : ℚ) : ℚ

The conic abscissa obtained from a line through (u,v)=(-1,2).

Equations

• MazurTorsion.XOneThirteenDescent.conicU t = (t ^ 2 + 4 * t - 1) / (1 - t ^ 2)

def MazurTorsion.XOneThirteenDescent.conicV (t : ℚ) : ℚ

The corresponding conic ordinate.

Equations

• MazurTorsion.XOneThirteenDescent.conicV t = 2 * (1 + t ^ 2) / (1 - t ^ 2)

theorem MazurTorsion.XOneThirteenDescent.conic_parameter_equation (t : ℚ) (ht : t ^ 2 ≠ 1) : conicV t ^ 2 = conicU t ^ 2 + 2 * conicU t + 5

The displayed parametrization lies on the quotient conic.

def MazurTorsion.XOneThirteenDescent.conicSlope (u v : ℚ) : ℚ

The slope recovering the conic parameter away from u=-1.

Equations

• MazurTorsion.XOneThirteenDescent.conicSlope u v = (v - 2) / (u + 1)

theorem MazurTorsion.XOneThirteenDescent.conic_parameter_inverse (u v : ℚ) (hu : u ≠ -1) (hconic : v ^ 2 = u ^ 2 + 2 * u + 5) : have t := conicSlope u v; t ^ 2 ≠ 1 ∧ conicU t = u ∧ conicV t = v

The slope construction recovers both conic coordinates away from the exceptional fiber u=-1.

theorem MazurTorsion.XOneThirteenDescent.conic_at_neg_one_iff (v : ℚ) : v ^ 2 = (-1) ^ 2 + 2 * -1 + 5 ↔ v = 2 ∨ v = -2

The exceptional conic fiber over u=-1 consists of v=±2.

theorem MazurTorsion.XOneThirteenDescent.conic_rational_parameterization (u v : ℚ) (hconic : v ^ 2 = u ^ 2 + 2 * u + 5) : u = -1 ∧ (v = 2 ∨ v = -2) ∨ ∃ (t : ℚ), t ^ 2 ≠ 1 ∧ conicU t = u ∧ conicV t = v

Every rational affine point on the quotient conic is either one of the two exceptional points over u=-1 or lies in the displayed one-parameter family.

def MazurTorsion.XOneThirteenDescent.fiberCubic (u z : ℚ) : ℚ

The cyclic cubic above a quotient abscissa.

Equations

• MazurTorsion.XOneThirteenDescent.fiberCubic u z = z ^ 3 - u * z ^ 2 - (u + 3) * z - 1

theorem MazurTorsion.XOneThirteenDescent.fiberCubic_neg_one_ne_zero (x : ℚ) : fiberCubic (-1) x ≠ 0

The exceptional quotient fiber u=-1 has no rational abscissa.

theorem MazurTorsion.XOneThirteenDescent.fiberCubic_quotientU (x : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) : fiberCubic (quotientU x) x = 0

The invariant abscissa of a noncuspidal point satisfies its cubic fiber equation.

theorem MazurTorsion.XOneThirteenDescent.quotientU_ne_neg_one (x : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) : quotientU x ≠ -1

A noncuspidal rational abscissa does not lie over the exceptional quotient value u=-1.

def MazurTorsion.XOneThirteenDescent.orbitNorm (x z : ℚ) : ℚ

Product over the three-element abscissa orbit.

Equations

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

theorem MazurTorsion.XOneThirteenDescent.orbitNorm_eq_fiberCubic (x z : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) : orbitNorm x z = fiberCubic (quotientU x) z

The orbit norm is the cyclic cubic fiber polynomial.

def MazurTorsion.XOneThirteenDescent.cubicDiscriminant (a b c d : ℚ) : ℚ

The standard coefficient discriminant of a cubic a z³+b z²+c z+d.

Equations

• MazurTorsion.XOneThirteenDescent.cubicDiscriminant a b c d = b ^ 2 * c ^ 2 - 4 * a * c ^ 3 - 4 * b ^ 3 * d - 27 * a ^ 2 * d ^ 2 + 18 * a * b * c * d

theorem MazurTorsion.XOneThirteenDescent.fiberCubic_discriminant (u : ℚ) : cubicDiscriminant 1 (-u) (-(u + 3)) (-1) = (u ^ 2 + 3 * u + 9) ^ 2

The cyclic cubic fiber has square discriminant.

def MazurTorsion.XOneThirteenDescent.clearedFiber (t z : ℚ) : ℚ

The conic-parameterized cubic with its denominator cleared.

Equations

• MazurTorsion.XOneThirteenDescent.clearedFiber t z = (1 - t ^ 2) * z ^ 3 - (t ^ 2 + 4 * t - 1) * z ^ 2 + (2 * t ^ 2 - 4 * t - 2) * z + (t ^ 2 - 1)

theorem MazurTorsion.XOneThirteenDescent.clearedFiber_eq_mul_fiberCubic (t z : ℚ) (ht : t ^ 2 ≠ 1) : clearedFiber t z = (1 - t ^ 2) * fiberCubic (conicU t) z

Clearing the conic denominator produces clearedFiber.

theorem MazurTorsion.XOneThirteenDescent.clearedFiber_eq_zero (t z : ℚ) (ht : t ^ 2 ≠ 1) (hroot : fiberCubic (conicU t) z = 0) : clearedFiber t z = 0

A root of the parameterized fiber is a root of the cleared cubic.

def MazurTorsion.XOneThirteenDescent.parameterDiscriminant (t : ℚ) : ℚ

The square root of the cleared cubic discriminant.

Equations

• MazurTorsion.XOneThirteenDescent.parameterDiscriminant t = 7 * t ^ 4 - 4 * t ^ 3 + 2 * t ^ 2 + 4 * t + 7

theorem MazurTorsion.XOneThirteenDescent.clearedFiber_discriminant (t : ℚ) : cubicDiscriminant (1 - t ^ 2) (-(t ^ 2 + 4 * t - 1)) (2 * t ^ 2 - 4 * t - 2) (t ^ 2 - 1) = parameterDiscriminant t ^ 2

The cleared cubic still has square discriminant, now with an integral quartic square root.

theorem MazurTorsion.XOneThirteenDescent.fiber_discriminant_parameter_factorization (t : ℚ) (ht : t ^ 2 ≠ 1) : conicU t ^ 2 + 3 * conicU t + 9 = parameterDiscriminant t / (1 - t ^ 2) ^ 2

The unscaled discriminant factor after conic parametrization.

def MazurTorsion.XOneThirteenDescent.homogeneousFiber (m n z : ℚ) : ℚ

Homogeneous form of the parameterized cyclic cubic.

Equations

• MazurTorsion.XOneThirteenDescent.homogeneousFiber m n z = (n ^ 2 - m ^ 2) * z ^ 3 - (m ^ 2 + 4 * m * n - n ^ 2) * z ^ 2 + (2 * m ^ 2 - 4 * m * n - 2 * n ^ 2) * z + (m ^ 2 - n ^ 2)

theorem MazurTorsion.XOneThirteenDescent.homogeneousFiber_eq_den_sq_mul (m n z : ℚ) (hn : n ≠ 0) : homogeneousFiber m n z = n ^ 2 * clearedFiber (m / n) z

Substitution t=m/n turns the cleared cubic into its homogeneous form after multiplication by n².

def MazurTorsion.XOneThirteenDescent.homogeneousDiscriminant (m n : ℚ) : ℚ

The homogeneous quartic discriminant factor.

Equations

• MazurTorsion.XOneThirteenDescent.homogeneousDiscriminant m n = 7 * m ^ 4 - 4 * m ^ 3 * n + 2 * m ^ 2 * n ^ 2 + 4 * m * n ^ 3 + 7 * n ^ 4

theorem MazurTorsion.XOneThirteenDescent.homogeneousFiber_discriminant (m n : ℚ) : cubicDiscriminant (n ^ 2 - m ^ 2) (-(m ^ 2 + 4 * m * n - n ^ 2)) (2 * m ^ 2 - 4 * m * n - 2 * n ^ 2) (m ^ 2 - n ^ 2) = homogeneousDiscriminant m n ^ 2

Discriminant of the homogeneous cubic.

theorem MazurTorsion.XOneThirteenDescent.noncuspidal_curve_parameterization (x y : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) (hcurve : y ^ 2 = Kubert.orderThirteenHyperellipticPolynomial x) : ∃ (t : ℚ), t ^ 2 ≠ 1 ∧ conicU t = quotientU x ∧ conicV t = quotientV x y ∧ clearedFiber t x = 0

Every noncuspidal rational point on the sextic admits an explicit conic parameter and satisfies the cleared cyclic cubic.

theorem MazurTorsion.XOneThirteenDescent.noncuspidal_curve_primitive_parameterization (x y : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) (hcurve : y ^ 2 = Kubert.orderThirteenHyperellipticPolynomial x) : ∃ (m : ℤ) (n : ℤ), 0 < n ∧ IsCoprime m n ∧ (↑m / ↑n) ^ 2 ≠ 1 ∧ conicU (↑m / ↑n) = quotientU x ∧ conicV (↑m / ↑n) = quotientV x y ∧ homogeneousFiber (↑m) (↑n) x = 0

The canonical numerator and denominator of the conic parameter give primitive homogeneous integer data.

The split prime above 19

def MazurTorsion.XOneThirteenDescent.sixthRootMul (z w : ℤ × ℤ) : ℤ × ℤ

Multiplication in coordinates a+bρ, where ρ²-ρ+1=0.

Equations

• MazurTorsion.XOneThirteenDescent.sixthRootMul z w = (z.1 * w.1 - z.2 * w.2, z.1 * w.2 + z.2 * w.1 + z.2 * w.2)

def MazurTorsion.XOneThirteenDescent.sixthRootNorm (z : ℤ × ℤ) : ℤ

The norm in the quadratic order generated by ρ.

Equations

• MazurTorsion.XOneThirteenDescent.sixthRootNorm z = z.1 ^ 2 + z.1 * z.2 + z.2 ^ 2

def MazurTorsion.XOneThirteenDescent.sixthRootRho : ℤ × ℤ

The distinguished primitive sixth root in coordinates.

Equations

• MazurTorsion.XOneThirteenDescent.sixthRootRho = (0, 1)

theorem MazurTorsion.XOneThirteenDescent.sixthRootRho_relation : sixthRootMul sixthRootRho sixthRootRho - sixthRootRho + (1, 0) = (0, 0)

Coordinate form of the relation ρ²-ρ+1=0.

theorem MazurTorsion.XOneThirteenDescent.sixthRootNorm_mul (z w : ℤ × ℤ) : sixthRootNorm (sixthRootMul z w) = sixthRootNorm z * sixthRootNorm w

The coordinate norm is multiplicative.

theorem MazurTorsion.XOneThirteenDescent.sixthRootCube_coordinates (a b : ℤ) : sixthRootMul (sixthRootMul (a, b) (a, b)) (a, b) = (a ^ 3 - 3 * a * b ^ 2 - b ^ 3, 3 * (a * b * (a + b)))

The two coordinates of a cube in the sixth-root order. These are exactly the three root factors and trace form occurring in the split cyclic cubic.

def MazurTorsion.XOneThirteenDescent.sixthRootConj (z : ℤ × ℤ) : ℤ × ℤ

Conjugation sends ρ to 1-ρ.

Equations

• MazurTorsion.XOneThirteenDescent.sixthRootConj z = (z.1 + z.2, -z.2)

theorem MazurTorsion.XOneThirteenDescent.sixthRootMul_conj (z : ℤ × ℤ) : sixthRootMul z (sixthRootConj z) = (sixthRootNorm z, 0)

Multiplication by the conjugate gives the rational integer norm.

theorem MazurTorsion.XOneThirteenDescent.sixthRootNorm_conj (z : ℤ × ℤ) : sixthRootNorm (sixthRootConj z) = sixthRootNorm z

Conjugation preserves the norm.

def MazurTorsion.XOneThirteenDescent.sixthRootPi : ℤ × ℤ

A prime above 19, represented by π=3+2ρ.

Equations

• MazurTorsion.XOneThirteenDescent.sixthRootPi = (3, 2)

theorem MazurTorsion.XOneThirteenDescent.sixthRootNorm_pi : sixthRootNorm sixthRootPi = 19

Its norm is 19.

theorem MazurTorsion.XOneThirteenDescent.sixthRootConj_pi : sixthRootConj sixthRootPi = (5, -2)

The conjugate prime is conj(π)=5-2ρ.

theorem MazurTorsion.XOneThirteenDescent.nineteen_eq_pi_mul_conj : sixthRootMul sixthRootPi (sixthRootConj sixthRootPi) = (19, 0)

Coordinate factorization 19=π·conj(π).

def MazurTorsion.XOneThirteenDescent.SixthRootPiDivides (z : ℤ × ℤ) : Prop

Divisibility by π in sixth-root coordinates.

Equations

• MazurTorsion.XOneThirteenDescent.SixthRootPiDivides z = ∃ (w : ℤ × ℤ), MazurTorsion.XOneThirteenDescent.sixthRootMul MazurTorsion.XOneThirteenDescent.sixthRootPi w = z

theorem MazurTorsion.XOneThirteenDescent.sixthRootPiDivides_iff (a b : ℤ) : SixthRootPiDivides (a, b) ↔ 19 ∣ 5 * a + 2 * b

Multiplication by π cuts out the index-19 lattice 5a+2b ≡ 0 mod 19.

def MazurTorsion.XOneThirteenDescent.SixthRootPiConjDivides (z : ℤ × ℤ) : Prop

Divisibility by the conjugate prime.

Equations

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

theorem MazurTorsion.XOneThirteenDescent.sixthRootPiConjDivides_iff (a b : ℤ) : SixthRootPiConjDivides (a, b) ↔ 19 ∣ 3 * a - 2 * b

Multiplication by conj(π) cuts out the conjugate index-19 lattice 3a-2b ≡ 0 mod 19.

theorem MazurTorsion.XOneThirteenDescent.nineteen_dvd_sixthRootNorm_of_piDivides (z : ℤ × ℤ) (hz : SixthRootPiDivides z) : 19 ∣ sixthRootNorm z

A factor of π forces a factor of 19 in the norm.

theorem MazurTorsion.XOneThirteenDescent.nineteen_dvd_sixthRootNorm_of_piConjDivides (z : ℤ × ℤ) (hz : SixthRootPiConjDivides z) : 19 ∣ sixthRootNorm z

The same norm consequence for conj(π).

theorem MazurTorsion.XOneThirteenDescent.piDivides_or_piConjDivides_of_nineteen_dvd_norm (a b : ℤ) (hnorm : 19 ∣ sixthRootNorm (a, b)) : SixthRootPiDivides (a, b) ∨ SixthRootPiConjDivides (a, b)

Conversely, every factor of 19 in a sixth-root norm comes from one of the two primes above 19.

The homogeneous discriminant as a split norm

def MazurTorsion.XOneThirteenDescent.parameterNormCoordinates (m n : ℤ) : ℤ × ℤ

Sixth-root coordinates for the homogeneous discriminant factor.

Equations

• MazurTorsion.XOneThirteenDescent.parameterNormCoordinates m n = (m ^ 2 + 4 * m * n - n ^ 2, 3 * (n ^ 2 - m ^ 2))

def MazurTorsion.XOneThirteenDescent.integerHomogeneousDiscriminant (m n : ℤ) : ℤ

Integral homogeneous discriminant factor.

Equations

• MazurTorsion.XOneThirteenDescent.integerHomogeneousDiscriminant m n = 7 * m ^ 4 - 4 * m ^ 3 * n + 2 * m ^ 2 * n ^ 2 + 4 * m * n ^ 3 + 7 * n ^ 4

theorem MazurTorsion.XOneThirteenDescent.parameter_discriminant_is_norm (m n : ℤ) : sixthRootNorm (parameterNormCoordinates m n) = integerHomogeneousDiscriminant m n

The homogeneous discriminant factor is a sixth-root norm.

theorem MazurTorsion.XOneThirteenDescent.integerHomogeneousDiscriminant_cast (m n : ℤ) : ↑(integerHomogeneousDiscriminant m n) = homogeneousDiscriminant ↑m ↑n

The rational and integral presentations of the homogeneous discriminant agree under coercion.

theorem MazurTorsion.XOneThirteenDescent.primitive_parameter_not_piConj_factor (m n : ℤ) (hcoprime : IsCoprime m n) : ¬SixthRootPiConjDivides (parameterNormCoordinates m n)

The primitive parameter norm is oriented away from conj(π), not merely away from simultaneous divisibility by the two primes over 19. The conjugate branch is an anisotropic binary quadratic form modulo 19.

theorem MazurTorsion.XOneThirteenDescent.primitive_parameter_not_both_pi_factors (m n : ℤ) (hcoprime : IsCoprime m n) : ¬(SixthRootPiDivides (parameterNormCoordinates m n) ∧ SixthRootPiConjDivides (parameterNormCoordinates m n))

For primitive integer parameters, the discriminant norm coordinate cannot be divisible by both primes above 19.

Rational-root divisibility and the primitive norm equation

theorem MazurTorsion.XOneThirteenDescent.root_orbit_product_dvd_leadingCoefficient (m n a b : ℤ) (hab : IsCoprime a b) (hroot : homogeneousFiber (↑m) (↑n) (↑a / ↑b) = 0) (hb : b ≠ 0) : a * b * (a + b) ∣ n ^ 2 - m ^ 2

If a primitive rational number a/b is a root of the homogeneous cyclic cubic, then the three pairwise-coprime cusp factors in its Möbius orbit divide the leading coefficient together.

theorem MazurTorsion.XOneThirteenDescent.integerDiscriminant_mul_orbitNorm_sq (m n a b : ℤ) (hn : n ≠ 0) (hb : b ≠ 0) (ha : a ≠ 0) (hasum : a + b ≠ 0) (ht : (↑m / ↑n) ^ 2 ≠ 1) (hU : conicU (↑m / ↑n) = quotientU (↑a / ↑b)) : integerHomogeneousDiscriminant m n * (a * b * (a + b)) ^ 2 = (n ^ 2 - m ^ 2) ^ 2 * (a ^ 2 + a * b + b ^ 2) ^ 3

Equating the parameter and orbit presentations of the cyclic-cubic discriminant gives an integral norm equation.

theorem MazurTorsion.XOneThirteenDescent.exists_root_leadingCoefficient_quotient (m n a b : ℤ) (hn : n ≠ 0) (hb : b ≠ 0) (ha : a ≠ 0) (hasum : a + b ≠ 0) (ht : (↑m / ↑n) ^ 2 ≠ 1) (hU : conicU (↑m / ↑n) = quotientU (↑a / ↑b)) (hdvd : a * b * (a + b) ∣ n ^ 2 - m ^ 2) : ∃ (k : ℤ), n ^ 2 - m ^ 2 = k * (a * b * (a + b)) ∧ integerHomogeneousDiscriminant m n = k ^ 2 * (a ^ 2 + a * b + b ^ 2) ^ 3

Dividing by the nonzero product of the cusp factors turns the discriminant identity into a square times an Eisenstein norm cube.

theorem MazurTorsion.XOneThirteenDescent.root_split_coefficient_identities (m n a b k : ℤ) (hn : n ≠ 0) (hb : b ≠ 0) (ha : a ≠ 0) (hasum : a + b ≠ 0) (ht : (↑m / ↑n) ^ 2 ≠ 1) (hU : conicU (↑m / ↑n) = quotientU (↑a / ↑b)) (hk : n ^ 2 - m ^ 2 = k * (a * b * (a + b))) : m ^ 2 + 4 * m * n - n ^ 2 = k * (a ^ 3 - 3 * a * b ^ 2 - b ^ 3) ∧ 2 * m ^ 2 - 4 * m * n - 2 * n ^ 2 = k * (-a ^ 3 - 3 * a ^ 2 * b + b ^ 3)

Once the leading coefficient has been divided by the three cusp factors, the invariant equality determines the other two coefficients of the split cyclic cubic.

theorem MazurTorsion.XOneThirteenDescent.split_root_not_piConj_factor (m n a b k : ℤ) (hmn : IsCoprime m n) (hk : n ^ 2 - m ^ 2 = k * (a * b * (a + b))) (htrace : m ^ 2 + 4 * m * n - n ^ 2 = k * (a ^ 3 - 3 * a * b ^ 2 - b ^ 3)) : ¬SixthRootPiConjDivides (a, b)

In any primitive split fiber, the root coordinate is oriented away from the conjugate prime above 19. Cubing preserves conjugate-prime divisibility, while the two coefficient identities identify that cube, up to the rational integer k, with the primitive parameter norm.

theorem MazurTorsion.XOneThirteenDescent.split_parameters_odd (m n a b k : ℤ) (hmn : IsCoprime m n) (hab : IsCoprime a b) (hk : n ^ 2 - m ^ 2 = k * (a * b * (a + b))) (htrace : m ^ 2 + 4 * m * n - n ^ 2 = k * (a ^ 3 - 3 * a * b ^ 2 - b ^ 3)) (hpair : 2 * m ^ 2 - 4 * m * n - 2 * n ^ 2 = k * (-a ^ 3 - 3 * a ^ 2 * b + b ^ 3)) : Odd m ∧ Odd n

Primitive split-fiber parameters are odd. Modulo two, every other primitive parameter class gives a cyclic cubic without a root.

theorem MazurTorsion.XOneThirteenDescent.split_parameter_resultant_identities (m n : ℤ) : (-4 * m + n) * (n ^ 2 - m ^ 2) + n * (m ^ 2 + 4 * m * n - n ^ 2) = 4 * m ^ 3 ∧ (m + 4 * n) * (n ^ 2 - m ^ 2) + m * (m ^ 2 + 4 * m * n - n ^ 2) = 4 * n ^ 3

The leading and trace parameter forms have resultant four.

theorem MazurTorsion.XOneThirteenDescent.split_quotient_divisibility (m n a b k : ℤ) (hmn : IsCoprime m n) (hab : IsCoprime a b) (hk : n ^ 2 - m ^ 2 = k * (a * b * (a + b))) (htrace : m ^ 2 + 4 * m * n - n ^ 2 = k * (a ^ 3 - 3 * a * b ^ 2 - b ^ 3)) (hpair : 2 * m ^ 2 - 4 * m * n - 2 * n ^ 2 = k * (-a ^ 3 - 3 * a ^ 2 * b + b ^ 3)) : Odd m ∧ Odd n ∧ 4 ∣ k ∧ ¬8 ∣ k ∧ k ∣ 4

For a primitive split fiber, the remaining quotient divides four and has exact two-adic valuation two.

theorem MazurTorsion.XOneThirteenDescent.split_quotient_eq_neg_four_or_four (m n a b k : ℤ) (hmn : IsCoprime m n) (hab : IsCoprime a b) (hk : n ^ 2 - m ^ 2 = k * (a * b * (a + b))) (htrace : m ^ 2 + 4 * m * n - n ^ 2 = k * (a ^ 3 - 3 * a * b ^ 2 - b ^ 3)) (hpair : 2 * m ^ 2 - 4 * m * n - 2 * n ^ 2 = k * (-a ^ 3 - 3 * a ^ 2 * b + b ^ 3)) : k = -4 ∨ k = 4

The quotient of a primitive split cyclic cubic is exactly 4 up to sign.

theorem MazurTorsion.XOneThirteenDescent.noncuspidal_curve_primitive_split_descent_data (x y : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) (hcurve : y ^ 2 = Kubert.orderThirteenHyperellipticPolynomial x) : ∃ (m : ℤ) (n : ℤ) (a : ℤ) (b : ℤ) (k : ℤ), 0 < n ∧ 0 < b ∧ IsCoprime m n ∧ IsCoprime a b ∧ ↑a / ↑b = x ∧ a ≠ 0 ∧ a + b ≠ 0 ∧ (↑m / ↑n) ^ 2 ≠ 1 ∧ conicU (↑m / ↑n) = quotientU (↑a / ↑b) ∧ conicV (↑m / ↑n) = quotientV x y ∧ homogeneousFiber (↑m) (↑n) (↑a / ↑b) = 0 ∧ n ^ 2 - m ^ 2 = k * (a * b * (a + b)) ∧ integerHomogeneousDiscriminant m n = k ^ 2 * (a ^ 2 + a * b + b ^ 2) ^ 3 ∧ ¬(SixthRootPiDivides (parameterNormCoordinates m n) ∧ SixthRootPiConjDivides (parameterNormCoordinates m n))

The complete explicit descent data obtained from a noncuspidal rational point. It includes primitive coordinates for both quotient and fiber parameters, the exact leading-coefficient quotient, and the resulting square-times-cube norm equation.

theorem MazurTorsion.XOneThirteenDescent.noncuspidal_curve_primitive_descent_data (x y : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) (hcurve : y ^ 2 = Kubert.orderThirteenHyperellipticPolynomial x) : ∃ (m : ℤ) (n : ℤ), 0 < n ∧ IsCoprime m n ∧ (↑m / ↑n) ^ 2 ≠ 1 ∧ conicU (↑m / ↑n) = quotientU x ∧ conicV (↑m / ↑n) = quotientV x y ∧ homogeneousFiber (↑m) (↑n) x = 0 ∧ ¬(SixthRootPiDivides (parameterNormCoordinates m n) ∧ SixthRootPiConjDivides (parameterNormCoordinates m n))

The original primitive conic-parameter package, retained as a stable projection of the stronger split-cubic descent data.

def MazurTorsion.XOneThirteenDescent.PrimitiveCyclicCubicObstruction : Prop

The residual integral statement after quotienting by the diamond symmetry and applying rational-root divisibility.

Equations

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

def MazurTorsion.XOneThirteenDescent.FiniteSplitCyclicCubicObstruction : Prop

The two-case integral boundary left after comparing all coefficients of the split cubic. The quotient is -4 or 4; rational-function equalities have become integral identities, while canonical denominator positivity and the two cusp exclusions remain explicit.

Equations

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

def MazurTorsion.XOneThirteenDescent.PositiveSplitCyclicCubicObstruction : Prop

A one-sign, one-chamber form of the split-cubic boundary. Both root coordinates are positive, the quotient is 4, and the root coordinate is oriented away from the conjugate prime over 19. The diamond orbit has a unique positive rational abscissa, so no noncuspidal root is lost. The final parameter split-prime condition from FiniteSplitCyclicCubicObstruction is omitted because it already follows from primitivity of m,n.

Equations

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

theorem MazurTorsion.XOneThirteenDescent.finiteSplitCyclicCubicObstruction_of_positiveSplit (hpositive : PositiveSplitCyclicCubicObstruction) : FiniteSplitCyclicCubicObstruction

It suffices to discharge the k=4 split-cubic family. For k=-4, oddness makes m nonzero, and one of (-n,m) or (n,-m) has positive second coordinate. Both substitutions negate all three quadratic coefficients and preserve the quartic discriminant.

theorem MazurTorsion.XOneThirteenDescent.primitiveCyclicCubicObstruction_of_finiteSplit (hfinite : FiniteSplitCyclicCubicObstruction) : PrimitiveCyclicCubicObstruction

The finite split-coefficient boundary implies the primitive rational-root obstruction.

theorem MazurTorsion.XOneThirteenDescent.no_noncuspidal_point_of_primitiveCyclicCubicObstruction (hobs : PrimitiveCyclicCubicObstruction) (x y : ℚ) (hx0 : x ≠ 0) (hxneg : x ≠ -1) (hcurve : y ^ 2 = Kubert.orderThirteenHyperellipticPolynomial x) : False

The primitive cyclic-cubic obstruction excludes every noncuspidal rational point on the X₁(13) sextic.

theorem MazurTorsion.XOneThirteenDescent.rationalPoint_addOrderOf_ne_thirteen_of_primitiveCyclicCubicObstruction (hobs : PrimitiveCyclicCubicObstruction) (E : WeierstrassCurve ℚ) [E.IsElliptic] (Q : (WeierstrassCurve.Affine.baseChange E ℚ).Point) : addOrderOf Q ≠ 13

A proof of the explicit primitive obstruction rules out exact rational order thirteen through the checked Tate-normal-form reduction.

theorem MazurTorsion.XOneThirteenDescent.rationalPoint_addOrderOf_ne_thirteen_of_finiteSplitCyclicCubicObstruction (hfinite : FiniteSplitCyclicCubicObstruction) (E : WeierstrassCurve ℚ) [E.IsElliptic] (Q : (WeierstrassCurve.Affine.baseChange E ℚ).Point) : addOrderOf Q ≠ 13

The two-case integral split obstruction excludes exact rational order thirteen through the checked primitive descent.

theorem MazurTorsion.XOneThirteenDescent.rationalPoint_addOrderOf_ne_thirteen_of_positiveSplitCyclicCubicObstruction (hpositive : PositiveSplitCyclicCubicObstruction) (E : WeierstrassCurve ℚ) [E.IsElliptic] (Q : (WeierstrassCurve.Affine.baseChange E ℚ).Point) : addOrderOf Q ≠ 13

The normalized one-sign split obstruction is already a complete downstream input for excluding exact rational order thirteen.

A degree-19 polynomial Pell certificate

def MazurTorsion.XOneThirteenDescent.pellH (x : ℚ) : ℚ

Degree-19 numerator in the polynomial Pell solution.

Equations

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

def MazurTorsion.XOneThirteenDescent.pellK (x : ℚ) : ℚ

Degree-16 denominator in the polynomial Pell solution.

Equations

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

theorem MazurTorsion.XOneThirteenDescent.pell_identity (x : ℚ) : pellH x ^ 2 - Kubert.orderThirteenHyperellipticPolynomial x * pellK x ^ 2 = -4

Exact polynomial Pell identity for the order-thirteen sextic.

theorem MazurTorsion.XOneThirteenDescent.pell_unit_factorization (x y : ℚ) (hcurve : y ^ 2 = Kubert.orderThirteenHyperellipticPolynomial x) : (pellH x + y * pellK x) * (pellH x - y * pellK x) = -4

On the curve, the two conjugate Pell functions multiply to the constant -4; in particular, they are units on the affine chart.

theorem MazurTorsion.XOneThirteenDescent.pell_factors_ne_zero (x y : ℚ) (hcurve : y ^ 2 = Kubert.orderThirteenHyperellipticPolynomial x) : pellH x + y * pellK x ≠ 0 ∧ pellH x - y * pellK x ≠ 0

Neither conjugate Pell factor vanishes at an affine rational point of the curve.

theorem MazurTorsion.XOneThirteenDescent.pell_affine_cusp_values : Kubert.orderThirteenHyperellipticPolynomial 0 = 1 ∧ Kubert.orderThirteenHyperellipticPolynomial (-1) = 1 ∧ pellH 0 = 0 ∧ pellH (-1) = 0 ∧ pellK 0 = 2 ∧ pellK (-1) = 2

Values of the sextic and Pell solution at the four affine rational cusp points.

def MazurTorsion.XOneThirteenDescent.infinitySextic (z : ℚ) : ℚ

The normalized sextic in the local coordinate z=1/x at infinity.

Equations

• MazurTorsion.XOneThirteenDescent.infinitySextic z = 1 + 2 * z + z ^ 2 + 2 * z ^ 3 + 6 * z ^ 4 + 4 * z ^ 5 + z ^ 6

def MazurTorsion.XOneThirteenDescent.infinityPellH (z : ℚ) : ℚ

Reversal of the degree-19 Pell numerator.

Equations

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

def MazurTorsion.XOneThirteenDescent.infinityPellK (z : ℚ) : ℚ

Reversal of the degree-16 Pell denominator.

Equations

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

theorem MazurTorsion.XOneThirteenDescent.infinitySextic_eq_reciprocal (z : ℚ) (hz : z ≠ 0) : infinitySextic z = z ^ 6 * Kubert.orderThirteenHyperellipticPolynomial (1 / z)

The reciprocal chart formula for the sextic.

theorem MazurTorsion.XOneThirteenDescent.infinityPellH_eq_reciprocal (z : ℚ) (hz : z ≠ 0) : infinityPellH z = z ^ 19 * pellH (1 / z)

Reciprocal chart formula for the degree-19 Pell numerator.

theorem MazurTorsion.XOneThirteenDescent.infinityPellK_eq_reciprocal (z : ℚ) (hz : z ≠ 0) : infinityPellK z = z ^ 16 * pellK (1 / z)

Reciprocal chart formula for the degree-16 Pell denominator.

theorem MazurTorsion.XOneThirteenDescent.infinity_pell_identity (z : ℚ) : infinityPellH z ^ 2 - infinitySextic z * infinityPellK z ^ 2 = -4 * z ^ 38

Reversed Pell identity. Its right side records total vanishing order 38, the algebraic precursor of a divisor difference of order 19 between the two infinity branches.

theorem MazurTorsion.XOneThirteenDescent.infinity_pell_factorization (z η : ℚ) (hchart : η ^ 2 = infinitySextic z) : (infinityPellH z + η * infinityPellK z) * (infinityPellH z - η * infinityPellK z) = -4 * z ^ 38

Factorization on the normalized infinity chart η²=F∞(z).

theorem MazurTorsion.XOneThirteenDescent.infinity_pell_boundary_values : infinitySextic 0 = 1 ∧ infinityPellH 0 = 1 ∧ infinityPellK 0 = 1 ∧ infinityPellH 0 + 1 * infinityPellK 0 = 2 ∧ infinityPellH 0 - -1 * infinityPellK 0 = 2

Values of the reversed Pell data at the two normalized infinity directions.

The exact two-prime Jacobian boundary

theorem MazurTorsion.XOneThirteenDescent.finitePicard_cards_eq_nineteen_of_reducedDegreeTwoEquiv {J3 : Type u_1} {J5 : Type u_2} [AddCommGroup J3] [AddCommGroup J5] [Fintype J3] [Fintype J5] (e3 : J3 ≃+ XOneThirteenFiniteField.ReducedDegreeTwoClassCertificateF3) (e5 : J5 ≃+ XOneThirteenFiniteField.ReducedDegreeTwoClassCertificateF5) : Fintype.card J3 = 19 ∧ Fintype.card J5 = 19

An equivalence from actual finite Picard/Jacobian point types to the checked reduced degree-two certificates would identify both finite groups as having order 19.

This theorem is deliberately an interface boundary: it consumes genuine equivalences, rather than treating the combinatorial certificates as Jacobians.

noncomputable def MazurTorsion.XOneThirteenDescent.finitePicard_addEquiv_zmodNineteen_of_F3Certificate {J3 : Type u_1} [AddCommGroup J3] (e3 : J3 ≃+ XOneThirteenFiniteField.ReducedDegreeTwoClassCertificateF3) : J3 ≃+ ZMod 19

A genuine additive identification of a finite Picard group with the reduced 𝔽₃ divisor certificate immediately gives its cyclic ZMod 19 presentation.

Equations

• MazurTorsion.XOneThirteenDescent.finitePicard_addEquiv_zmodNineteen_of_F3Certificate e3 = e3.trans MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassAddEquivZModF3

noncomputable def MazurTorsion.XOneThirteenDescent.finitePicard_addEquiv_zmodNineteen_of_F5Certificate {J5 : Type u_1} [AddCommGroup J5] (e5 : J5 ≃+ XOneThirteenFiniteField.ReducedDegreeTwoClassCertificateF5) : J5 ≃+ ZMod 19

The corresponding cyclic presentation from the 𝔽₅ certificate.

Equations

• MazurTorsion.XOneThirteenDescent.finitePicard_addEquiv_zmodNineteen_of_F5Certificate e5 = e5.trans MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassAddEquivZModF5

theorem MazurTorsion.XOneThirteenDescent.rationalJacobian_card_eq_nineteen_of_two_reduction_bounds {JQ : Type u_1} [Fintype JQ] (a b : ℕ) (h3 : Fintype.card JQ ∣ Fintype.card XOneThirteenFiniteField.ReducedDegreeTwoClassCertificateF3 * 3 ^ a) (h5 : Fintype.card JQ ∣ Fintype.card XOneThirteenFiniteField.ReducedDegreeTwoClassCertificateF5 * 5 ^ b) (h19 : 19 ∣ Fintype.card JQ) : Fintype.card JQ = 19

The arithmetic endpoint of the two-good-reduction argument for the rational Jacobian.

For a finite rational Jacobian JQ, good reduction at 3 and 5 should produce the first two divisibilities: their extra factors are precisely the possible primary kernels at the residue characteristics. A nonzero divisor class of exact order 19, obtained from the Pell certificate, produces the last divisibility. The checked finite-field class certificates then force #JQ = 19.

What remains outside this theorem is geometric and global: constructing the smooth proper genus-two curve and its Picard/Jacobian, identifying its finite Picard groups with the two certificate types, proving Mordell--Weil rank zero, and proving the two reduction-kernel bounds.

theorem MazurTorsion.XOneThirteenDescent.rationalJacobian_card_eq_nineteen_of_reduction_homs {JQ : Type u_1} {J3 : Type u_2} {J5 : Type u_3} [AddCommGroup JQ] [AddCommGroup J3] [AddCommGroup J5] [Fintype JQ] (e3 : J3 ≃+ XOneThirteenFiniteField.ReducedDegreeTwoClassCertificateF3) (e5 : J5 ≃+ XOneThirteenFiniteField.ReducedDegreeTwoClassCertificateF5) (red3 : JQ →+ J3) (red5 : JQ →+ J5) (a b : ℕ) (hker3 : Nat.card ↥red3.ker = 3 ^ a) (hker5 : Nat.card ↥red5.ker = 5 ^ b) (h19 : 19 ∣ Fintype.card JQ) : Fintype.card JQ = 19

The same rational-Jacobian endpoint, now in the form directly consumed by geometric reduction maps. The hypotheses require additive identifications of both finite Picard groups with the checked certificates and reduction homomorphisms whose kernels have 3-power and 5-power cardinality. Together with the Pell-supplied order-19 subgroup, these data force the rational Jacobian to have cardinality 19; cyclicity then follows from the standard prime-order group theorem.

theorem MazurTorsion.XOneThirteenDescent.exact_order_nineteen_of_divisor_certificate {G : Type u_1} [AddMonoid G] (D : G) (hD : 19 • D = 0) (hne : D ≠ 0) : addOrderOf D = 19

Once a divisor implementation turns the Pell identity into 19 • D = 0, distinctness of the two infinity branches is the only remaining group-theoretic input needed to certify exact order 19.