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.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.