Further multiples on Tate normal form

This file extends the kernel-checked low-multiple calculations for the marked point P = (0, 0) on

y² + (1-c)xy - by = x³ - bx².

The central lemma is a small recurrence: if Q = (x, y) and x ≠ 0, it computes Q + P. The formulas for 5P and 6P are then consequences of the already checked formula for 4P. Every denominator used below has a corresponding explicit nonvanishing hypothesis.

def MazurTorsion.Kubert.tateNextX (b c x y : ℚ) : ℚ

The X-coordinate obtained by adding the marked Tate point (0, 0) to (x, y).

Equations

• MazurTorsion.Kubert.tateNextX b c x y = (y / x) ^ 2 + (1 - c) * (y / x) + b - x

def MazurTorsion.Kubert.tateNextY (b c x y : ℚ) : ℚ

The Y-coordinate obtained by adding the marked Tate point (0, 0) to (x, y).

Equations

• MazurTorsion.Kubert.tateNextY b c x y = -(y / x * (MazurTorsion.Kubert.tateNextX b c x y - x) + y) - (1 - c) * MazurTorsion.Kubert.tateNextX b c x y + b

theorem MazurTorsion.Kubert.add_origin_coordinates (b c x y : ℚ) (hx : x ≠ 0) (hxy : (tateNormalCurve b c).toAffine.Nonsingular x y) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) : ∃ (hnext : (tateNormalCurve b c).toAffine.Nonsingular (tateNextX b c x y) (tateNextY b c x y)), WeierstrassCurve.Affine.Point.some x y hxy + WeierstrassCurve.Affine.Point.some 0 0 h00 = WeierstrassCurve.Affine.Point.some (tateNextX b c x y) (tateNextY b c x y) hnext

Kernel-checked recurrence for adding the marked point to an affine Tate-normal-form point. The sole denominator introduced by the secant formula is recorded as hx.

def MazurTorsion.Kubert.tateSuccessiveCoordinates (b c : ℚ) : ℕ → ℚ × ℚ

Successive affine coordinates obtained by starting at 2P = (b, bc) and repeatedly adding the marked Tate point P = (0, 0). Index n is intended to represent (n + 2)P; the accompanying theorem records exactly the nonzero abscissas needed for this rational recurrence to agree with the group law.

Equations

• One or more equations did not get rendered due to their size.
• MazurTorsion.Kubert.tateSuccessiveCoordinates b c 0 = (b, b * c)

def MazurTorsion.Kubert.tateSuccessiveX (b c : ℚ) (n : ℕ) : ℚ

The recurrence-defined abscissa of (n + 2)P.

Equations

• MazurTorsion.Kubert.tateSuccessiveX b c n = (MazurTorsion.Kubert.tateSuccessiveCoordinates b c n).1

def MazurTorsion.Kubert.tateSuccessiveY (b c : ℚ) (n : ℕ) : ℚ

The recurrence-defined ordinate of (n + 2)P.

Equations

• MazurTorsion.Kubert.tateSuccessiveY b c n = (MazurTorsion.Kubert.tateSuccessiveCoordinates b c n).2

@[simp]

theorem MazurTorsion.Kubert.tateSuccessiveX_zero (b c : ℚ) : tateSuccessiveX b c 0 = b

@[simp]

theorem MazurTorsion.Kubert.tateSuccessiveY_zero (b c : ℚ) : tateSuccessiveY b c 0 = b * c

@[simp]

theorem MazurTorsion.Kubert.tateSuccessiveX_succ (b c : ℚ) (n : ℕ) : tateSuccessiveX b c (n + 1) = tateNextX b c (tateSuccessiveX b c n) (tateSuccessiveY b c n)

@[simp]

theorem MazurTorsion.Kubert.tateSuccessiveY_succ (b c : ℚ) (n : ℕ) : tateSuccessiveY b c (n + 1) = tateNextY b c (tateSuccessiveX b c n) (tateSuccessiveY b c n)

theorem MazurTorsion.Kubert.nsmul_origin_eq_successiveCoordinates (b c : ℚ) (hb : b ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) (n : ℕ) (hx : ∀ k < n, tateSuccessiveX b c k ≠ 0) : ∃ (h : (tateNormalCurve b c).toAffine.Nonsingular (tateSuccessiveX b c n) (tateSuccessiveY b c n)), (n + 2) • WeierstrassCurve.Affine.Point.some 0 0 h00 = WeierstrassCurve.Affine.Point.some (tateSuccessiveX b c n) (tateSuccessiveY b c n) h

The rational recurrence computes (n + 2)P whenever every earlier abscissa used as a secant denominator is nonzero.

