The eighteen-point bound over F_11 for the order-35 endpoint

The squarefree-level formal-immersion route at auxiliary prime 11 needs only the concrete inequality #E(F_11) ≤ 18. Short-Weierstrass normalization reduces this to 121 coefficient pairs, which are checked exhaustively here instead of importing a general Hasse theorem.

def MazurTorsion.OrderThirtyFive.shortCurveEleven (a b : ZMod 11) : WeierstrassCurve (ZMod 11)

The short Weierstrass equation y² = x³ + a*x + b over F_11.

Equations

• MazurTorsion.OrderThirtyFive.shortCurveEleven a b = { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := a, a₆ := b }

theorem MazurTorsion.OrderThirtyFive.card_shortCurveEleven_le_eighteen (a b : ZMod 11) : Fintype.card (shortCurveEleven a b).toAffine.Point ≤ 18

Every short Weierstrass model over F_11 has at most eighteen nonsingular projective points.

theorem MazurTorsion.OrderThirtyFive.card_reductionAtEleven_le_eighteen (W : WeierstrassCurve (ZMod 11)) [W.IsElliptic] : Nat.card W.toAffine.Point ≤ 18

Every elliptic Weierstrass equation over F_11 is point-group equivalent to an enumerated short model, so its point group has at most eighteen elements.