Documentation

MazurTorsion.Kubert.OrderTwentyFive

Rational points of order twenty-five #

An exact order-25 point is put in Tate normal form. The checked rational recurrence computes 12P and 13P, with every nonzero secant denominator deduced from exact order. Since 13P = -12P, their abscissas agree. This gives an explicit rational-function equation on X₁(25). A second checked recurrence carries numerator and denominator data without division and cross-multiplies the collision to a fixed polynomial expression, while preserving the discriminant scaling from the original elliptic curve.

This is a forward reduction, not yet a tractable birational model or the Diophantine exclusion of all noncuspidal rational points on the resulting curve.

source
def MazurTorsion.Kubert.orderTwentyFiveRecurrenceEquation (b c : ℚ) :
ℚ

The rational-function equation obtained by comparing 12P and 13P in the denominator-checked Tate recurrence.

Equations
Instances For
    source
    def MazurTorsion.Kubert.orderTwentyFiveClearedEquation (b c : ℚ) :
    ℚ

    The fraction-free cross-multiplied form of the 12P/13P collision. It is a fixed expression involving only addition and multiplication in b,c; the recurrence specification proves that no extraneous denominator is used.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MazurTorsion.Kubert.tateSuccessiveX_ne_zero_of_marked_order_twentyFive (b c : ℚ) (hb : b ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) (horder : addOrderOf (WeierstrassCurve.Affine.Point.some 0 0 h00) = 25) (n : ℕ) :
      n ≤ 10 → tateSuccessiveX b c n ≠ 0

      Exact order 25 makes every abscissa used to compute through 13P nonzero. These are precisely the secant denominators of the recurrence.

      source
      theorem MazurTorsion.Kubert.orderTwentyFiveRecurrenceEquation_eq_zero_of_marked_order (b c : ℚ) (hb : b ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) (horder : addOrderOf (WeierstrassCurve.Affine.Point.some 0 0 h00) = 25) :
      orderTwentyFiveRecurrenceEquation b c = 0

      Exact order 25 of the marked Tate point forces the checked 12P/13P rational-function equation.

      source
      theorem MazurTorsion.Kubert.orderTwentyFiveClearedEquation_eq_zero_of_marked_order (b c : ℚ) (hb : b ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) (horder : addOrderOf (WeierstrassCurve.Affine.Point.some 0 0 h00) = 25) :
      orderTwentyFiveClearedEquation b c = 0

      Exact order 25 forces the fraction-free X₁(25) recurrence equation. The proof obtains both denominator certificates before cross-multiplying.

      source
      theorem MazurTorsion.Kubert.exists_tateOrderTwentyFive_recurrence_certificate (E : WeierstrassCurve ℚ) [E.IsElliptic] (P : (WeierstrassCurve.Affine.baseChange E ℚ).Point) (hP : addOrderOf P = 25) :
      ∃ (b : ℚ) (c : ℚ) (u : ℚ), u ≠ 0 ∧ b ≠ 0 ∧ (∀ n ≤ 10, tateSuccessiveX b c n ≠ 0) ∧ orderTwentyFiveRecurrenceEquation b c = 0 ∧ orderTwentyFiveClearedEquation b c = 0 ∧ u ^ 12 * E.Δ = (tateNormalCurve b c).Δ

      A rational point of exact order 25 supplies a denominator-checked point on the explicit Tate recurrence locus, retaining the twelfth-power discriminant scale of the original curve.