Finite-field and symmetry certificates for the X₁(18) sextic

The genus-two reduction for order eighteen produces

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

This file records two independent elementary boundaries.

First, modulo 5, the sextic is separable and has exactly four affine solutions, all above X = 0 or X = 1. Its monic even-degree infinity chart has two smooth normalized directions. Their sum is packaged only as a six-element finite-field point certificate; no projective-curve API equivalence or reduction theorem is asserted.

Second, over ℚ, the Möbius transformation

X ↦ 1/(1-X)

has order three on the abscissa. Its lift

(X,Y) ↦ (1/(1-X), -Y/(1-X)³)

preserves the sextic and also has order three away from X = 0,1. Two checked invariant functions satisfy a conic equation. These identities expose the elementary order-three symmetry used in classical treatments; they do not construct an endomorphism of the Jacobian or prove its rank.

Rational order-three symmetry

def MazurTorsion.XOneEighteenFiniteField.orderThreeX (x : ℚ) : ℚ

The order-three Möbius transformation on the abscissa.

Equations

• MazurTorsion.XOneEighteenFiniteField.orderThreeX x = 1 / (1 - x)

def MazurTorsion.XOneEighteenFiniteField.orderThreeY (x y : ℚ) : ℚ

The order-three lift to the ordinate. The minus sign selects the order-three lift rather than the lift whose cube is the hyperelliptic involution.

Equations

• MazurTorsion.XOneEighteenFiniteField.orderThreeY x y = -y / (1 - x) ^ 3

theorem MazurTorsion.XOneEighteenFiniteField.orderThree_sextic_covariance (x : ℚ) (hx1 : x ≠ 1) : (1 - x) ^ 6 * Kubert.orderEighteenHyperellipticPolynomial (orderThreeX x) = Kubert.orderEighteenHyperellipticPolynomial x

The sextic is covariant under the Möbius transformation.

theorem MazurTorsion.XOneEighteenFiniteField.orderThreeX_sq (x : ℚ) (hx0 : x ≠ 0) (hx1 : x ≠ 1) : orderThreeX (orderThreeX x) = (x - 1) / x

The second Möbius iterate in a denominator-safe form.

theorem MazurTorsion.XOneEighteenFiniteField.orderThreeX_cube (x : ℚ) (hx0 : x ≠ 0) (hx1 : x ≠ 1) : orderThreeX (orderThreeX (orderThreeX x)) = x

The Möbius transformation has exact third iterate equal to the identity on its noncuspidal affine domain.

theorem MazurTorsion.XOneEighteenFiniteField.orderThree_preserves_curve (x y : ℚ) (hx1 : x ≠ 1) (hcurve : y ^ 2 = Kubert.orderEighteenHyperellipticPolynomial x) : orderThreeY x y ^ 2 = Kubert.orderEighteenHyperellipticPolynomial (orderThreeX x)

The lifted transformation preserves the hyperelliptic equation.

theorem MazurTorsion.XOneEighteenFiniteField.orderThreeY_cube (x y : ℚ) (hx0 : x ≠ 0) (hx1 : x ≠ 1) : orderThreeY (orderThreeX (orderThreeX x)) (orderThreeY (orderThreeX x) (orderThreeY x y)) = y

The selected lift has third iterate equal to the identity on the noncuspidal affine domain.

def MazurTorsion.XOneEighteenFiniteField.invariantX (x : ℚ) : ℚ

A rational invariant of the order-three action on the abscissa.

Equations

• MazurTorsion.XOneEighteenFiniteField.invariantX x = (x ^ 3 - 3 * x + 1) / (x * (x - 1))

def MazurTorsion.XOneEighteenFiniteField.invariantY (x y : ℚ) : ℚ

A rational invariant involving the ordinate.

Equations

• MazurTorsion.XOneEighteenFiniteField.invariantY x y = y / (x * (x - 1))

theorem MazurTorsion.XOneEighteenFiniteField.invariantX_eq_orbit_sum (x : ℚ) (hx0 : x ≠ 0) (hx1 : x ≠ 1) : invariantX x = x + orderThreeX x + orderThreeX (orderThreeX x)

The abscissa invariant is the trace of the three-element Möbius orbit.

theorem MazurTorsion.XOneEighteenFiniteField.orderThree_orbit_product (x : ℚ) (hx0 : x ≠ 0) (hx1 : x ≠ 1) : x * orderThreeX x * orderThreeX (orderThreeX x) = -1

The product of the three abscissas in a Möbius orbit is -1.

theorem MazurTorsion.XOneEighteenFiniteField.invariantX_orderThree (x : ℚ) (hx0 : x ≠ 0) (hx1 : x ≠ 1) : invariantX (orderThreeX x) = invariantX x

The first displayed function is invariant under the Möbius action.

theorem MazurTorsion.XOneEighteenFiniteField.invariantY_orderThree (x y : ℚ) (hx0 : x ≠ 0) (hx1 : x ≠ 1) : invariantY (orderThreeX x) (orderThreeY x y) = invariantY x y

The ordinate invariant is fixed by the chosen order-three lift.