structure MazurTorsion.Kubert.TateClearedCoordinateDatum : Type

Fraction-free numerator and denominator data for one pair of Tate recurrence coordinates.

• xNum : ℚ

  Numerator of the x-coordinate.

• xDen : ℚ

  Denominator of the x-coordinate.

• yNum : ℚ

  Numerator of the y-coordinate.

• yDen : ℚ

  Denominator of the y-coordinate.

def MazurTorsion.Kubert.tateClearedNext (b c : ℚ) (Q : TateClearedCoordinateDatum) : TateClearedCoordinateDatum

One fraction-free step of the Tate recurrence. No division occurs in this definition; its specification theorem records the nonzero inputs needed to recover tateNextX and tateNextY.

Equations

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

def MazurTorsion.Kubert.tateClearedCoordinates (b c : ℚ) : ℕ → TateClearedCoordinateDatum

Fraction-free coordinates corresponding to tateSuccessiveCoordinates. Index zero is the cleared presentation (b/1, bc/1) of 2P.

Equations

• MazurTorsion.Kubert.tateClearedCoordinates b c 0 = { xNum := b, xDen := 1, yNum := b * c, yDen := 1 }
• MazurTorsion.Kubert.tateClearedCoordinates b c n.succ = MazurTorsion.Kubert.tateClearedNext b c (MazurTorsion.Kubert.tateClearedCoordinates b c n)

theorem MazurTorsion.Kubert.tateClearedCoordinates_spec (b c : ℚ) (n : ℕ) (hx : ∀ k < n, tateSuccessiveX b c k ≠ 0) : have Q := tateClearedCoordinates b c n; Q.xDen ≠ 0 ∧ Q.yDen ≠ 0 ∧ tateSuccessiveX b c n = Q.xNum / Q.xDen ∧ tateSuccessiveY b c n = Q.yNum / Q.yDen

The fraction-free recurrence represents the rational Tate recurrence, and all its denominators are nonzero whenever the abscissas used as secants are nonzero.

def MazurTorsion.Kubert.tateFiveX (b c : ℚ) : ℚ

The X-coordinate of 5P in Tate normal form.

Equations

• MazurTorsion.Kubert.tateFiveX b c = b * c * (c ^ 2 + c - b) / (b - c) ^ 2

def MazurTorsion.Kubert.tateFiveY (b c : ℚ) : ℚ

The Y-coordinate of 5P in Tate normal form.

Equations

• MazurTorsion.Kubert.tateFiveY b c = b * c ^ 2 * (b ^ 2 - b * c - c ^ 3) / (b - c) ^ 3

theorem MazurTorsion.Kubert.five_nsmul_origin_coordinates (b c : ℚ) (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) : ∃ (h₅ : (tateNormalCurve b c).toAffine.Nonsingular (tateFiveX b c) (tateFiveY b c)), 5 • WeierstrassCurve.Affine.Point.some 0 0 h00 = WeierstrassCurve.Affine.Point.some (tateFiveX b c) (tateFiveY b c) h₅

Provided b, c, and b-c are nonzero, the marked point has the displayed fifth multiple. These are exactly the denominators used in the calculation.

def MazurTorsion.Kubert.tateSixX (b c : ℚ) : ℚ

The recurrence-defined X-coordinate of 6P. Keeping the sixth multiple in recurrence form avoids expanding a much larger rational expression and makes subsequent calculations share the same checked addition interface.

Equations

• MazurTorsion.Kubert.tateSixX b c = MazurTorsion.Kubert.tateNextX b c (MazurTorsion.Kubert.tateFiveX b c) (MazurTorsion.Kubert.tateFiveY b c)

def MazurTorsion.Kubert.tateSixY (b c : ℚ) : ℚ

The recurrence-defined Y-coordinate of 6P.

Equations

• MazurTorsion.Kubert.tateSixY b c = MazurTorsion.Kubert.tateNextY b c (MazurTorsion.Kubert.tateFiveX b c) (MazurTorsion.Kubert.tateFiveY b c)

theorem MazurTorsion.Kubert.six_nsmul_origin_coordinates (b c : ℚ) (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (hfiveNumerator : c ^ 2 + c - b ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) : ∃ (h₆ : (tateNormalCurve b c).toAffine.Nonsingular (tateSixX b c) (tateSixY b c)), 6 • WeierstrassCurve.Affine.Point.some 0 0 h00 = WeierstrassCurve.Affine.Point.some (tateSixX b c) (tateSixY b c) h₆

If the additional fifth-multiple numerator c²+c-b is nonzero, the recurrence computes 6P. Together with b ≠ 0, c ≠ 0, and b ≠ c, this is precisely what proves that the X-coordinate of 5P is nonzero.