Paired terms in Vélu's formulas

This file isolates the two elementary chord-law identities behind the paired form of Vélu's formulas. Pairing a point R = (r, s) with -R removes the source ordinate from the abscissa correction. The corresponding completed-ordinate sum is the formal derivative of that correction times the completed ordinate of the input point.

The total coordinate evaluators below assign zero to the point at infinity. This convention is convenient for finite kernel-orbit sums; the paired identities themselves only evaluate affine sums guaranteed by x ≠ r.

noncomputable def MazurTorsion.Velu.pointXOrZero (W : WeierstrassCurve ℚ) : W.toAffine.Point → ℚ

The abscissa of an affine point, extended by zero at infinity.

Equations

• MazurTorsion.Velu.pointXOrZero W WeierstrassCurve.Affine.Point.zero = 0
• MazurTorsion.Velu.pointXOrZero W (WeierstrassCurve.Affine.Point.some x_1 y h) = x_1

noncomputable def MazurTorsion.Velu.pointCompletedYOrZero (W : WeierstrassCurve ℚ) : W.toAffine.Point → ℚ

The completed ordinate 2y + a₁x + a₃ of an affine point, extended by zero at infinity.

Equations

• MazurTorsion.Velu.pointCompletedYOrZero W WeierstrassCurve.Affine.Point.zero = 0
• MazurTorsion.Velu.pointCompletedYOrZero W (WeierstrassCurve.Affine.Point.some x_1 y h) = 2 * y + W.a₁ * x_1 + W.a₃

@[simp]

theorem MazurTorsion.Velu.pointXOrZero_zero (W : WeierstrassCurve ℚ) : pointXOrZero W 0 = 0

@[simp]

theorem MazurTorsion.Velu.pointXOrZero_some (W : WeierstrassCurve ℚ) {x y : ℚ} (h : W.toAffine.Nonsingular x y) : pointXOrZero W (WeierstrassCurve.Affine.Point.some x y h) = x

@[simp]

theorem MazurTorsion.Velu.pointXOrZero_neg (W : WeierstrassCurve ℚ) (P : W.toAffine.Point) : pointXOrZero W (-P) = pointXOrZero W P

@[simp]

theorem MazurTorsion.Velu.pointCompletedYOrZero_zero (W : WeierstrassCurve ℚ) : pointCompletedYOrZero W 0 = 0

@[simp]

theorem MazurTorsion.Velu.pointCompletedYOrZero_some (W : WeierstrassCurve ℚ) {x y : ℚ} (h : W.toAffine.Nonsingular x y) : pointCompletedYOrZero W (WeierstrassCurve.Affine.Point.some x y h) = 2 * y + W.a₁ * x + W.a₃

@[simp]

theorem MazurTorsion.Velu.pointCompletedYOrZero_neg (W : WeierstrassCurve ℚ) (P : W.toAffine.Point) : pointCompletedYOrZero W (-P) = -pointCompletedYOrZero W P

def MazurTorsion.Velu.pairXCorrection (W : WeierstrassCurve ℚ) (x r s : ℚ) : ℚ

The paired abscissa correction contributed by R = (r, s) and -R.

Equations

• MazurTorsion.Velu.pairXCorrection W x r s = (6 * r ^ 2 + W.b₂ * r + W.b₄) / (x - r) + (2 * s + W.a₁ * r + W.a₃) ^ 2 / (x - r) ^ 2

def MazurTorsion.Velu.pairDifferentialCorrection (W : WeierstrassCurve ℚ) (x r s : ℚ) : ℚ

The formal derivative in x of pairXCorrection.

Equations

• MazurTorsion.Velu.pairDifferentialCorrection W x r s = -(6 * r ^ 2 + W.b₂ * r + W.b₄) / (x - r) ^ 2 - 2 * (2 * s + W.a₁ * r + W.a₃) ^ 2 / (x - r) ^ 3

theorem MazurTorsion.Velu.pointXOrZero_add_pair (W : WeierstrassCurve ℚ) {x y r s : ℚ} (hP : W.toAffine.Nonsingular x y) (hR : W.toAffine.Nonsingular r s) (hxr : x ≠ r) : pointXOrZero W (WeierstrassCurve.Affine.Point.some x y hP + WeierstrassCurve.Affine.Point.some r s hR) + pointXOrZero W (WeierstrassCurve.Affine.Point.some x y hP + -WeierstrassCurve.Affine.Point.some r s hR) - 2 * r = pairXCorrection W x r s

Pairing R and -R in the chord law gives the standard paired abscissa term in Vélu's formula.

theorem MazurTorsion.Velu.pointCompletedYOrZero_add_pair (W : WeierstrassCurve ℚ) {x y r s : ℚ} (hP : W.toAffine.Nonsingular x y) (hR : W.toAffine.Nonsingular r s) (hxr : x ≠ r) : pointCompletedYOrZero W (WeierstrassCurve.Affine.Point.some x y hP + WeierstrassCurve.Affine.Point.some r s hR) + pointCompletedYOrZero W (WeierstrassCurve.Affine.Point.some x y hP + -WeierstrassCurve.Affine.Point.some r s hR) = pairDifferentialCorrection W x r s * (2 * y + W.a₁ * x + W.a₃)

The paired completed-ordinate sum is the derivative correction times the completed ordinate of the input point.