theorem MazurTorsion.XOneEighteenFiniteField.invariant_conic_equation (x y : ℚ) (hx0 : x ≠ 0) (hx1 : x ≠ 1) (hcurve : y ^ 2 = Kubert.orderEighteenHyperellipticPolynomial x) : invariantY x y ^ 2 = invariantX x ^ 2 - 4 * invariantX x + 12

On the sextic, the two invariant functions lie on a rational conic. This is only a function-field identity, not a theorem about the Jacobian.

Reduction modulo five

@[reducible, inline]

abbrev MazurTorsion.XOneEighteenFiniteField.F5 : Type

The five-element residue field used for the order-eighteen point count.

Equations

• MazurTorsion.XOneEighteenFiniteField.F5 = ZMod 5

noncomputable def MazurTorsion.XOneEighteenFiniteField.sextic : Polynomial F5

The order-eighteen sextic reduced modulo 5, in reduced-coefficient form.

Equations

• MazurTorsion.XOneEighteenFiniteField.sextic = Polynomial.X ^ 6 + Polynomial.X ^ 5 + 3 * Polynomial.X + 1

def MazurTorsion.XOneEighteenFiniteField.sexticValue (x : F5) : F5

A computable presentation of the reduced sextic's value function.

Equations

• MazurTorsion.XOneEighteenFiniteField.sexticValue x = x ^ 6 + x ^ 5 + 3 * x + 1

theorem MazurTorsion.XOneEighteenFiniteField.eval_sextic (x : F5) : Polynomial.eval x sextic = sexticValue x

Evaluation of the polynomial agrees with its computable value function.

theorem MazurTorsion.XOneEighteenFiniteField.sexticValue_eq_model_formula (x : F5) : sexticValue x = x ^ 6 - 4 * x ^ 5 + 10 * x ^ 4 - 10 * x ^ 3 + 5 * x ^ 2 - 2 * x + 1

The reduced value function agrees with the original integral sextic formula modulo 5.

theorem MazurTorsion.XOneEighteenFiniteField.derivative_sextic : Polynomial.derivative sextic = Polynomial.X ^ 5 + 3

The formal derivative of the reduced sextic.

noncomputable def MazurTorsion.XOneEighteenFiniteField.bezoutLeft : Polynomial F5

Left Bézout coefficient for the sextic and its derivative.

Equations

• MazurTorsion.XOneEighteenFiniteField.bezoutLeft = 2

noncomputable def MazurTorsion.XOneEighteenFiniteField.bezoutRight : Polynomial F5

Right Bézout coefficient for the sextic and its derivative.

Equations

• MazurTorsion.XOneEighteenFiniteField.bezoutRight = 3 * Polynomial.X + 3

theorem MazurTorsion.XOneEighteenFiniteField.sextic_derivative_bezout : bezoutLeft * sextic + bezoutRight * Polynomial.derivative sextic = 1

Explicit gcd certificate for the sextic and its derivative.

theorem MazurTorsion.XOneEighteenFiniteField.sextic_isCoprime_derivative : IsCoprime sextic (Polynomial.derivative sextic)

The reduced sextic is coprime to its derivative.

theorem MazurTorsion.XOneEighteenFiniteField.sextic_separable : sextic.Separable

The reduction modulo 5 is separable.

theorem MazurTorsion.XOneEighteenFiniteField.sextic_squarefree : Squarefree sextic

In particular, the reduced sextic is squarefree.

theorem MazurTorsion.XOneEighteenFiniteField.sextic_or_derivative_ne_zero (x : F5) : Polynomial.eval x sextic ≠ 0 ∨ Polynomial.eval x (Polynomial.derivative sextic) ≠ 0

The sextic and its derivative have no common root over F5.

def MazurTorsion.XOneEighteenFiniteField.AffineSolution : Type

An affine solution of the reduced hyperelliptic equation.

Equations

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

@[instance_reducible]

instance MazurTorsion.XOneEighteenFiniteField.instFintypeAffineSolution : Fintype AffineSolution

Equations

• MazurTorsion.XOneEighteenFiniteField.instFintypeAffineSolution = id inferInstance

theorem MazurTorsion.XOneEighteenFiniteField.affine_solution_iff (x y : F5) : y ^ 2 = sexticValue x ↔ x = 0 ∧ (y = 1 ∨ y = -1) ∨ x = 1 ∧ (y = 1 ∨ y = -1)

Complete enumeration of affine solutions over F5.

theorem MazurTorsion.XOneEighteenFiniteField.affine_solution_polynomial_iff (x y : F5) : y ^ 2 = Polynomial.eval x sextic ↔ x = 0 ∧ (y = 1 ∨ y = -1) ∨ x = 1 ∧ (y = 1 ∨ y = -1)

Polynomial-evaluation form of the complete affine enumeration.

theorem MazurTorsion.XOneEighteenFiniteField.card_affineSolution : Fintype.card AffineSolution = 4

There are exactly four affine solutions over F5.

def MazurTorsion.XOneEighteenFiniteField.IsAffineCuspX (x : F5) : Prop

