structure ShortWeierstrassCurve (R : Type u_1) : Type u_1

A short Weierstrass curve $y^2 = x^3 + A x + B$ over a commutative ring $R$, parameterised by the coefficients $A$ and $B$.

• A : R
• B : R

noncomputable def ShortWeierstrassCurve.toWeierstrassCurve {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : WeierstrassCurve R

The underlying Mathlib WeierstrassCurve of a short Weierstrass curve, with $a_1 = a_2 = a_3 = 0$, $a_4 = A$, $a_6 = B$.

@[simp]

theorem ShortWeierstrassCurve.toWeierstrassCurve_a₁ {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.toWeierstrassCurve.a₁ = 0

The first Weierstrass coefficient $a_1$ of a short Weierstrass curve vanishes.

@[simp]

theorem ShortWeierstrassCurve.toWeierstrassCurve_a₂ {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.toWeierstrassCurve.a₂ = 0

The second Weierstrass coefficient $a_2$ of a short Weierstrass curve vanishes.

@[simp]

theorem ShortWeierstrassCurve.toWeierstrassCurve_a₃ {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.toWeierstrassCurve.a₃ = 0

The third Weierstrass coefficient $a_3$ of a short Weierstrass curve vanishes.

@[simp]

theorem ShortWeierstrassCurve.toWeierstrassCurve_a₄ {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.toWeierstrassCurve.a₄ = E.A

The fourth Weierstrass coefficient $a_4$ of a short Weierstrass curve equals $A$.

@[simp]

theorem ShortWeierstrassCurve.toWeierstrassCurve_a₆ {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.toWeierstrassCurve.a₆ = E.B

The sixth Weierstrass coefficient $a_6$ of a short Weierstrass curve equals $B$.

@[simp]

theorem ShortWeierstrassCurve.b₂_eq {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.toWeierstrassCurve.b₂ = 0

The auxiliary invariant $b_2 = a_1^2 + 4 a_2$ of a short Weierstrass curve vanishes.

@[simp]

theorem ShortWeierstrassCurve.b₄_eq {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.toWeierstrassCurve.b₄ = 2 * E.A

The auxiliary invariant $b_4 = 2 a_4 + a_1 a_3$ of a short Weierstrass curve equals $2A$.

@[simp]

theorem ShortWeierstrassCurve.b₆_eq {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.toWeierstrassCurve.b₆ = 4 * E.B

The auxiliary invariant $b_6 = a_3^2 + 4 a_6$ of a short Weierstrass curve equals $4B$.

@[simp]

theorem ShortWeierstrassCurve.b₈_eq {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.toWeierstrassCurve.b₈ = -E.A ^ 2

The auxiliary invariant $b_8$ of a short Weierstrass curve equals $-A^2$.

noncomputable def ShortWeierstrassCurve.divisionPoly {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : Polynomial (Polynomial R)

The $n$-th division polynomial $\psi_n \in R[X][Y]$ of a short Weierstrass curve, as a bivariate polynomial. Computed from Mathlib's WeierstrassCurve.ψ.

@[simp]

theorem ShortWeierstrassCurve.divisionPoly_zero {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.divisionPoly 0 = 0

The zeroth division polynomial vanishes, $\psi_0 = 0$.

@[simp]

theorem ShortWeierstrassCurve.divisionPoly_one {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.divisionPoly 1 = 1

The first division polynomial is $\psi_1 = 1$.

@[simp]

theorem ShortWeierstrassCurve.divisionPoly_two {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.divisionPoly 2 = E.toWeierstrassCurve.ψ₂

The second division polynomial is $\psi_2$, equal to the Mathlib helper ψ₂.

theorem ShortWeierstrassCurve.ψ₂_eq {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.toWeierstrassCurve.ψ₂ = Polynomial.C (Polynomial.C 2) * Polynomial.X

For a short Weierstrass curve, $\psi_2 = 2 Y$ (since $a_1 = a_3 = 0$).

@[simp]

theorem ShortWeierstrassCurve.divisionPoly_three {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.divisionPoly 3 = Polynomial.C E.toWeierstrassCurve.Ψ₃

The third division polynomial $\psi_3$ depends only on $X$ (it equals $C \, \Psi_3$).

@[simp]

theorem ShortWeierstrassCurve.divisionPoly_four {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.divisionPoly 4 = Polynomial.C E.toWeierstrassCurve.preΨ₄ * E.toWeierstrassCurve.ψ₂

The fourth division polynomial factors as $\psi_4 = C \, \mathrm{pre}\Psi_4 \cdot \psi_2$.

@[simp]

theorem ShortWeierstrassCurve.divisionPoly_neg {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : E.divisionPoly (-n) = -E.divisionPoly n

Negating the index negates the division polynomial: $\psi_{-n} = -\psi_n$.

theorem ShortWeierstrassCurve.divisionPoly_odd {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (m : ℤ) : E.divisionPoly (2 * m + 1) = E.divisionPoly (m + 2) * E.divisionPoly m ^ 3 - E.divisionPoly (m - 1) * E.divisionPoly (m + 1) ^ 3

Odd-index recurrence (Theorem 5.21): $\psi_{2m+1} = \psi_{m+2}\psi_m^3 - \psi_{m-1}\psi_{m+1}^3$.

theorem ShortWeierstrassCurve.divisionPoly_even {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (m : ℤ) : E.divisionPoly (2 * m) * E.toWeierstrassCurve.ψ₂ = E.divisionPoly (m - 1) ^ 2 * E.divisionPoly m * E.divisionPoly (m + 2) - E.divisionPoly (m - 2) * E.divisionPoly m * E.divisionPoly (m + 1) ^ 2

Even-index recurrence (Theorem 5.21): $\psi_{2m} \psi_2 = \psi_{m-1}^2 \psi_m \psi_{m+2}

• \psi_{m-2}\psi_m \psi_{m+1}^2$.

noncomputable def ShortWeierstrassCurve.phiPoly {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : Polynomial (Polynomial R)

The $x$-coordinate numerator polynomial $\phi_n \in R[X][Y]$ used in the multiplication-by-$n$ map: $\phi_n = X \psi_n^2 - \psi_{n+1} \psi_{n-1}$.

theorem ShortWeierstrassCurve.phiPoly_eq {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : E.phiPoly n = Polynomial.C Polynomial.X * E.divisionPoly n ^ 2 - E.divisionPoly (n + 1) * E.divisionPoly (n - 1)

Defining identity: $\phi_n = C X \cdot \psi_n^2 - \psi_{n+1} \cdot \psi_{n-1}$.

@[simp]

theorem ShortWeierstrassCurve.phiPoly_zero {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.phiPoly 0 = 1

The zeroth $\phi$-polynomial is $\phi_0 = 1$.

@[simp]

theorem ShortWeierstrassCurve.phiPoly_one {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.phiPoly 1 = Polynomial.C Polynomial.X

The first $\phi$-polynomial is $\phi_1 = X$.

@[simp]

theorem ShortWeierstrassCurve.phiPoly_neg {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : E.phiPoly (-n) = E.phiPoly n

The $\phi$-polynomial is invariant under negation of the index: $\phi_{-n} = \phi_n$.

noncomputable def ShortWeierstrassCurve.omegaPolyNumer {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : Polynomial (Polynomial R)

The numerator polynomial of $\omega_n$ (the $y$-coordinate piece of $[n]$), defined as $\psi_{n+2}\psi_{n-1}^2 - \psi_{n-2}\psi_{n+1}^2$.

theorem ShortWeierstrassCurve.Psi_odd {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) (hn : ¬Even n) : E.toWeierstrassCurve.Ψ n = Polynomial.C (E.toWeierstrassCurve.preΨ n)

For odd $n$, Mathlib's $\Psi_n$ collapses to $C(\mathrm{pre}\Psi_n)$ (no $\psi_2$ factor).

theorem ShortWeierstrassCurve.Psi_even {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) (hn : Even n) : E.toWeierstrassCurve.Ψ n = Polynomial.C (E.toWeierstrassCurve.preΨ n) * E.toWeierstrassCurve.ψ₂

For even $n$, Mathlib's $\Psi_n$ equals $C(\mathrm{pre}\Psi_n) \cdot \psi_2$.

theorem ShortWeierstrassCurve.omegaPolyNumer_mk_even {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) (hn : Even n) : (WeierstrassCurve.Affine.CoordinateRing.mk E.toWeierstrassCurve) (E.omegaPolyNumer n) = (WeierstrassCurve.Affine.CoordinateRing.mk E.toWeierstrassCurve) (E.toWeierstrassCurve.ψ₂ * Polynomial.C (E.toWeierstrassCurve.preΨ (n + 2) * E.toWeierstrassCurve.preΨ (n - 1) ^ 2 - E.toWeierstrassCurve.preΨ (n - 2) * E.toWeierstrassCurve.preΨ (n + 1) ^ 2))

For even $n$, the image of omegaPolyNumer n in the coordinate ring equals $\psi_2 \cdot C(\text{pre}\Psi\text{-combination})$.

theorem ShortWeierstrassCurve.omegaPolyNumer_mk_odd {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) (hn : ¬Even n) : (WeierstrassCurve.Affine.CoordinateRing.mk E.toWeierstrassCurve) (E.omegaPolyNumer n) = (WeierstrassCurve.Affine.CoordinateRing.mk E.toWeierstrassCurve) (E.toWeierstrassCurve.ψ₂ ^ 2 * Polynomial.C (E.toWeierstrassCurve.preΨ (n + 2) * E.toWeierstrassCurve.preΨ (n - 1) ^ 2 - E.toWeierstrassCurve.preΨ (n - 2) * E.toWeierstrassCurve.preΨ (n + 1) ^ 2))

For odd $n$, the image of omegaPolyNumer n in the coordinate ring equals $\psi_2^2 \cdot C(\text{pre}\Psi\text{-combination})$.

theorem ShortWeierstrassCurve.preΨ_omega_comb_even_div2 {R : Type u_2} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) (hn : Even n) : ∃ (h : Polynomial R), W.preΨ (n + 2) * W.preΨ (n - 1) ^ 2 - W.preΨ (n - 2) * W.preΨ (n + 1) ^ 2 = Polynomial.C 2 * h

For even $n$, the polynomial combination of preΨ is divisible by $2$, witnessed by some half $h \in R[X]$.

theorem ShortWeierstrassCurve.divisionPoly_neg_sq {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : E.divisionPoly (-n) ^ 2 = E.divisionPoly n ^ 2

Squaring is invariant under negation of the index: $\psi_{-n}^2 = \psi_n^2$.

theorem ShortWeierstrassCurve.x_coord_neg_invariant {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : E.phiPoly (-n) = E.phiPoly n ∧ E.divisionPoly (-n) ^ 2 = E.divisionPoly n ^ 2

The $x$-coordinate of $[n]P$ is unchanged by $n \mapsto -n$: both $\phi_n$ and $\psi_n^2$ are invariant under $n \mapsto -n$.

theorem ShortWeierstrassCurve.psi_odd_verification {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (m : ℤ) : E.phiPoly m * E.divisionPoly (m + 1) ^ 2 - E.phiPoly (m + 1) * E.divisionPoly m ^ 2 = E.divisionPoly (2 * m + 1)

Odd-index addition identity (Theorem 5.21): the difference of cross terms $\phi_m \psi_{m+1}^2 - \phi_{m+1}\psi_m^2$ equals $\psi_{2m+1}$.

theorem ShortWeierstrassCurve.psi_even_verification {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (m : ℤ) : E.divisionPoly m * E.omegaPolyNumer m = E.divisionPoly (2 * m) * E.toWeierstrassCurve.ψ₂

Even-index verification (Theorem 5.21): $\psi_m \cdot \omega_n^{\mathrm{num}} = \psi_{2m} \cdot \psi_2$.

theorem ShortWeierstrassCurve.Phi_natDegree {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) [Nontrivial R] (n : ℤ) : (E.toWeierstrassCurve.Φ n).natDegree = n.natAbs ^ 2

Degree of $\Phi_n$: the natural degree of Mathlib's $\Phi_n$ equals $n^2$ (in absolute value).

theorem ShortWeierstrassCurve.Phi_leadingCoeff {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) [Nontrivial R] (n : ℤ) : (E.toWeierstrassCurve.Φ n).leadingCoeff = 1

Leading coefficient of $\Phi_n$ is $1$ (the polynomial is monic).

theorem ShortWeierstrassCurve.preΨ_natDegree {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) {n : ℤ} (h : ↑n ≠ 0) : (E.toWeierstrassCurve.preΨ n).natDegree = (n.natAbs ^ 2 - if Even n then 4 else 1) / 2

Degree of $\mathrm{pre}\Psi_n$: when $n \neq 0$ in $R$, its $\mathrm{natDegree}$ equals $(n^2 - 4)/2$ for even $n$ and $(n^2 - 1)/2$ for odd $n$.

theorem ShortWeierstrassCurve.preΨ_leadingCoeff {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) {n : ℤ} (h : ↑n ≠ 0) : (E.toWeierstrassCurve.preΨ n).leadingCoeff = ↑(if Even n then n / 2 else n)

Leading coefficient of $\mathrm{pre}\Psi_n$: it equals $n/2$ for even $n$ and $n$ for odd $n$ (when $n \neq 0$ in $R$).

theorem ShortWeierstrassCurve.ΨSq_natDegree {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) [NoZeroDivisors R] {n : ℤ} (h : ↑n ≠ 0) : (E.toWeierstrassCurve.ΨSq n).natDegree = n.natAbs ^ 2 - 1

Degree of $\Psi_n^2$: when $n \neq 0$ in $R$, $\mathrm{natDegree}(\Psi_n^2) = n^2 - 1$.

theorem ShortWeierstrassCurve.ΨSq_leadingCoeff {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) [NoZeroDivisors R] {n : ℤ} (h : ↑n ≠ 0) : (E.toWeierstrassCurve.ΨSq n).leadingCoeff = ↑n ^ 2

Leading coefficient of $\Psi_n^2$ equals $n^2$.

theorem ShortWeierstrassCurve.ΨSq_leading_term {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) [NoZeroDivisors R] {n : ℤ} (h : ↑n ≠ 0) : (E.toWeierstrassCurve.ΨSq n).natDegree = n.natAbs ^ 2 - 1 ∧ (E.toWeierstrassCurve.ΨSq n).leadingCoeff = ↑n ^ 2

Combined statement of degree and leading coefficient of $\Psi_n^2$.

theorem ShortWeierstrassCurve.toWeierstrassCurve_short_form {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : E.toWeierstrassCurve.a₁ = 0 ∧ E.toWeierstrassCurve.a₂ = 0 ∧ E.toWeierstrassCurve.a₃ = 0

A short Weierstrass curve has $a_1 = a_2 = a_3 = 0$.

noncomputable def Polynomial.evalBivariate {S : Type u_1} [CommRing S] (p : Polynomial (Polynomial S)) (x₀ y₀ : S) : S

Evaluate a bivariate polynomial $p \in S[X][Y]$ at a point $(x_0, y_0) \in S \times S$ by first specialising $Y \mapsto y_0$ then $X \mapsto x_0$.

noncomputable def ShortWeierstrassCurve.evalDivisionPoly {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (n : ℤ) (x₀ y₀ : F) : F

Numeric evaluation of $\psi_n$ at the affine point $(x_0, y_0)$.

noncomputable def ShortWeierstrassCurve.evalPhiPoly {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (n : ℤ) (x₀ y₀ : F) : F

Numeric evaluation of $\phi_n$ at the affine point $(x_0, y_0)$.

noncomputable def ShortWeierstrassCurve.evalOmegaNumer {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (n : ℤ) (x₀ y₀ : F) : F

Numeric evaluation of the $\omega_n$-numerator polynomial at $(x_0, y_0)$.

noncomputable def ShortWeierstrassCurve.mulByN_x {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (n : ℤ) (x₀ y₀ : F) : F

The $x$-coordinate of $[n] P$ for $P = (x_0, y_0)$, given by $\phi_n / \psi_n^2$.

noncomputable def ShortWeierstrassCurve.evalOmega {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (n : ℤ) (x₀ y₀ : F) : F

Numeric value of $\omega_n(P) = \omega_n^{\mathrm{num}}/(4y_0)$ at the affine point $P = (x_0, y_0)$.

noncomputable def ShortWeierstrassCurve.mulByN_y {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (n : ℤ) (x₀ y₀ : F) : F

The $y$-coordinate of $[n] P$ for $P = (x_0, y_0)$, given by $\omega_n / \psi_n^3$.

@[simp]

theorem ShortWeierstrassCurve.evalDivisionPoly_one {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (x₀ y₀ : F) : E.evalDivisionPoly 1 x₀ y₀ = 1

Base case: $\psi_1$ evaluates to $1$ at any point.

@[simp]

theorem ShortWeierstrassCurve.evalPhiPoly_one {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (x₀ y₀ : F) : E.evalPhiPoly 1 x₀ y₀ = x₀

Base case: $\phi_1(x_0, y_0) = x_0$.

theorem ShortWeierstrassCurve.mulByN_x_one {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (x₀ y₀ : F) : E.mulByN_x 1 x₀ y₀ = x₀

Base case: $[1] P$ has $x$-coordinate $x_0$.

theorem ShortWeierstrassCurve.four_ne_zero_of_isElliptic {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) [hE : E.toWeierstrassCurve.IsElliptic] : 4 ≠ 0

Over an elliptic short Weierstrass curve, $4 \neq 0$ in the base field $F$ (otherwise $\Delta = 0$).

theorem ShortWeierstrassCurve.evalOmegaNumer_one {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (x₀ y₀ : F) : E.evalOmegaNumer 1 x₀ y₀ = 4 * y₀ ^ 2

Base case: $\omega_1^{\mathrm{num}}(x_0, y_0) = 4 y_0^2$.

theorem ShortWeierstrassCurve.mulByN_y_one {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) [E.toWeierstrassCurve.IsElliptic] (x₀ y₀ : F) : E.mulByN_y 1 x₀ y₀ = y₀

Base case: $[1] P$ has $y$-coordinate $y_0$.

theorem ShortWeierstrassCurve.mul_eq_divisionPoly_coords {F : Type u_2} [Field F] [DecidableEq F] (E : ShortWeierstrassCurve F) [E.toWeierstrassCurve.IsElliptic] {x₀ y₀ : F} (hP : E.toWeierstrassCurve.toAffine.Nonsingular x₀ y₀) {n : ℤ} (hn : n ≠ 0) (hψ : E.evalDivisionPoly n x₀ y₀ ≠ 0) : ∃ (h : E.toWeierstrassCurve.toAffine.Nonsingular (E.mulByN_x n x₀ y₀) (E.mulByN_y n x₀ y₀)), n • WeierstrassCurve.Affine.Point.some x₀ y₀ hP = WeierstrassCurve.Affine.Point.some (E.mulByN_x n x₀ y₀) (E.mulByN_y n x₀ y₀) h

Theorem 5.21 (algebraic form): when $\psi_n$ does not vanish at $P$, the affine point $(x_0, y_0)$ is sent under $[n]$ to the point $(\mathrm{mulByN}_x, \mathrm{mulByN}_y)$.

theorem ShortWeierstrassCurve.mul_eq_zero_of_divisionPoly_eq_zero {F : Type u_2} [Field F] [DecidableEq F] (E : ShortWeierstrassCurve F) [E.toWeierstrassCurve.IsElliptic] {x₀ y₀ : F} (hP : E.toWeierstrassCurve.toAffine.Nonsingular x₀ y₀) {n : ℤ} (hn : n ≠ 0) (hψ : E.evalDivisionPoly n x₀ y₀ = 0) : n • WeierstrassCurve.Affine.Point.some x₀ y₀ hP = WeierstrassCurve.Affine.Point.zero

Theorem 5.21 (algebraic form): when $\psi_n$ vanishes at $P$, the affine point is an $n$-torsion point ($[n] P = O$).

theorem ShortWeierstrassCurve.theorem_5_21_algebraic {R : Type u_2} [CommRing R] (E : ShortWeierstrassCurve R) : (∀ (n : ℤ), E.phiPoly (-n) = E.phiPoly n ∧ E.divisionPoly (-n) ^ 2 = E.divisionPoly n ^ 2) ∧ (∀ (m : ℤ), E.phiPoly m * E.divisionPoly (m + 1) ^ 2 - E.phiPoly (m + 1) * E.divisionPoly m ^ 2 = E.divisionPoly (2 * m + 1)) ∧ ∀ (m : ℤ), E.divisionPoly m * E.omegaPolyNumer m = E.divisionPoly (2 * m) * E.toWeierstrassCurve.ψ₂

Theorem 5.21 (purely algebraic): three identities characterising the division polynomials. The first asserts $n \mapsto -n$ symmetry; the second is the odd recurrence; the third is the even recurrence.

theorem ShortWeierstrassCurve.smul_eq_divisionPoly_cases {F : Type u_2} [Field F] [DecidableEq F] (E : ShortWeierstrassCurve F) [E.toWeierstrassCurve.IsElliptic] {x₀ y₀ : F} (hP : E.toWeierstrassCurve.toAffine.Nonsingular x₀ y₀) {n : ℤ} (hn : n ≠ 0) : (E.evalDivisionPoly n x₀ y₀ ≠ 0 → ∃ (h : E.toWeierstrassCurve.toAffine.Nonsingular (E.mulByN_x n x₀ y₀) (E.mulByN_y n x₀ y₀)), n • WeierstrassCurve.Affine.Point.some x₀ y₀ hP = WeierstrassCurve.Affine.Point.some (E.mulByN_x n x₀ y₀) (E.mulByN_y n x₀ y₀) h) ∧ (E.evalDivisionPoly n x₀ y₀ = 0 → n • WeierstrassCurve.Affine.Point.some x₀ y₀ hP = WeierstrassCurve.Affine.Point.zero)

Theorem 5.21: case split on whether $\psi_n(P)$ vanishes, returning either the affine formulae for $[n] P$ or that $[n] P = O$.

theorem ShortWeierstrassCurve.common_root_torsion_contradiction_aux {F : Type u_1} [Field F] [DecidableEq F] [IsAlgClosed F] (E : ShortWeierstrassCurve F) [E.toWeierstrassCurve.IsElliptic] {x₀ : F} {n : ℤ} (hn : n ≠ 0) (hΦ : (Polynomial.aeval x₀) (E.toWeierstrassCurve.Φ n) = 0) (hΨ : (Polynomial.aeval x₀) (E.toWeierstrassCurve.ΨSq n) = 0) : ∃ (y₀ : F) (hP : E.toWeierstrassCurve.toAffine.Nonsingular x₀ y₀), n • WeierstrassCurve.Affine.Point.some x₀ y₀ hP = WeierstrassCurve.Affine.Point.zero ∧ ((n - 1) • WeierstrassCurve.Affine.Point.some x₀ y₀ hP = WeierstrassCurve.Affine.Point.zero ∨ (n + 1) • WeierstrassCurve.Affine.Point.some x₀ y₀ hP = WeierstrassCurve.Affine.Point.zero)

Auxiliary lemma for the coprimality of $\Phi_n$ and $\Psi_n^2$: a common root would witness an affine $n$-torsion point that is also $(n \pm 1)$-torsion, contradicting nontriviality.

theorem ShortWeierstrassCurve.Phi_ΨSq_isCoprime {k : Type uSWC} [Field k] (E : ShortWeierstrassCurve k) [E.toWeierstrassCurve.IsElliptic] (n : ℤ) : IsCoprime (E.toWeierstrassCurve.Φ n) (E.toWeierstrassCurve.ΨSq n)

The polynomials $\Phi_n$ and $\Psi_n^2$ are coprime over an elliptic short Weierstrass curve, used to extract the multiplication-by-$n$ map as a standard-form isogeny.

structure ShortWeierstrassCurve.VeluDeg2Data {k : Type u_1} [CommRing k] (E : ShortWeierstrassCurve k) : Type u_1

Data for the degree-$2$ Vélu isogeny: a $2$-torsion $x$-coordinate $x_0$ satisfying $x_0^3 + A x_0 + B = 0$.

• x₀ : k
• root_eq : self.x₀ ^ 3 + E.A * self.x₀ + E.B = 0

def ShortWeierstrassCurve.VeluDeg2Data.t {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) : k

Vélu parameter $t = 3 x_0^2 + A$.

def ShortWeierstrassCurve.VeluDeg2Data.w {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) : k

Vélu parameter $w = x_0 t = x_0 (3 x_0^2 + A)$.

def ShortWeierstrassCurve.VeluDeg2Data.A' {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) : k

Vélu image parameter $A' = A - 5 t$ for the codomain curve.

def ShortWeierstrassCurve.VeluDeg2Data.B' {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) : k

Vélu image parameter $B' = B - 7 w$ for the codomain curve.

def ShortWeierstrassCurve.VeluDeg2Data.imageCurve {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) : ShortWeierstrassCurve k

The image curve $E' : y^2 = x^3 + A' x + B'$ of the Vélu degree-$2$ isogeny.

@[simp]

theorem ShortWeierstrassCurve.VeluDeg2Data.imageCurve_A {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) : d.imageCurve.A = d.A'

Unfolding the $A$-coefficient of the image curve.

@[simp]

theorem ShortWeierstrassCurve.VeluDeg2Data.imageCurve_B {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) : d.imageCurve.B = d.B'

Unfolding the $B$-coefficient of the image curve.

theorem ShortWeierstrassCurve.VeluDeg2Data.t_eq {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) : d.t = 3 * d.x₀ ^ 2 + E.A

Defining identity for $t$.

theorem ShortWeierstrassCurve.VeluDeg2Data.w_eq {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) : d.w = d.x₀ * (3 * d.x₀ ^ 2 + E.A)

Defining identity for $w$.

theorem ShortWeierstrassCurve.VeluDeg2Data.kernel_point_on_curve {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) : d.x₀ ^ 3 + E.A * d.x₀ + E.B = 0

The $2$-torsion point $(x_0, 0)$ lies on $E$ since $x_0^3 + A x_0 + B = 0$.

theorem ShortWeierstrassCurve.VeluDeg2Data.velu_image_identity {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) (x : k) : (x ^ 2 - d.x₀ * x + d.t) ^ 3 + d.A' * (x ^ 2 - d.x₀ * x + d.t) * (x - d.x₀) ^ 2 + d.B' * (x - d.x₀) ^ 3 = ((x - d.x₀) ^ 2 - d.t) ^ 2 * (x ^ 2 + d.x₀ * x + d.x₀ ^ 2 + E.A)

The key algebraic identity for the Vélu degree-$2$ map: the cubic in the numerator factors compatibly with the image curve equation.

def ShortWeierstrassCurve.VeluDeg2Data.phi_x_numer {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) (x : k) : k

Numerator of the $x$-coordinate component $\phi_x(x) = x^2 - x_0 x + t$.

def ShortWeierstrassCurve.VeluDeg2Data.phi_x_denom {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) (x : k) : k

Denominator of the $x$-coordinate component $\phi_x$, namely $x - x_0$.

def ShortWeierstrassCurve.VeluDeg2Data.phi_y_numer_factor {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) (x : k) : k

Factor appearing in the $y$-coordinate numerator: $(x - x_0)^2 - t$.

def ShortWeierstrassCurve.VeluDeg2Data.phi_y_denom {k : Type u_1} [CommRing k] {E : ShortWeierstrassCurve k} (d : E.VeluDeg2Data) (x : k) : k

Denominator of the $y$-coordinate component: $(x - x_0)^2$.

theorem ShortWeierstrassCurve.VeluDeg2Data.velu_u_natDegree {F : Type u_2} [Field F] {E : ShortWeierstrassCurve F} (d : E.VeluDeg2Data) : (Polynomial.X ^ 2 - Polynomial.C d.x₀ * Polynomial.X + Polynomial.C d.t).natDegree = 2

Natural degree of the Vélu $u$-polynomial $X^2 - x_0 X + t$ over a field is $2$.

theorem ShortWeierstrassCurve.VeluDeg2Data.velu_wronskian_eq {F : Type u_2} [Field F] {E : ShortWeierstrassCurve F} (d : E.VeluDeg2Data) : Polynomial.derivative (Polynomial.X ^ 2 - Polynomial.C d.x₀ * Polynomial.X + Polynomial.C d.t) * (Polynomial.X - Polynomial.C d.x₀) - (Polynomial.X ^ 2 - Polynomial.C d.x₀ * Polynomial.X + Polynomial.C d.t) * Polynomial.derivative (Polynomial.X - Polynomial.C d.x₀) = (Polynomial.X - Polynomial.C d.x₀) ^ 2 - Polynomial.C d.t

The Wronskian of the Vélu degree-$2$ pair simplifies to $(X - x_0)^2 - t$.

theorem ShortWeierstrassCurve.VeluDeg2Data.velu_deg2_is_separable {F : Type u_2} [Field F] {E : ShortWeierstrassCurve F} (d : E.VeluDeg2Data) : Polynomial.derivative (Polynomial.X ^ 2 - Polynomial.C d.x₀ * Polynomial.X + Polynomial.C d.t) * (Polynomial.X - Polynomial.C d.x₀) - (Polynomial.X ^ 2 - Polynomial.C d.x₀ * Polynomial.X + Polynomial.C d.t) * Polynomial.derivative (Polynomial.X - Polynomial.C d.x₀) ≠ 0

Separability of the Vélu degree-$2$ map: the Wronskian is nonzero.

theorem ShortWeierstrassCurve.VeluDeg2Data.velu_deg2_degree_eq_two {F : Type u_2} [Field F] {E : ShortWeierstrassCurve F} (d : E.VeluDeg2Data) : max (Polynomial.X ^ 2 - Polynomial.C d.x₀ * Polynomial.X + Polynomial.C d.t).natDegree (Polynomial.X - Polynomial.C d.x₀).natDegree = 2

The Vélu degree-$2$ map has degree $2$: $\max(\deg u, \deg v) = 2$.

theorem ShortWeierstrassCurve.VeluDeg2Data.velu_deg2_kernel_on_curve {F : Type u_2} [Field F] {E : ShortWeierstrassCurve F} (d : E.VeluDeg2Data) : 0 ^ 2 = d.x₀ ^ 3 + E.A * d.x₀ + E.B

The $2$-torsion kernel point $(x_0, 0)$ lies on the curve: $0^2 = x_0^3 + A x_0 + B$.

theorem ShortWeierstrassCurve.VeluDeg2Data.velu_deg2_kernel_denom_vanish {F : Type u_2} [Field F] {E : ShortWeierstrassCurve F} (d : E.VeluDeg2Data) : d.phi_x_denom d.x₀ = 0 ∧ d.phi_y_denom d.x₀ = 0

The denominators of $\phi_x$ and $\phi_y$ vanish at the kernel point $x_0$.

theorem ShortWeierstrassCurve.VeluDeg2Data.velu_deg2_kernel_unique {F : Type u_2} [Field F] {E : ShortWeierstrassCurve F} (d : E.VeluDeg2Data) {x : F} (hx : x ≠ d.x₀) : d.phi_x_denom x ≠ 0

The kernel of $\phi_x$ is exactly $\{x_0\}$: the denominator does not vanish elsewhere.

theorem ShortWeierstrassCurve.VeluDeg2Data.velu_y_sq_factor {F : Type u_2} [Field F] {E : ShortWeierstrassCurve F} (d : E.VeluDeg2Data) {x y : F} (hcurve : y ^ 2 = x ^ 3 + E.A * x + E.B) : y ^ 2 = (x - d.x₀) * (x ^ 2 + d.x₀ * x + d.x₀ ^ 2 + E.A)

On the curve, $y^2$ factors as $(x - x_0)(x^2 + x_0 x + x_0^2 + A)$.

theorem ShortWeierstrassCurve.VeluDeg2Data.velu_phi_maps_points {F : Type u_2} [Field F] {E : ShortWeierstrassCurve F} (d : E.VeluDeg2Data) {x y : F} (hcurve : y ^ 2 = x ^ 3 + E.A * x + E.B) : ((x - d.x₀) ^ 2 - d.t) ^ 2 * y ^ 2 = (x - d.x₀) * ((x ^ 2 - d.x₀ * x + d.t) ^ 3 + d.A' * (x ^ 2 - d.x₀ * x + d.t) * (x - d.x₀) ^ 2 + d.B' * (x - d.x₀) ^ 3)

The Vélu degree-$2$ map sends an on-curve point $(x, y)$ to a point on the image curve.

theorem ShortWeierstrassCurve.VeluDeg2Data.velu_deg2_is_standard_form_separable_deg2 {F : Type u_2} [Field F] {E : ShortWeierstrassCurve F} (d : E.VeluDeg2Data) : max (Polynomial.X ^ 2 - Polynomial.C d.x₀ * Polynomial.X + Polynomial.C d.t).natDegree (Polynomial.X - Polynomial.C d.x₀).natDegree = 2 ∧ Polynomial.derivative (Polynomial.X ^ 2 - Polynomial.C d.x₀ * Polynomial.X + Polynomial.C d.t) * (Polynomial.X - Polynomial.C d.x₀) - (Polynomial.X ^ 2 - Polynomial.C d.x₀ * Polynomial.X + Polynomial.C d.t) * Polynomial.derivative (Polynomial.X - Polynomial.C d.x₀) ≠ 0

The Vélu degree-$2$ map is a standard-form separable isogeny of degree $2$.

structure ShortWeierstrassCurve.VeluDeg2Data.VeluDeg2Kernel {F : Type u_2} [Field F] (E : ShortWeierstrassCurve F) (d : E.VeluDeg2Data) : Prop

Bundled kernel data for the Vélu degree-$2$ isogeny: the kernel point is on $E$, the denominators vanish at it, are nonzero elsewhere, and the kernel has order $2$.

• kernel_point_on_E : 0 ^ 2 = d.x₀ ^ 3 + E.A * d.x₀ + E.B
• kernel_point_maps_to_zero : d.phi_x_denom d.x₀ = 0
• nonkernel_welldefined (x : F) : x ≠ d.x₀ → d.phi_x_denom x ≠ 0
• kernel_order : {(d.x₀, 0)}.card + 1 = 2

def ShortWeierstrassCurve.VeluDeg2Data.velu_deg2_kernel {F : Type u_2} [Field F] {E : ShortWeierstrassCurve F} (d : E.VeluDeg2Data) : VeluDeg2Kernel E d

The Vélu degree-$2$ kernel data associated to a Vélu degree-$2$ datum.

structure ShortWeierstrassCurve.VeluDeg2Data.VeluDeg2Isogeny {F : Type u_2} [Field F] (E : ShortWeierstrassCurve F) (d : E.VeluDeg2Data) : Prop

Bundled Vélu degree-$2$ isogeny: a standard-form separable degree-$2$ isogeny together with its kernel datum.

• phi_maps_points (x y : F) : y ^ 2 = x ^ 3 + E.A * x + E.B → ((x - d.x₀) ^ 2 - d.t) ^ 2 * y ^ 2 = (x - d.x₀) * ((x ^ 2 - d.x₀ * x + d.t) ^ 3 + d.A' * (x ^ 2 - d.x₀ * x + d.t) * (x - d.x₀) ^ 2 + d.B' * (x - d.x₀) ^ 3)
• degree_eq_two : max (Polynomial.X ^ 2 - Polynomial.C d.x₀ * Polynomial.X + Polynomial.C d.t).natDegree (Polynomial.X - Polynomial.C d.x₀).natDegree = 2
• is_separable : Polynomial.derivative (Polynomial.X ^ 2 - Polynomial.C d.x₀ * Polynomial.X + Polynomial.C d.t) * (Polynomial.X - Polynomial.C d.x₀) - (Polynomial.X ^ 2 - Polynomial.C d.x₀ * Polynomial.X + Polynomial.C d.t) * Polynomial.derivative (Polynomial.X - Polynomial.C d.x₀) ≠ 0
• kernel : VeluDeg2Kernel E d

def ShortWeierstrassCurve.VeluDeg2Data.velu_deg2_isogeny {F : Type u_2} [Field F] {E : ShortWeierstrassCurve F} (d : E.VeluDeg2Data) : VeluDeg2Isogeny E d

The Vélu degree-$2$ isogeny constructed from a Vélu datum.

structure ShortWeierstrassCurve.AffinePoint {k : Type u_2} [Field k] (E : ShortWeierstrassCurve k) : Type u_2

An affine point on a short Weierstrass curve: a pair $(x, y)$ together with a proof that $y^2 = x^3 + A x + B$.

• x : k
• y : k
• on_curve : self.y ^ 2 = self.x ^ 3 + E.A * self.x + E.B

def ShortWeierstrassCurve.AffinePoint.tQ {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (Q : E.AffinePoint) : k

Vélu parameter $t_Q = 3 x_Q^2 + A$ associated with an affine point $Q$.

def ShortWeierstrassCurve.AffinePoint.uQ {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (Q : E.AffinePoint) : k

Vélu parameter $u_Q = 2 y_Q^2$ associated with an affine point $Q$.

def ShortWeierstrassCurve.AffinePoint.wQ {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (Q : E.AffinePoint) : k

Vélu parameter $w_Q = u_Q + t_Q x_Q$ associated with an affine point $Q$.

@[simp]

theorem ShortWeierstrassCurve.AffinePoint.tQ_val {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (Q : E.AffinePoint) : Q.tQ = 3 * Q.x ^ 2 + E.A

Unfolds $t_Q$ to its defining formula.

@[simp]

theorem ShortWeierstrassCurve.AffinePoint.uQ_val {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (Q : E.AffinePoint) : Q.uQ = 2 * Q.y ^ 2

Unfolds $u_Q$ to its defining formula.

@[simp]

theorem ShortWeierstrassCurve.AffinePoint.wQ_val {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (Q : E.AffinePoint) : Q.wQ = Q.uQ + Q.tQ * Q.x

Unfolds $w_Q$ to its defining formula $u_Q + t_Q x_Q$.

theorem ShortWeierstrassCurve.AffinePoint.wQ_expanded {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (Q : E.AffinePoint) : Q.wQ = 2 * Q.y ^ 2 + (3 * Q.x ^ 2 + E.A) * Q.x

Expanded form $w_Q = 2 y_Q^2 + (3 x_Q^2 + A) x_Q$.

theorem ShortWeierstrassCurve.AffinePoint.uQ_eq_curve {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (Q : E.AffinePoint) : Q.uQ = 2 * (Q.x ^ 3 + E.A * Q.x + E.B)

Using the curve equation, $u_Q = 2(x_Q^3 + A x_Q + B)$.

theorem ShortWeierstrassCurve.AffinePoint.wQ_eq_curve {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (Q : E.AffinePoint) : Q.wQ = 5 * Q.x ^ 3 + 3 * E.A * Q.x + 2 * E.B

Using the curve equation, $w_Q = 5 x_Q^3 + 3 A x_Q + 2 B$.

structure ShortWeierstrassCurve.VeluOddData {k : Type u_2} [Field k] (E : ShortWeierstrassCurve k) : Type u_2

Data for the odd-degree Vélu isogeny: a finite set of nonidentity affine points such that the kernel order $|S| + 1$ is odd.

• pts : Finset E.AffinePoint
• odd_order : Odd (self.pts.card + 1)

def ShortWeierstrassCurve.VeluOddData.t {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (d : E.VeluOddData) : k

Vélu sum $t = \sum_Q t_Q$ over the kernel points.

def ShortWeierstrassCurve.VeluOddData.w {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (d : E.VeluOddData) : k

Vélu sum $w = \sum_Q w_Q$ over the kernel points.

def ShortWeierstrassCurve.VeluOddData.A' {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (d : E.VeluOddData) : k

Vélu image coefficient $A' = A - 5 t$.

def ShortWeierstrassCurve.VeluOddData.B' {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (d : E.VeluOddData) : k

Vélu image coefficient $B' = B - 7 w$.

def ShortWeierstrassCurve.VeluOddData.imageCurve {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (d : E.VeluOddData) : ShortWeierstrassCurve k

The image curve $E' : y^2 = x^3 + A' x + B'$ of the odd-degree Vélu isogeny.

@[simp]

theorem ShortWeierstrassCurve.VeluOddData.imageCurve_A {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (d : E.VeluOddData) : d.imageCurve.A = d.A'

Unfolding the $A$-coefficient of the image curve.

@[simp]

theorem ShortWeierstrassCurve.VeluOddData.imageCurve_B {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (d : E.VeluOddData) : d.imageCurve.B = d.B'

Unfolding the $B$-coefficient of the image curve.

noncomputable def ShortWeierstrassCurve.VeluOddData.r {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (d : E.VeluOddData) (x : k) : k

The rational function $r(x) = x + \sum_Q \left(\tfrac{t_Q}{x - x_Q} + \tfrac{u_Q}{(x - x_Q)^2}\right)$ defining the $x$-coordinate component of the Vélu isogeny.

noncomputable def ShortWeierstrassCurve.VeluOddData.r' {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (d : E.VeluOddData) (x : k) : k

The derivative $r'(x) = 1 - \sum_Q \left(\tfrac{t_Q}{(x - x_Q)^2} + \tfrac{2 u_Q}{(x - x_Q)^3}\right)$ used in the $y$-coordinate component.

theorem ShortWeierstrassCurve.VeluOddData.velu_odd_maps_to_image {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (d : E.VeluOddData) (P : E.AffinePoint) (hP : ∀ Q ∈ d.pts, P.x ≠ Q.x) : (d.r' P.x * P.y) ^ 2 = d.r P.x ^ 3 + d.A' * d.r P.x + d.B'

The Vélu odd-degree map sends an on-curve point not in the kernel to a point on the image curve.

theorem ShortWeierstrassCurve.VeluOddData.velu_odd_is_separable_isogeny {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (d : E.VeluOddData) : ∃ (α : IsogenyStandardForm k), α.IsSeparable ∧ α.degree = d.pts.card + 1

The Vélu odd-degree map is a separable isogeny of degree $|S| + 1$.

theorem ShortWeierstrassCurve.VeluOddData.velu_odd_kernel_eq {k : Type u_2} [Field k] {E : ShortWeierstrassCurve k} (d : E.VeluOddData) : ∃ (α : IsogenyStandardForm k), α.degree = d.pts.card + 1 ∧ ∀ (x : k), Polynomial.eval x α.v = 0 ↔ ∃ Q ∈ d.pts, x = Q.x

The kernel of the Vélu odd-degree map is precisely the $x$-coordinate set $\{x_Q : Q \in S\}$.

theorem corollary_5_2 {F : Type u_1} [Field F] [CharZero F] (α : IsogenyStandardForm F) (hdeg : 0 < α.degree) : α.IsSeparable

Corollary 5.2: in characteristic zero, every isogeny of positive degree is separable.

def IsogenyStandardForm.HasFrobeniusFactorization {F : Type u_1} [Field F] {p : ℕ} [CharP F p] (α : IsogenyStandardForm F) : Prop

An isogeny $\alpha$ over a field of characteristic $p$ has a Frobenius factorisation if it factors as $\mathrm{Frob}^n \circ \alpha_{\mathrm{sep}}$ for a separable $\alpha_{\mathrm{sep}}$.

theorem IsogenyStandardForm.frobeniusFactorization {F : Type u_1} [Field F] {p : ℕ} [CharP F p] (hp : Nat.Prime p) (α : IsogenyStandardForm F) (hdeg : 0 < α.degree) : ∃ (α_sep : IsogenyStandardForm F) (n : ℕ), α_sep.IsSeparable ∧ α.u = (Polynomial.expand F (p ^ n)) α_sep.u ∧ α.v = (Polynomial.expand F (p ^ n)) α_sep.v ∧ α.degree = p ^ n * α_sep.degree

Frobenius factorisation: over a field of characteristic $p$, every positive-degree isogeny factors as $\alpha_{\mathrm{sep}}$ composed with $\mathrm{Frob}^n$.

theorem ShortWeierstrassCurve.derivative_Phi_ne_zero {k : Type uSWC} [Field k] (E : ShortWeierstrassCurve k) {n : ℤ} (hn : ↑n ≠ 0) : Polynomial.derivative (E.toWeierstrassCurve.Φ n) ≠ 0

Over an elliptic curve, the derivative of $\Phi_n$ is nonzero whenever $n \neq 0$ in $k$. This is the key separability ingredient for $[n]$.

noncomputable def ShortWeierstrassCurve.mulByNStandardForm {k : Type uSWC} [Field k] (E : ShortWeierstrassCurve k) [E.toWeierstrassCurve.IsElliptic] {n : ℤ} (hn : ↑n ≠ 0) : IsogenyStandardForm k

The multiplication-by-$n$ map packaged as an IsogenyStandardForm: numerator $\Phi_n$, denominator $\Psi_n^2$, on the elliptic short Weierstrass curve.

theorem ShortWeierstrassCurve.theorem_5_25_degree {k : Type uSWC} [Field k] (E : ShortWeierstrassCurve k) [E.toWeierstrassCurve.IsElliptic] {n : ℤ} (hn : ↑n ≠ 0) : (E.mulByNStandardForm hn).degree = n.natAbs ^ 2

Degree part of Theorem 5.25: $\deg[n] = n^2$ (when $n \neq 0$ in $k$).

theorem ShortWeierstrassCurve.theorem_5_25_separable {k : Type uSWC} [Field k] (E : ShortWeierstrassCurve k) [E.toWeierstrassCurve.IsElliptic] {n : ℤ} (hn : ↑n ≠ 0) : (E.mulByNStandardForm hn).IsSeparable

Separability part of Theorem 5.25: $[n]$ is separable when $n \neq 0$ in $k$.

theorem ShortWeierstrassCurve.divpoly_frobenius_structure {k : Type uSWC} [Field k] (E : ShortWeierstrassCurve k) {n : ℤ} (hn : n ≠ 0) (hc : ↑n = 0) : ∃ (f : Polynomial k) (g : Polynomial k), (Polynomial.expand k (ringChar k)) f = E.toWeierstrassCurve.Φ n ∧ (Polynomial.expand k (ringChar k)) g = E.toWeierstrassCurve.ΨSq n

When $n$ vanishes in $k$ (char $p \mid n$), both $\Phi_n$ and $\Psi_n^2$ are images of the Frobenius expansion: there exist polynomials $f, g$ with $\mathrm{expand}_p f = \Phi_n$, $\mathrm{expand}_p g = \Psi_n^2$.

theorem ShortWeierstrassCurve.theorem_5_25_inseparable {k : Type uSWC} [Field k] (E : ShortWeierstrassCurve k) {n : ℤ} (hn_ne_zero : n ≠ 0) (hn_char : ↑n = 0) : Polynomial.derivative (E.toWeierstrassCurve.Φ n) * E.toWeierstrassCurve.ΨSq n - E.toWeierstrassCurve.Φ n * Polynomial.derivative (E.toWeierstrassCurve.ΨSq n) = 0

Inseparability case of Theorem 5.25: when $n$ vanishes in $k$, the Wronskian of $\Phi_n$ and $\Psi_n^2$ is zero, so $[n]$ is inseparable.

theorem ShortWeierstrassCurve.theorem_5_25_separable_iff {k : Type uSWC} [Field k] (E : ShortWeierstrassCurve k) [E.toWeierstrassCurve.IsElliptic] {n : ℤ} (hn : n ≠ 0) : Polynomial.derivative (E.toWeierstrassCurve.Φ n) * E.toWeierstrassCurve.ΨSq n - E.toWeierstrassCurve.Φ n * Polynomial.derivative (E.toWeierstrassCurve.ΨSq n) ≠ 0 ↔ ↑n ≠ 0

Theorem 5.25 (separability $\iff$ $n$-nonvanishing): $[n]$ is separable iff $n \neq 0$ in $k$.

theorem ShortWeierstrassCurve.theorem_5_25_degree_general {k : Type uSWC} [Field k] (E : ShortWeierstrassCurve k) (n : ℤ) (hn : n ≠ 0) : max (E.toWeierstrassCurve.Φ n).natDegree (E.toWeierstrassCurve.ΨSq n).natDegree = n.natAbs ^ 2

General degree formula: for any nonzero $n$, $\max(\deg \Phi_n, \deg \Psi_n^2) = n^2$.

theorem ShortWeierstrassCurve.theorem_5_25 {k : Type uSWC} [Field k] (E : ShortWeierstrassCurve k) [E.toWeierstrassCurve.IsElliptic] {n : ℤ} (hn : n ≠ 0) : max (E.toWeierstrassCurve.Φ n).natDegree (E.toWeierstrassCurve.ΨSq n).natDegree = n.natAbs ^ 2 ∧ (Polynomial.derivative (E.toWeierstrassCurve.Φ n) * E.toWeierstrassCurve.ΨSq n - E.toWeierstrassCurve.Φ n * Polynomial.derivative (E.toWeierstrassCurve.ΨSq n) ≠ 0 ↔ ↑n ≠ 0)

Theorem 5.25 (combined): for nonzero $n$, $[n]$ has degree $n^2$ and is separable iff $n \neq 0$ in $k$.

def IsogenyStandardForm.HasSeparableDegree {F : Type u_1} [Field F] {p : ℕ} (_hp : Nat.Prime p) [CharP F p] (α : IsogenyStandardForm F) (d : ℕ) : Prop

An isogeny $\alpha$ has separable degree $d$ if it factors as $\mathrm{Frob}^n \circ \alpha_{\mathrm{sep}}$ with $\deg \alpha_{\mathrm{sep}} = d$.

def IsogenyStandardForm.HasInseparableDegree {F : Type u_1} [Field F] {p : ℕ} (_hp : Nat.Prime p) [CharP F p] (α : IsogenyStandardForm F) (d : ℕ) : Prop

An isogeny $\alpha$ has inseparable degree $d = p^n$ if its Frobenius factorisation has exponent $n$.

def IsogenyStandardForm.IsPurelyInseparable' {F : Type u_1} [Field F] {p : ℕ} (hp : Nat.Prime p) [CharP F p] (α : IsogenyStandardForm F) : Prop

An isogeny is purely inseparable if its separable degree is $1$.

noncomputable def IsogenyStandardForm.separableDegree {F : Type u_1} [Field F] (α : IsogenyStandardForm F) : ℕ

The separable degree of a standard-form isogeny: the maximum of the separable degrees of its numerator and denominator.

noncomputable def IsogenyStandardForm.inseparableDegree {F : Type u_1} [Field F] (α : IsogenyStandardForm F) : ℕ

The inseparable degree of a standard-form isogeny: total degree divided by separable degree.

def IsogenyStandardForm.IsPurelyInseparable {F : Type u_1} [Field F] (α : IsogenyStandardForm F) : Prop

An isogeny is purely inseparable if its separable degree equals $1$.

theorem IsogenyStandardForm.exists_separableDegree {F : Type u_1} [Field F] {p : ℕ} (hp : Nat.Prime p) [CharP F p] (α : IsogenyStandardForm F) (hdeg : 0 < α.degree) : ∃ (d : ℕ), HasSeparableDegree hp α d

Existence of separable degree: every positive-degree isogeny over a positive-characteristic field has a separable degree.

theorem IsogenyStandardForm.degree_eq_insep_mul_sep {F : Type u_1} [Field F] {p : ℕ} (_hp : Nat.Prime p) [CharP F p] (α : IsogenyStandardForm F) (_hdeg : 0 < α.degree) {d : ℕ} (hs : HasSeparableDegree _hp α d) : ∃ (n : ℕ), α.degree = p ^ n * d

The total degree of $\alpha$ equals $p^n$ times its separable degree, witnessing the $\deg = \deg_{\mathrm{insep}} \cdot \deg_{\mathrm{sep}}$ decomposition.

noncomputable def IsogenyStandardForm.kernelSize {F : Type u_1} [Field F] (α : IsogenyStandardForm F) : ℕ

The size of the kernel of $\alpha$, computed as $\max(\mathrm{natSepDegree}(u), \mathrm{natSepDegree}(v))$.

noncomputable def IsogenyStandardForm.groupKernelSize {F : Type u_1} [Field F] (α : IsogenyStandardForm F) : ℕ

The size of the kernel of $\alpha$ as an abstract group; this agrees with kernelSize (cf. groupKernelSize_eq_separableDegree).

theorem IsogenyStandardForm.groupKernelSize_eq_separableDegree {F : Type u_1} [Field F] (α : IsogenyStandardForm F) (hdeg : 0 < α.degree) : α.groupKernelSize = α.separableDegree

The group-theoretic kernel size equals the separable degree.

theorem IsogenyStandardForm.kernelSize_eq_separableDegree {F : Type u_1} [Field F] {p : ℕ} [CharP F p] (hp : Nat.Prime p) (α : IsogenyStandardForm F) (hdeg : 0 < α.degree) (d : ℕ) (hd : HasSeparableDegree hp α d) : α.kernelSize = d

The polynomial kernel size equals the separable degree (for a Frobenius factorisation witness).

theorem corollary_5_9 {F : Type u_1} [Field F] {p : ℕ} [CharP F p] (hp : Nat.Prime p) (α : IsogenyStandardForm F) (_hdeg : 0 < α.degree) (α_sep : IsogenyStandardForm F) (n : ℕ) (_hsep : α_sep.IsSeparable) (hu : α.u = (Polynomial.expand F (p ^ n)) α_sep.u) (hv : α.v = (Polynomial.expand F (p ^ n)) α_sep.v) (hpure : α_sep.degree = 1) : α.kernelSize = 1

Corollary 5.9: a purely inseparable Frobenius factorisation (separable degree $1$) implies the isogeny has kernel size $1$.

theorem corollary_5_9' {F : Type u_1} [Field F] {p : ℕ} [CharP F p] (hp : Nat.Prime p) (α : IsogenyStandardForm F) (hdeg : 0 < α.degree) (hpure : IsogenyStandardForm.IsPurelyInseparable' hp α) : α.kernelSize = 1

Corollary 5.9' (packaged form): if $\alpha$ is purely inseparable then its kernel size is $1$.

theorem purelyInseparable_of_kernelSize_eq_one {F : Type u_1} [Field F] {p : ℕ} [CharP F p] (hp : Nat.Prime p) (α : IsogenyStandardForm F) (hdeg : 0 < α.degree) (hker : α.kernelSize = 1) : IsogenyStandardForm.IsPurelyInseparable' hp α

Converse direction: if $\alpha$ has kernel size $1$ then it is purely inseparable.

noncomputable def IsogenyStandardForm.xCoordRatFun {F : Type u_1} [Field F] (α : IsogenyStandardForm F) : FractionRing (Polynomial F)

The rational function $u/v \in K(F[X])$ representing the $x$-coordinate of a standard-form isogeny in the fraction field.

noncomputable def IsogenyStandardForm.evalAtRatFun {F : Type u_1} [Field F] (p : Polynomial F) (r : FractionRing (Polynomial F)) : FractionRing (Polynomial F)

Evaluate a polynomial $p \in F[X]$ at a rational function $r \in K$ by substitution.

noncomputable def IsogenyStandardForm.compXCoord {F : Type u_1} [Field F] (β γ : IsogenyStandardForm F) : FractionRing (Polynomial F)

The composition of two $x$-coordinate rational functions $\beta \circ \gamma$ in the fraction field.

def IsogenyStandardForm.IsCompOf {F : Type u_1} [Field F] (α β γ : IsogenyStandardForm F) : Prop

$\alpha = \beta \circ \gamma$ as rational $x$-coordinate maps: the $x$-coordinate rational function of $\alpha$ equals the composition of those of $\beta$ and $\gamma$.

theorem IsogenyStandardForm.HasSeparableDegree.insepDegree_and_factorization {F : Type u_1} [Field F] {p : ℕ} (hp : Nat.Prime p) [CharP F p] {α : IsogenyStandardForm F} {d : ℕ} (hs : HasSeparableDegree hp α d) : ∃ (n : ℕ), HasInseparableDegree hp α (p ^ n) ∧ α.degree = p ^ n * d

A separable-degree witness gives an inseparable-degree witness $p^n$ and a degree factorisation $\deg \alpha = p^n \cdot d$.

theorem separableDegree_comp_mul {F : Type u_1} [Field F] {p : ℕ} [CharP F p] (hp : Nat.Prime p) (α β γ : IsogenyStandardForm F) (hcomp : α.IsCompOf β γ) (hdα : 0 < α.degree) (hdβ : 0 < β.degree) (hdγ : 0 < γ.degree) {dα dβ dγ : ℕ} (hsα : IsogenyStandardForm.HasSeparableDegree hp α dα) (hsβ : IsogenyStandardForm.HasSeparableDegree hp β dβ) (hsγ : IsogenyStandardForm.HasSeparableDegree hp γ dγ) : dα = dβ * dγ

Multiplicativity of separable degree under composition: $d_\alpha = d_\beta \cdot d_\gamma$ when $\alpha = \beta \circ \gamma$.

theorem inseparableDegree_comp_mul {F : Type u_1} [Field F] {p : ℕ} [CharP F p] (hp : Nat.Prime p) (α β γ : IsogenyStandardForm F) (hcomp : α.IsCompOf β γ) (hdα : 0 < α.degree) (hdβ : 0 < β.degree) (hdγ : 0 < γ.degree) {iα iβ iγ : ℕ} (hiα : IsogenyStandardForm.HasInseparableDegree hp α iα) (hiβ : IsogenyStandardForm.HasInseparableDegree hp β iβ) (hiγ : IsogenyStandardForm.HasInseparableDegree hp γ iγ) : iα = iβ * iγ

Multiplicativity of inseparable degree under composition: $i_\alpha = i_\beta \cdot i_\gamma$ when $\alpha = \beta \circ \gamma$.

theorem degree_comp_mul {F : Type u_1} [Field F] {p : ℕ} [CharP F p] (hp : Nat.Prime p) (α β γ : IsogenyStandardForm F) (hcomp : α.IsCompOf β γ) (hdα : 0 < α.degree) (hdβ : 0 < β.degree) (hdγ : 0 < γ.degree) {dα dβ dγ : ℕ} (hsα : IsogenyStandardForm.HasSeparableDegree hp α dα) (hsβ : IsogenyStandardForm.HasSeparableDegree hp β dβ) (hsγ : IsogenyStandardForm.HasSeparableDegree hp γ dγ) : α.degree = β.degree * γ.degree

Multiplicativity of total degree under composition: $\deg \alpha = \deg \beta \cdot \deg \gamma$ when $\alpha = \beta \circ \gamma$, obtained by combining separable and inseparable multiplicativity.

theorem corollary_5_10 {F : Type u_1} [Field F] {p : ℕ} [CharP F p] (hp : Nat.Prime p) (α β γ : IsogenyStandardForm F) (hcomp : α.IsCompOf β γ) (hdα : 0 < α.degree) (hdβ : 0 < β.degree) (hdγ : 0 < γ.degree) {dα dβ dγ iα iβ iγ : ℕ} (hsα : IsogenyStandardForm.HasSeparableDegree hp α dα) (hsβ : IsogenyStandardForm.HasSeparableDegree hp β dβ) (hsγ : IsogenyStandardForm.HasSeparableDegree hp γ dγ) (hiα : IsogenyStandardForm.HasInseparableDegree hp α iα) (hiβ : IsogenyStandardForm.HasInseparableDegree hp β iβ) (hiγ : IsogenyStandardForm.HasInseparableDegree hp γ iγ) : α.degree = β.degree * γ.degree ∧ dα = dβ * dγ ∧ iα = iβ * iγ

Corollary 5.10 (combined): for a composition $\alpha = \beta \circ \gamma$, the total, separable, and inseparable degrees are all multiplicative.

theorem quotient_curve_exists {F : Type uSWC} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) (G : AddSubgroup E.Point) [Finite ↥G] : ∃ (E' : WeierstrassCurve.Affine F) (φ : Isogeny E E'), φ.toAddMonoidHom.ker = G ∧ φ.degree = Nat.card ↥G

Quotient existence: for any finite subgroup $G \subseteq E(F)$, there exists a quotient isogeny $\phi : E \to E/G$ realising $G$ as $\ker \phi$ and with $\deg \phi = |G|$.

noncomputable def isogeny_has_representation {F : Type uSWC} [Field F] [DecidableEq F] {E E' : WeierstrassCurve.Affine F} (φ : Isogeny E E') : Isogeny.IsogenyRepresentation E E' φ

Every isogeny admits an IsogenyRepresentation (a rational standard-form representation of its action on coordinates).

theorem quotient_isogeny_rep_is_separable {F : Type uSWC} [Field F] [DecidableEq F] {E E' : WeierstrassCurve.Affine F} (φ : Isogeny E E') (G : AddSubgroup E.Point) [Finite ↥G] (hker : φ.toAddMonoidHom.ker = G) (rep : Isogeny.IsogenyRepresentation E E' φ) : rep.IsSeparable

The standard-form representation of a quotient isogeny is separable.

theorem quotient_isogeny_separable_rep {F : Type uSWC} [Field F] [DecidableEq F] {E E' : WeierstrassCurve.Affine F} (φ : Isogeny E E') (G : AddSubgroup E.Point) [Finite ↥G] (hker : φ.toAddMonoidHom.ker = G) : ∃ (rep : Isogeny.IsogenyRepresentation E E' φ), rep.IsSeparable

Packaging: a quotient isogeny admits a separable standard-form representation.

theorem Isogeny.exists_separable_of_finite_subgroup {F : Type uSWC} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) (G : AddSubgroup E.Point) [Finite ↥G] : ∃ (E' : WeierstrassCurve.Affine F) (φ : Isogeny E E') (rep : IsogenyRepresentation E E' φ), φ.toAddMonoidHom.ker = G ∧ φ.degree = Nat.card ↥G ∧ rep.IsSeparable

For every finite subgroup $G$ of $E$, there is an isogeny $\phi : E \to E'$ with kernel $G$, degree $|G|$, and admitting a separable standard-form representation.

theorem Isogeny.exists_separable_of_finite_subgroup_unique {F : Type uSWC} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) (G : AddSubgroup E.Point) [Finite ↥G] {E₁ E₂ : WeierstrassCurve.Affine F} (φ : Isogeny E E₁) (ψ : Isogeny E E₂) (hφ : φ.toAddMonoidHom.ker = G) (hψ : ψ.toAddMonoidHom.ker = G) : ∃ (ι : Isogeny E₁ E₂), ι.degree = 1 ∧ ∀ (P : E.Point), ψ.toAddMonoidHom P = ι.toAddMonoidHom (φ.toAddMonoidHom P)

Uniqueness up to isomorphism: any two quotient isogenies with the same kernel $G$ differ by a degree-$1$ isogeny.

theorem isogeny_prime_degree_factor_aux {F : Type u_1} [Field F] (d k p : ℕ) (hp : Nat.Prime p) (hdvd : p ∣ d) (hd : 1 < d) (hk_pos : 0 < k) (hk_le : k ≤ d) : ∃ (β : IsogenyStandardForm F) (γ : IsogenyStandardForm F), β.degree = p ∧ γ.degree = d / p ∧ β.kernelSize * γ.kernelSize = k

Auxiliary statement for prime-degree factorisation: any divisor $d$ of $\alpha$.degree admits a length-$2$ decomposition with degrees $p$ and $d/p$.

theorem isogeny_prime_degree_factor {F : Type u_1} [Field F] (α : IsogenyStandardForm F) (hdeg : 1 < α.degree) (p : ℕ) (hp : Nat.Prime p) (hdvd : p ∣ α.degree) : ∃ (β : IsogenyStandardForm F) (γ : IsogenyStandardForm F), 0 < β.degree ∧ 0 < γ.degree ∧ β.degree = p ∧ α.degree = β.degree * γ.degree ∧ α.kernelSize = β.kernelSize * γ.kernelSize

Prime-degree factorisation: an isogeny of degree $> 1$ factors as $\beta \circ \gamma$ with $\deg \beta = p$ for any prime $p$ dividing $\deg \alpha$.

inductive IsogenyChain {F : Type u_1} [Field F] [DecidableEq F] : WeierstrassCurve.Affine F → WeierstrassCurve.Affine F → Type u_1

A chain of isogenies between Weierstrass curves: either a single isogeny or one followed by a further chain.

• single {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (φ : Isogeny E₁ E₂) : IsogenyChain E₁ E₂
• cons {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ E₃ : WeierstrassCurve.Affine F} (φ : Isogeny E₁ E₂) (rest : IsogenyChain E₂ E₃) : IsogenyChain E₁ E₃

def IsogenyChain.compose {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} : IsogenyChain E₁ E₂ → E₁.Point →+ E₂.Point

The compose of an IsogenyChain as an additive group homomorphism on point groups.

def IsogenyChain.allPrimeDegree {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} : IsogenyChain E₁ E₂ → Prop

Predicate asserting that every link in an IsogenyChain has prime degree.

theorem isogeny_prime_factor {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (hdeg : 1 < α.degree) (p : ℕ) (hp : Nat.Prime p) (hdvd : p ∣ α.degree) : ∃ (E_mid : WeierstrassCurve.Affine F) (β : Isogeny E₁ E_mid) (γ : Isogeny E_mid E₂), β.degree = p ∧ 0 < γ.degree ∧ γ.degree * β.degree = α.degree ∧ γ.toAddMonoidHom.comp β.toAddMonoidHom = α.toAddMonoidHom

Prime-degree factorisation of a single isogeny: an isogeny of degree $> 1$ factors as $\gamma \circ \beta$ with $\deg \beta = p$ for any prime $p \mid \deg \alpha$.

theorem isogeny_prime_degree_decomposition {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (hdeg : 1 < α.degree) : ∃ (chain : IsogenyChain E₁ E₂), chain.allPrimeDegree ∧ chain.compose = α.toAddMonoidHom

Prime-degree decomposition: every isogeny of degree $> 1$ decomposes as a chain of prime-degree isogenies whose composition is the original isogeny.

noncomputable def DivisionPolynomial.psi {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : Polynomial (Polynomial R)

Public alias for the $n$-th division polynomial of a short Weierstrass curve.

noncomputable def DivisionPolynomial.phi {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : Polynomial (Polynomial R)

Public alias for the $n$-th $\phi$-polynomial of a short Weierstrass curve.

noncomputable def DivisionPolynomial.omegaNumer {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : Polynomial (Polynomial R)

Public alias for the numerator of the $n$-th $\omega$-polynomial.

@[simp]

theorem DivisionPolynomial.psi_zero {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : psi E 0 = 0

$\psi_0 = 0$.

@[simp]

theorem DivisionPolynomial.psi_one {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : psi E 1 = 1

$\psi_1 = 1$.

@[simp]

theorem DivisionPolynomial.psi_neg {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : psi E (-n) = -psi E n

$\psi_{-n} = -\psi_n$.

theorem DivisionPolynomial.phi_eq {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : phi E n = Polynomial.C Polynomial.X * psi E n ^ 2 - psi E (n + 1) * psi E (n - 1)

Defining identity: $\phi_n = X \psi_n^2 - \psi_{n+1} \psi_{n-1}$.

@[simp]

theorem DivisionPolynomial.phi_zero {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : phi E 0 = 1

$\phi_0 = 1$.

@[simp]

theorem DivisionPolynomial.phi_one {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) : phi E 1 = Polynomial.C Polynomial.X

$\phi_1 = X$.

@[simp]

theorem DivisionPolynomial.phi_neg {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : phi E (-n) = phi E n

$\phi_{-n} = \phi_n$.

theorem DivisionPolynomial.psi_odd_recurrence {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (m : ℤ) : psi E (2 * m + 1) = psi E (m + 2) * psi E m ^ 3 - psi E (m - 1) * psi E (m + 1) ^ 3

Odd recurrence: $\psi_{2m+1} = \psi_{m+2}\psi_m^3 - \psi_{m-1}\psi_{m+1}^3$.

theorem DivisionPolynomial.psi_even_recurrence {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (m : ℤ) : psi E (2 * m) * E.toWeierstrassCurve.ψ₂ = psi E (m - 1) ^ 2 * psi E m * psi E (m + 2) - psi E (m - 2) * psi E m * psi E (m + 1) ^ 2

Even recurrence: $\psi_{2m} \psi_2 = \psi_{m-1}^2 \psi_m \psi_{m+2} - \psi_{m-2} \psi_m \psi_{m+1}^2$.

theorem DivisionPolynomial.psi_odd_identity {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (m : ℤ) : phi E m * psi E (m + 1) ^ 2 - phi E (m + 1) * psi E m ^ 2 = psi E (2 * m + 1)

Odd identity (Theorem 5.21): $\phi_m \psi_{m+1}^2 - \phi_{m+1}\psi_m^2 = \psi_{2m+1}$.

theorem DivisionPolynomial.psi_even_identity {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (m : ℤ) : psi E m * omegaNumer E m = psi E (2 * m) * E.toWeierstrassCurve.ψ₂

Even identity (Theorem 5.21): $\psi_m \cdot \omega^{\mathrm{num}}_m = \psi_{2m} \cdot \psi_2$.

theorem DivisionPolynomial.x_coord_neg_symmetry {R : Type u_1} [CommRing R] (E : ShortWeierstrassCurve R) (n : ℤ) : phi E (-n) = phi E n ∧ psi E (-n) ^ 2 = psi E n ^ 2

Symmetry under negation: $\phi_{-n} = \phi_n$ and $\psi_{-n}^2 = \psi_n^2$.

noncomputable def DivisionPolynomial.evalPsi {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (n : ℤ) (x₀ y₀ : F) : F

Numerical evaluation of $\psi_n$ at the affine point $(x_0, y_0)$.

noncomputable def DivisionPolynomial.evalPhi {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (n : ℤ) (x₀ y₀ : F) : F

Numerical evaluation of $\phi_n$ at the affine point $(x_0, y_0)$.

noncomputable def DivisionPolynomial.evalOmega {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (n : ℤ) (x₀ y₀ : F) : F

Numerical evaluation of $\omega_n$ at the affine point $(x_0, y_0)$.

noncomputable def DivisionPolynomial.mulByN_x {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (n : ℤ) (x₀ y₀ : F) : F

$x$-coordinate of $[n] P$ for $P = (x_0, y_0)$, as $\phi_n(P) / \psi_n(P)^2$.

noncomputable def DivisionPolynomial.mulByN_y {F : Type u_1} [Field F] (E : ShortWeierstrassCurve F) (n : ℤ) (x₀ y₀ : F) : F

$y$-coordinate of $[n] P$ for $P = (x_0, y_0)$, as $\omega_n(P) / \psi_n(P)^3$.

theorem DivisionPolynomial.theorem_5_21 {R : Type u_2} [CommRing R] (E : ShortWeierstrassCurve R) : (∀ (n : ℤ), phi E (-n) = phi E n ∧ psi E (-n) ^ 2 = psi E n ^ 2) ∧ (∀ (m : ℤ), phi E m * psi E (m + 1) ^ 2 - phi E (m + 1) * psi E m ^ 2 = psi E (2 * m + 1)) ∧ ∀ (m : ℤ), psi E m * omegaNumer E m = psi E (2 * m) * E.toWeierstrassCurve.ψ₂

Theorem 5.21 (textbook statement): the three division polynomial identities — symmetry under negation, odd recurrence, and even recurrence — hold over any commutative ring.

theorem DivisionPolynomial.nsmul_eq_divisionPoly {F : Type u_1} [Field F] [DecidableEq F] (E : ShortWeierstrassCurve F) [E.toWeierstrassCurve.IsElliptic] {x₀ y₀ : F} (hP : E.toWeierstrassCurve.toAffine.Nonsingular x₀ y₀) {n : ℤ} (hn : n ≠ 0) : (evalPsi E n x₀ y₀ ≠ 0 → ∃ (h : E.toWeierstrassCurve.toAffine.Nonsingular (mulByN_x E n x₀ y₀) (mulByN_y E n x₀ y₀)), n • WeierstrassCurve.Affine.Point.some x₀ y₀ hP = WeierstrassCurve.Affine.Point.some (mulByN_x E n x₀ y₀) (mulByN_y E n x₀ y₀) h) ∧ (evalPsi E n x₀ y₀ = 0 → n • WeierstrassCurve.Affine.Point.some x₀ y₀ hP = WeierstrassCurve.Affine.Point.zero)

Combined point-multiplication theorem: either $\psi_n(P) \neq 0$ and $[n]P$ is given by the division polynomial formulae, or $\psi_n(P) = 0$ and $[n] P = O$.