Discriminant obstructions to full odd-prime torsion

For an odd integer n, the nonzero n-torsion points modulo sign are the roots of the univariate division polynomial preΨ' n. If all of those points are rational, that polynomial splits over ℚ, so its discriminant is a rational square. For n = 5 and n = 7, the classical division-polynomial discriminant formula has respectively the shapes

• 5 ^ 11 * Δ ^ 22, and
• -(7 ^ 23 * Δ ^ 92).

Neither is a square when the curve discriminant Δ is nonzero. This file establishes the polynomial and rational-arithmetic part of that argument. The two missing geometric identities (the torsion/root equivalence and the division-polynomial discriminant formula) are intentionally not postulated here.

theorem MazurTorsion.OddPrimeFullTorsion.isSquare_discr_of_splits {f : Polynomial ℚ} (hf : f.Splits) : IsSquare f.discr

A polynomial over ℚ which splits completely has square discriminant.

This includes the repeated-root case, when the discriminant is zero. The result is the elementary polynomial bridge used by the fixed-prime torsion obstruction below.

def MazurTorsion.OddPrimeFullTorsion.HasDivisionPolynomialRootCriterion (W : WeierstrassCurve ℚ) (n : ℕ) : Prop

The forward division-polynomial root criterion needed by the discriminant argument.

Mathlib currently defines the division polynomials but does not yet connect their evaluation to scalar multiplication of affine points.

Equations

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

theorem MazurTorsion.OddPrimeFullTorsion.fifth_division_polynomial_splits_of_full_torsion (W : WeierstrassCurve ℚ) [W.IsElliptic] (hroot : HasDivisionPolynomialRootCriterion W 5) (φ : ZMod 5 × ZMod 5 →+ W.toAffine.Point) (hφ : Function.Injective ⇑φ) : (W.preΨ' 5).Splits

Full rational 5-torsion makes the fifth division polynomial split, assuming only the forward torsion/root criterion.

theorem MazurTorsion.OddPrimeFullTorsion.seventh_division_polynomial_splits_of_full_torsion (W : WeierstrassCurve ℚ) [W.IsElliptic] (hroot : HasDivisionPolynomialRootCriterion W 7) (φ : ZMod 7 × ZMod 7 →+ W.toAffine.Point) (hφ : Function.Injective ⇑φ) : (W.preΨ' 7).Splits

Full rational 7-torsion makes the seventh division polynomial split, assuming only the forward torsion/root criterion.

theorem MazurTorsion.OddPrimeFullTorsion.not_isSquare_five_discriminant_shape {Δ : ℚ} (hΔ : Δ ≠ 0) : ¬IsSquare (5 ^ 11 * Δ ^ 22)

The square class occurring in the discriminant of the fifth division polynomial is nontrivial over ℚ.

theorem MazurTorsion.OddPrimeFullTorsion.not_isSquare_seven_discriminant_shape {Δ : ℚ} (hΔ : Δ ≠ 0) : ¬IsSquare (-(7 ^ 23 * Δ ^ 92))

The square class occurring in the discriminant of the seventh division polynomial is nontrivial over ℚ.

theorem MazurTorsion.OddPrimeFullTorsion.not_splits_of_discr_eq_five_shape {f : Polynomial ℚ} {Δ : ℚ} (hΔ : Δ ≠ 0) (hdiscr : f.discr = 5 ^ 11 * Δ ^ 22) : ¬f.Splits

A rational polynomial with the fifth-division discriminant shape cannot split over ℚ.

theorem MazurTorsion.OddPrimeFullTorsion.not_splits_of_discr_eq_seven_shape {f : Polynomial ℚ} {Δ : ℚ} (hΔ : Δ ≠ 0) (hdiscr : f.discr = -(7 ^ 23 * Δ ^ 92)) : ¬f.Splits

A rational polynomial with the seventh-division discriminant shape cannot split over ℚ.

theorem MazurTorsion.OddPrimeFullTorsion.fifth_division_polynomial_not_splits_of_discr (W : WeierstrassCurve ℚ) [W.IsElliptic] (hdiscr : (W.preΨ' 5).discr = 5 ^ 11 * W.Δ ^ 22) : ¬(W.preΨ' 5).Splits

The fifth division polynomial cannot split once its classical discriminant identity is available. This isolates that identity as the only missing polynomial calculation.

theorem MazurTorsion.OddPrimeFullTorsion.seventh_division_polynomial_not_splits_of_discr (W : WeierstrassCurve ℚ) [W.IsElliptic] (hdiscr : (W.preΨ' 7).discr = -(7 ^ 23 * W.Δ ^ 92)) : ¬(W.preΨ' 7).Splits

The seventh division polynomial cannot split once its classical discriminant identity is available. This isolates that identity as the only missing polynomial calculation.

theorem MazurTorsion.OddPrimeFullTorsion.not_injective_zmod_five_square_of_division_inputs (W : WeierstrassCurve ℚ) [W.IsElliptic] (hroot : HasDivisionPolynomialRootCriterion W 5) (hdiscr : (W.preΨ' 5).discr = 5 ^ 11 * W.Δ ^ 22) (φ : ZMod 5 × ZMod 5 →+ W.toAffine.Point) : ¬Function.Injective ⇑φ

The exact full-rational-5-torsion obstruction obtained from the two missing division-polynomial inputs.

theorem MazurTorsion.OddPrimeFullTorsion.not_injective_zmod_seven_square_of_division_inputs (W : WeierstrassCurve ℚ) [W.IsElliptic] (hroot : HasDivisionPolynomialRootCriterion W 7) (hdiscr : (W.preΨ' 7).discr = -(7 ^ 23 * W.Δ ^ 92)) (φ : ZMod 7 × ZMod 7 →+ W.toAffine.Point) : ¬Function.Injective ⇑φ

The exact full-rational-7-torsion obstruction obtained from the two missing division-polynomial inputs.