The two affine abscissas occurring modulo 5.

Equations

• MazurTorsion.XOneEighteenFiniteField.IsAffineCuspX x = (x = 0 ∨ x = 1)

@[instance_reducible]

instance MazurTorsion.XOneEighteenFiniteField.instDecidableIsAffineCuspX (x : F5) : Decidable (IsAffineCuspX x)

Equations

• MazurTorsion.XOneEighteenFiniteField.instDecidableIsAffineCuspX x = MazurTorsion.XOneEighteenFiniteField.instDecidableIsAffineCuspX._aux_1 x

theorem MazurTorsion.XOneEighteenFiniteField.affine_solution_is_cusp_value (x y : F5) : y ^ 2 = sexticValue x → IsAffineCuspX x

Every affine F5-solution has a cusp abscissa.

theorem MazurTorsion.XOneEighteenFiniteField.affine_solution_is_cusp (x y : F5) (hxy : y ^ 2 = Polynomial.eval x sextic) : IsAffineCuspX x

Polynomial-evaluation form of the cusp-abscissa enumeration.

theorem MazurTorsion.XOneEighteenFiniteField.cusp_abscissa_solution_iff (x : F5) : IsAffineCuspX x → ∀ (y : F5), y ^ 2 = sexticValue x ↔ y = 1 ∨ y = -1

The affine equation has two ordinates over each cusp abscissa.

theorem MazurTorsion.XOneEighteenFiniteField.eval_derivative_sextic (x : F5) : Polynomial.eval x (Polynomial.derivative sextic) = x ^ 5 + 3

The derivative has the following computable value function.

theorem MazurTorsion.XOneEighteenFiniteField.affine_jacobian_nonsingular (x y : F5) : y ^ 2 = sexticValue x → x ^ 5 + 3 ≠ 0 ∨ 2 * y ≠ 0

Explicit affine Jacobian certificate.

theorem MazurTorsion.XOneEighteenFiniteField.affine_jacobian_nonsingular_polynomial (x y : F5) (hxy : y ^ 2 = Polynomial.eval x sextic) : Polynomial.eval x (Polynomial.derivative sextic) ≠ 0 ∨ 2 * y ≠ 0

Polynomial-evaluation form of the affine Jacobian certificate.

theorem MazurTorsion.XOneEighteenFiniteField.sextic_monic : sextic.Monic

The reduced sextic is monic.

def MazurTorsion.XOneEighteenFiniteField.InfinityDirection : Type

A normalized direction in the infinity chart of the monic even-degree model.

Equations

• MazurTorsion.XOneEighteenFiniteField.InfinityDirection = { η : MazurTorsion.XOneEighteenFiniteField.F5 // η ^ 2 = 1 }

@[instance_reducible]

instance MazurTorsion.XOneEighteenFiniteField.instFintypeInfinityDirection : Fintype InfinityDirection

Equations

• MazurTorsion.XOneEighteenFiniteField.instFintypeInfinityDirection = id inferInstance

theorem MazurTorsion.XOneEighteenFiniteField.infinity_equation_iff_leadingCoeff (η : F5) : η ^ 2 = 1 ↔ η ^ 2 = sextic.leadingCoeff

The normalized equation is exactly the leading-coefficient equation for this monic sextic.

theorem MazurTorsion.XOneEighteenFiniteField.infinity_direction_satisfies_leadingCoeff (η : InfinityDirection) : ↑η ^ 2 = sextic.leadingCoeff

Every normalized infinity direction satisfies the actual leading-coefficient equation.

theorem MazurTorsion.XOneEighteenFiniteField.infinity_direction_iff (η : F5) : η ^ 2 = 1 ↔ η = 1 ∨ η = -1

The normalized infinity directions are exactly η = ±1.

theorem MazurTorsion.XOneEighteenFiniteField.card_infinityDirection : Fintype.card InfinityDirection = 2

There are exactly two normalized points in the infinity chart.

theorem MazurTorsion.XOneEighteenFiniteField.infinity_direction_jacobian_nonsingular (η : InfinityDirection) : 2 * ↑η ≠ 0

The Y-partial derivative is nonzero at either infinity direction.

def MazurTorsion.XOneEighteenFiniteField.PointCertificate : Type

The elementary six-element certificate obtained by adjoining the two normalized infinity directions to the four affine solutions.

No equivalence with a projective-curve implementation is claimed here.

Equations

• MazurTorsion.XOneEighteenFiniteField.PointCertificate = (MazurTorsion.XOneEighteenFiniteField.AffineSolution ⊕ MazurTorsion.XOneEighteenFiniteField.InfinityDirection)

@[instance_reducible]

instance MazurTorsion.XOneEighteenFiniteField.instFintypePointCertificate : Fintype PointCertificate

Equations

• MazurTorsion.XOneEighteenFiniteField.instFintypePointCertificate = id inferInstance

theorem MazurTorsion.XOneEighteenFiniteField.card_pointCertificate : Fintype.card PointCertificate = 6

The affine enumeration plus the normalized infinity chart has six elements.