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.

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_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.

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 complete explicit descent data obtained here from a noncuspidal rational point.

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.

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.