Point-order consequences of the finite-field-eleven enumeration

This file is the point-level consumer of the exhaustive 121-model enumeration in OrderThirtyFiveFiniteField. It turns the checked bound #E(F_11) ≤ 18 into the exact local obstruction used by the order-35 formal-immersion route. No modular interpretation of the fixed quotient model is asserted here.

theorem MazurTorsion.OrderThirtyFive.shortCurveEleven_addOrderOf_le_eighteen (a b : ZMod 11) [(shortCurveEleven a b).IsElliptic] (P : (shortCurveEleven a b).toAffine.Point) : addOrderOf P ≤ 18

Every point on an elliptic short Weierstrass model over F_11 has additive order at most eighteen.

theorem MazurTorsion.OrderThirtyFive.shortCurveEleven_addOrderOf_ne_of_nineteen_le (a b : ZMod 11) [(shortCurveEleven a b).IsElliptic] (P : (shortCurveEleven a b).toAffine.Point) (N : ℕ) (hN : 19 ≤ N) : addOrderOf P ≠ N

An elliptic short model over F_11 has no point whose exact order is at least nineteen.

theorem MazurTorsion.OrderThirtyFive.zmod_eleven_addOrderOf_le_eighteen (W : WeierstrassCurve (ZMod 11)) [W.IsElliptic] (P : W.toAffine.Point) : addOrderOf P ≤ 18

The exhaustive normalization-and-enumeration certificate bounds the additive order of every point on every elliptic curve over F_11.

theorem MazurTorsion.OrderThirtyFive.zmod_eleven_addOrderOf_ne_of_nineteen_le (W : WeierstrassCurve (ZMod 11)) [W.IsElliptic] (P : W.toAffine.Point) (N : ℕ) (hN : 19 ≤ N) : addOrderOf P ≠ N

No point on an elliptic curve over F_11 has additive order at least nineteen.

theorem MazurTorsion.OrderThirtyFive.zmod_eleven_addOrderOf_ne_thirtyFive (W : WeierstrassCurve (ZMod 11)) [W.IsElliptic] (P : W.toAffine.Point) : addOrderOf P ≠ 35

In particular, the finite-field certificate rules out a specialized point of exact order 35.