theorem lemma_5_1_first_iff {k : Type u_1} [Field k] {u v : Polynomial k} (hcop : IsCoprime u v) : u.wronskian v = 0 ↔ Polynomial.derivative u = 0 ∧ Polynomial.derivative v = 0

Lemma 5.1, first equivalence. For coprime polynomials $u, v$ over a field $k$, the Wronskian $W(u, v) = u v' - u' v$ vanishes iff both $u$ and $v$ are constant (have zero derivative).

theorem lemma_5_1_second_iff {k : Type u_1} [Field k] (u : Polynomial k) : Polynomial.derivative u = 0 ↔ ∃ (g : Polynomial k), (Polynomial.expand k (ringChar k)) g = u

Lemma 5.1, second equivalence. Over a field $k$, a polynomial $u$ has zero derivative iff it is a $p$-th power (in the sense of being in the image of the Frobenius expand map), where $p = \mathrm{char}\, k$ (with the convention $p = 0$ giving the constant polynomials).

theorem lemma_5_1 {k : Type u_1} [Field k] {u v : Polynomial k} (hcop : IsCoprime u v) : u.wronskian v = 0 ↔ (∃ (f : Polynomial k), (Polynomial.expand k (ringChar k)) f = u) ∧ ∃ (g : Polynomial k), (Polynomial.expand k (ringChar k)) g = v

Lemma 5.1. For coprime polynomials $u, v$ over a field $k$, the Wronskian $W(u, v)$ vanishes iff both $u$ and $v$ are $p$-th powers (in the sense of expand), where $p = \mathrm{char}\, k$.

structure Velu.ShortWeierstrassCurve (k : Type u_2) : Type u_2

A short Weierstrass curve $y^2 = x^3 + A x + B$, recorded by its coefficients $A, B \in k$.

• A : k
• B : k

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

An affine point $(x, y)$ on a short Weierstrass curve $E$, together with a proof that it satisfies the curve equation $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

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

Input data for the Vélu degree-2 isogeny construction: a $k$-rational $2$-torsion point $(x_0, 0)$ on $E$, encoded by $x_0$ together with a proof that $x_0$ is a root of the cubic $x^3 + A x + B$.

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

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

Vélu's degree-2 parameter $t = 3 x_0^2 + A$ (twice the slope of the tangent at the kernel point).

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

Vélu's degree-2 parameter $w = x_0 \cdot t$.

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

New $A$-coefficient $A' = A - 5 t$ of the Vélu degree-2 image curve.

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

New $B$-coefficient $B' = B - 7 w$ of the Vélu degree-2 image curve.

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

The image curve $E' : y^2 = x^3 + A' x + B'$ produced by Vélu's degree-2 formula.

@[simp]

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

The $A$-coefficient of the Vélu degree-2 image curve unfolds to $A'$.

@[simp]

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

The $B$-coefficient of the Vélu degree-2 image curve unfolds to $B'$.

noncomputable def Velu.VeluDeg2Data.φ_x {k : Type u_1} [Field k] {E : ShortWeierstrassCurve k} (d : VeluDeg2Data E) (x : k) : k

The $x$-coordinate of the Vélu degree-2 isogeny: $\varphi_x(x) = \frac{x^2 - x_0 x + t}{x - x_0}$.

noncomputable def Velu.VeluDeg2Data.φ_y_coeff {k : Type u_1} [Field k] {E : ShortWeierstrassCurve k} (d : VeluDeg2Data E) (x : k) : k

Multiplier appearing in the $y$-coordinate of the Vélu degree-2 isogeny: $\frac{(x - x_0)^2 - t}{(x - x_0)^2}$, so that $\varphi_y(x, y) = y \cdot \frac{(x - x_0)^2 - t}{(x - x_0)^2}$.

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

The kernel point $(x_0, 0)$ satisfies the curve equation $y^2 = x^3 + A x + B$ with $y = 0$ since $x_0$ is a root of the cubic.

def Velu.VeluDeg2Data.kernelPoint {k : Type u_1} [Field k] {E : ShortWeierstrassCurve k} (d : VeluDeg2Data E) : AffinePoint E

The (generator of the) Vélu degree-2 kernel: the $2$-torsion point $(x_0, 0)$ on $E$.

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

Vélu's per-point parameter $t_Q = 3 x_Q^2 + A$ at the point $Q = (x_Q, y_Q)$.

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

Vélu's per-point parameter $u_Q = 2 y_Q^2$ at the point $Q$.

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

Vélu's per-point parameter $w_Q = u_Q + t_Q x_Q$ at the point $Q$.

@[simp]

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

Unfolding $t_Q$.

@[simp]

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

Unfolding $u_Q$.

@[simp]

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

