Finite-field certificates for the X₁(13) sextic

This file records elementary certificates for the reduction modulo 3 of

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

The reduced sextic is separable: explicit Bézout coefficients for it and its derivative are checked in the kernel. Its affine solutions over ZMod 3 are exactly

(0, 1), (0, -1), (-1, 1), (-1, -1).

For the usual weighted-projective compactification of a monic even-degree hyperelliptic equation, the normalized infinity chart has equation η² = 1. We define and enumerate those normalized directions, obtaining two of them. The resulting sum type is only an explicit finite-field point certificate; this file does not assert an equivalence with a projective-curve API.

In particular, none of these calculations proves a classification over ℚ, a theorem about the Jacobian, or injectivity of reduction on rational points.

@[reducible, inline]

abbrev MazurTorsion.XOneThirteenFiniteField.F3 : Type

The three-element residue field used for the order-thirteen point count.

Equations

• MazurTorsion.XOneThirteenFiniteField.F3 = ZMod 3

noncomputable def MazurTorsion.XOneThirteenFiniteField.sextic : Polynomial F3

The order-thirteen hyperelliptic sextic reduced modulo 3.

Equations

• MazurTorsion.XOneThirteenFiniteField.sextic = Polynomial.X ^ 6 + 2 * Polynomial.X ^ 5 + Polynomial.X ^ 4 + 2 * Polynomial.X ^ 3 + 6 * Polynomial.X ^ 2 + 4 * Polynomial.X + 1

def MazurTorsion.XOneThirteenFiniteField.sexticValue (x : F3) : F3

A computable presentation of the sextic's value function.

Equations

• MazurTorsion.XOneThirteenFiniteField.sexticValue x = x ^ 6 + 2 * x ^ 5 + x ^ 4 + 2 * x ^ 3 + 6 * x ^ 2 + 4 * x + 1

theorem MazurTorsion.XOneThirteenFiniteField.eval_sextic (x : F3) : Polynomial.eval x sextic = sexticValue x

Evaluation of the reduced sextic agrees with the displayed formula.

theorem MazurTorsion.XOneThirteenFiniteField.derivative_sextic : Polynomial.derivative sextic = Polynomial.X ^ 4 + Polynomial.X ^ 3 + 1

The formal derivative of the reduced sextic.

noncomputable def MazurTorsion.XOneThirteenFiniteField.bezoutLeft : Polynomial F3

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

Equations

• MazurTorsion.XOneThirteenFiniteField.bezoutLeft = Polynomial.X ^ 3 + 1

noncomputable def MazurTorsion.XOneThirteenFiniteField.bezoutRight : Polynomial F3

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

Equations

• MazurTorsion.XOneThirteenFiniteField.bezoutRight = -(Polynomial.X ^ 5 + Polynomial.X ^ 4 + Polynomial.X)

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

Explicit gcd certificate for the sextic and its derivative.

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

The reduced sextic is coprime to its derivative.

theorem MazurTorsion.XOneThirteenFiniteField.sextic_separable : sextic.Separable

The reduction modulo 3 is separable.

theorem MazurTorsion.XOneThirteenFiniteField.sextic_squarefree : Squarefree sextic

In particular, the reduced sextic is squarefree.

theorem MazurTorsion.XOneThirteenFiniteField.sextic_or_derivative_ne_zero (x : F3) : Polynomial.eval x sextic ≠ 0 ∨ Polynomial.eval x (Polynomial.derivative sextic) ≠ 0

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

def MazurTorsion.XOneThirteenFiniteField.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.XOneThirteenFiniteField.instFintypeAffineSolution : Fintype AffineSolution

Equations

• MazurTorsion.XOneThirteenFiniteField.instFintypeAffineSolution = id inferInstance

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

Complete enumeration of affine solutions over F3.

theorem MazurTorsion.XOneThirteenFiniteField.affine_solution_polynomial_iff (x y : F3) : 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.XOneThirteenFiniteField.card_affineSolution : Fintype.card AffineSolution = 4

There are exactly four affine solutions over F3.

def MazurTorsion.XOneThirteenFiniteField.IsAffineCuspX (x : F3) : Prop

The two affine abscissas occurring modulo 3. They are precisely the reductions of the rational affine cusp abscissas from the sextic model.

Equations

• MazurTorsion.XOneThirteenFiniteField.IsAffineCuspX x = (x = 0 ∨ x = -1)

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instDecidableIsAffineCuspX (x : F3) : Decidable (IsAffineCuspX x)

Equations

• MazurTorsion.XOneThirteenFiniteField.instDecidableIsAffineCuspX x = MazurTorsion.XOneThirteenFiniteField.instDecidableIsAffineCuspX._aux_1 x

theorem MazurTorsion.XOneThirteenFiniteField.affine_solution_is_cusp_value (x y : F3) : y ^ 2 = sexticValue x → IsAffineCuspX x

Computable form of affine_solution_is_cusp.

theorem MazurTorsion.XOneThirteenFiniteField.affine_solution_is_cusp (x y : F3) : y ^ 2 = Polynomial.eval x sextic → IsAffineCuspX x

Every affine F3-solution has a cusp abscissa.

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

The affine equation has two ordinates over each cusp abscissa.

theorem MazurTorsion.XOneThirteenFiniteField.eval_derivative_sextic (x : F3) : Polynomial.eval x (Polynomial.derivative sextic) = x ^ 4 + x ^ 3 + 1

The derivative has the following computable value function.

theorem MazurTorsion.XOneThirteenFiniteField.affine_jacobian_nonsingular (x y : F3) : y ^ 2 = sexticValue x → x ^ 4 + x ^ 3 + 1 ≠ 0 ∨ 2 * y ≠ 0

Explicit affine Jacobian certificate: at a solution, the two partial derivatives -f'(x) and 2y cannot both vanish.

theorem MazurTorsion.XOneThirteenFiniteField.affine_jacobian_nonsingular_polynomial (x y : F3) (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.XOneThirteenFiniteField.sextic_monic : sextic.Monic

The reduced sextic is monic.

def MazurTorsion.XOneThirteenFiniteField.InfinityDirection : Type

A normalized direction in the infinity chart of the monic even-degree model. In weighted-projective coordinates these are the solutions with X = 1 and Z = 0.

Equations

• MazurTorsion.XOneThirteenFiniteField.InfinityDirection = { η : MazurTorsion.XOneThirteenFiniteField.F3 // η ^ 2 = 1 }

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeInfinityDirection : Fintype InfinityDirection

Equations

• MazurTorsion.XOneThirteenFiniteField.instFintypeInfinityDirection = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.infinity_equation_iff_leadingCoeff (η : F3) : η ^ 2 = 1 ↔ η ^ 2 = sextic.leadingCoeff

The normalized equation η² = 1 is exactly the leading-coefficient equation for this monic sextic.

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

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

theorem MazurTorsion.XOneThirteenFiniteField.infinity_direction_iff (η : F3) : η ^ 2 = 1 ↔ η = 1 ∨ η = -1

The normalized infinity directions are exactly η = ±1.

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

There are exactly two normalized points in the infinity chart.

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

The Y-partial derivative is nonzero at either infinity direction, so the two normalized infinity-chart points are distinct smooth directions.

def MazurTorsion.XOneThirteenFiniteField.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.XOneThirteenFiniteField.PointCertificate = (MazurTorsion.XOneThirteenFiniteField.AffineSolution ⊕ MazurTorsion.XOneThirteenFiniteField.InfinityDirection)

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypePointCertificate : Fintype PointCertificate

Equations

• MazurTorsion.XOneThirteenFiniteField.instFintypePointCertificate = id inferInstance

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

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