Unfolding $w_Q$.

theorem Velu.AffinePoint.wQ_expanded {k : Type u_1} [Field k] {E : ShortWeierstrassCurve k} (Q : AffinePoint E) : 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 Velu.AffinePoint.uQ_eq_curve {k : Type u_1} [Field k] {E : ShortWeierstrassCurve k} (Q : AffinePoint E) : 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 Velu.AffinePoint.wQ_eq_curve {k : Type u_1} [Field k] {E : ShortWeierstrassCurve k} (Q : AffinePoint E) : 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 Velu.VeluOddData {k : Type u_1} [Field k] (E : ShortWeierstrassCurve k) : Type u_1

Input data for Vélu's odd-degree isogeny construction: a finite set $\{Q_1, \dots, Q_n\}$ of affine points (representatives modulo $\pm$), such that the resulting kernel has odd order $n + 1$ (i.e.\ the cardinality of pts plus one is odd).

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

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

Aggregated Vélu parameter $t = \sum_Q t_Q$ over the (odd-order) kernel.

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

Aggregated Vélu parameter $w = \sum_Q w_Q$ over the (odd-order) kernel.

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

New $A$-coefficient $A' = A - 5 t$ of the Vélu odd-degree image curve.

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

New $B$-coefficient $B' = B - 7 w$ of the Vélu odd-degree image curve.

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

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

@[simp]

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

The $A$-coefficient of the Vélu odd-degree image curve unfolds to $A'$.

@[simp]

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

The $B$-coefficient of the Vélu odd-degree image curve unfolds to $B'$.

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

The Vélu odd-degree rational function on $x$-coordinates: $r(x) = x + \sum_{Q} \left( \frac{t_Q}{x - x_Q} + \frac{u_Q}{(x - x_Q)^2} \right)$.

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

Derivative of the Vélu rational function: $r'(x) = 1 - \sum_{Q} \left( \frac{t_Q}{(x - x_Q)^2} + \frac{2 u_Q}{(x - x_Q)^3} \right)$.

theorem Velu.VeluOddData.velu_odd_image_property {k : Type u_1} [Field k] {E : ShortWeierstrassCurve k} (d : VeluOddData E) (P : AffinePoint E) : (∀ 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 image of a point under the Vélu odd-degree isogeny lies on the image curve: $(r'(x_P) y_P)^2 = r(x_P)^3 + A' r(x_P) + B'$ for any point $P$ whose $x$-coordinate differs from all kernel $x$-coordinates.

theorem Velu.VeluOddData.velu_odd_separable_kernel {k : Type u_1} [Field k] {E : ShortWeierstrassCurve k} (d : VeluOddData E) : ∃ (p : Polynomial k) (q : Polynomial k), q ≠ 0 ∧ IsCoprime p q ∧ (∀ (x : k), (∀ Q ∈ d.pts, x ≠ Q.x) → d.r x = Polynomial.eval x p / Polynomial.eval x q ^ 2) ∧ p.wronskian (q ^ 2) ≠ 0 ∧ max p.natDegree (2 * q.natDegree) = d.pts.card + 1 ∧ ∀ (x : k), Polynomial.eval x q = 0 ↔ ∃ Q ∈ d.pts, x = Q.x

Separability of Vélu's odd-degree isogeny: the rational function $r(x)$ admits a separable representation $r(x) = p(x)/q(x)^2$ for coprime polynomials $p, q$ with non-vanishing Wronskian, where $q$ has the kernel $x$-coordinates as its zero set, and $\max(\deg p, 2 \deg q) = |\mathrm{pts}| + 1$ is the degree of the isogeny.

theorem Velu.VeluOddData.velu_odd_isogeny {k : Type u_1} [Field k] {E : ShortWeierstrassCurve k} (d : VeluOddData E) : (∀ (P : AffinePoint E), (∀ 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') ∧ ∃ (p : Polynomial k) (q : Polynomial k), q ≠ 0 ∧ IsCoprime p q ∧ (∀ (x : k), (∀ Q ∈ d.pts, x ≠ Q.x) → d.r x = Polynomial.eval x p / Polynomial.eval x q ^ 2) ∧ p.wronskian (q ^ 2) ≠ 0 ∧ max p.natDegree (2 * q.natDegree) = d.pts.card + 1 ∧ ∀ (x : k), Polynomial.eval x q = 0 ↔ ∃ Q ∈ d.pts, x = Q.x

Vélu's odd-degree isogeny theorem (combined form): the rational formulae $(r, r')$ define an isogeny $E \to E'$ with the prescribed kernel, and this isogeny is separable, of degree $|\mathrm{pts}| + 1$, with kernel $x$-coordinates exactly the zeros of $q$.