Montgomery curve as a Weierstrass curve (Option B)

The Montgomery equation y² = x³ + A x² + x (with B = 1) is literally a Weierstrass equation with a₁ = 0, a₂ = A, a₃ = 0, a₄ = 1, a₆ = 0. We instantiate Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass directly and reuse its proved AddCommGroup structure on affine points.

This closes the full MontyCurveGroup specification without needing a separate Montgomery-form group-law port:

• Definition montgomeryW A : WeierstrassCurve F — trivial
• Group instance (montgomeryW A).toAffine.Point — free from Mathlib
• xProjW — projective x-coordinate map (zero ↦ (1, 0); affine (x, _) ↦ (x, 1))
• xdbl_spec_W — x-only doubling formula matches P + P's x-coord, covering the point at infinity, 2-torsion, and generic cases
• xdadd_spec_W — x-only differential addition matches P + Q's x-coord, covering P = 0, Q = 0, P = ±Q, and generic cases (xp ≠ xq)
• montgomeryW_MontyCurveGroup — packages the above into a MontyCurveGroup instance, modulo the hypotheses 2 ≠ 0 and 4 · a24 = A + 2.

The proof reduces everything to two polynomial identities over the base field (xdbl_affine_numerator_identity and xdadd_affine_identity), both of which are provable by linear_combination using only the two curve equations for P, Q.

References

• Costello, Smith, "Montgomery curves and the Montgomery ladder", IACR eprint 2017/212, §4.
• Mathlib, AlgebraicGeometry/EllipticCurve/Affine/Formula.lean.

Montgomery curve as a Weierstrass curve

def CatCrypt.Crypto.ECC.montgomeryW {F : Type u_1} [Field F] (A : F) : WeierstrassCurve F

The Montgomery equation y² = x³ + A x² + x expressed as a Weierstrass curve with (a₁, a₂, a₃, a₄, a₆) = (0, A, 0, 1, 0).

Equations

• CatCrypt.Crypto.ECC.montgomeryW A = { a₁ := 0, a₂ := A, a₃ := 0, a₄ := 1, a₆ := 0 }

@[simp]

theorem CatCrypt.Crypto.ECC.montgomeryW_a₁ {F : Type u_1} [Field F] (A : F) : (montgomeryW A).a₁ = 0

@[simp]

theorem CatCrypt.Crypto.ECC.montgomeryW_a₂ {F : Type u_1} [Field F] (A : F) : (montgomeryW A).a₂ = A

@[simp]

theorem CatCrypt.Crypto.ECC.montgomeryW_a₃ {F : Type u_1} [Field F] (A : F) : (montgomeryW A).a₃ = 0

@[simp]

theorem CatCrypt.Crypto.ECC.montgomeryW_a₄ {F : Type u_1} [Field F] (A : F) : (montgomeryW A).a₄ = 1

@[simp]

theorem CatCrypt.Crypto.ECC.montgomeryW_a₆ {F : Type u_1} [Field F] (A : F) : (montgomeryW A).a₆ = 0

theorem CatCrypt.Crypto.ECC.montgomeryW_equation {F : Type u_1} [Field F] (A x y : F) : (montgomeryW A).toAffine.Equation x y ↔ y ^ 2 = x ^ 3 + A * x ^ 2 + x

Curve equation check: y² = x³ + A x² + x iff the Weierstrass equation holds for (x, y) on montgomeryW A.

Affine-doubling x-coordinate matches xdbl ratio

def CatCrypt.Crypto.ECC.montyDoublingSlope {F : Type u_1} [Field F] (A x y : F) : F

The affine slope for doubling a Montgomery point: ℓ = (3x² + 2Ax + 1) / (2y). This is Mathlib's slope specialised to the doubling case (x₁ = x₂, y₁ = y₂) on montgomeryW A.

Equations

• CatCrypt.Crypto.ECC.montyDoublingSlope A x y = (3 * x ^ 2 + 2 * A * x + 1) / (2 * y)

def CatCrypt.Crypto.ECC.montyDoublingX {F : Type u_1} [Field F] (A x ℓ : F) : F

The x-coordinate of 2P via the affine formula, specialised to montgomeryW A. Mathlib's addX x x ℓ = ℓ² + a₁·ℓ − a₂ − 2x, which for Montgomery (a₁=0, a₂=A) reduces to ℓ² − A − 2x.

Equations

• CatCrypt.Crypto.ECC.montyDoublingX A x ℓ = ℓ ^ 2 - A - 2 * x

theorem CatCrypt.Crypto.ECC.xdbl_matches_affine_doubling {F : Type u_1} [Field F] (A a24 x y : F) (hCurve : y ^ 2 = x ^ 3 + A * x ^ 2 + x) (hy : 2 * y ≠ 0) (h24 : 4 * a24 = A + 2) : montyDoublingX A x (montyDoublingSlope A x y) * (xdbl a24 (x, 1)).2 = (xdbl a24 (x, 1)).1

Core identity — affine doubling x-coord matches xdbl's ratio.

Given a point (x, y) on Montgomery y² = x³ + A x² + x with y ≠ 0 (not a 2-torsion point), and 4 · a24 = A + 2, the affine-formula x-coordinate of 2 · (x, y) equals the projective ratio X' / Z' of xdbl a24 (x, 1), expressed as X' = montyDoublingX · Z'.

Projective x-coordinate map and MontyCurveGroup specs

def CatCrypt.Crypto.ECC.xProjW {F : Type u_1} [Field F] (A : F) : (montgomeryW A).toAffine.Point → F × F

Projective x-coordinate of a Weierstrass affine point on the Montgomery curve. The point at infinity projects to (1, 0) (representing the "point at infinity" in the projective line); a finite affine point (x, y) projects to (x, 1).

Equations

• CatCrypt.Crypto.ECC.xProjW A WeierstrassCurve.Affine.Point.zero = (1, 0)
• CatCrypt.Crypto.ECC.xProjW A (WeierstrassCurve.Affine.Point.some x_1 y h) = (x_1, 1)

@[simp]

theorem CatCrypt.Crypto.ECC.xProjW_zero {F : Type u_1} [Field F] (A : F) : xProjW A WeierstrassCurve.Affine.Point.zero = (1, 0)

@[simp]

theorem CatCrypt.Crypto.ECC.xProjW_some {F : Type u_1} [Field F] (A : F) {x y : F} (h : (montgomeryW A).toAffine.Nonsingular x y) : xProjW A (WeierstrassCurve.Affine.Point.some x y h) = (x, 1)

@[simp]

theorem CatCrypt.Crypto.ECC.xProjW_neg {F : Type u_1} [Field F] (A : F) (P : (montgomeryW A).toAffine.Point) : xProjW A (-P) = xProjW A P

xProjW is negation-invariant. The x-coordinate of -P equals that of P, since Montgomery negation only flips y.

@[simp]

theorem CatCrypt.Crypto.ECC.montgomeryW_negY {F : Type u_1} [Field F] (A x y : F) : (montgomeryW A).toAffine.negY x y = -y

The Mathlib negY for Montgomery is -y (since a₁ = a₃ = 0).

theorem CatCrypt.Crypto.ECC.montgomeryW_slope_double {F : Type u_1} [Field F] [DecidableEq F] (A x y : F) (hy : y ≠ -y) : (montgomeryW A).toAffine.slope x x y y = montyDoublingSlope A x y

The Mathlib doubling slope on Montgomery is (3x² + 2Ax + 1) / (2y).

theorem CatCrypt.Crypto.ECC.montgomeryW_addX_double {F : Type u_1} [Field F] (A x ℓ : F) : (montgomeryW A).toAffine.addX x x ℓ = montyDoublingX A x ℓ

The Mathlib addX on doubling reduces to montyDoublingX.

theorem CatCrypt.Crypto.ECC.xdbl_spec_W {F : Type u_1} [Field F] [DecidableEq F] (h2 : 2 ≠ 0) (A a24 : F) (h24 : 4 * a24 = A + 2) (P : (montgomeryW A).toAffine.Point) : (xdbl a24 (xProjW A P)).1 * (xProjW A (P + P)).2 = (xProjW A (P + P)).1 * (xdbl a24 (xProjW A P)).2

xdbl_spec on (montgomeryW A).toAffine.Point. The x-only doubling formula xdbl computes the projective x-coordinate of P + P for any point P on the Montgomery curve as a Weierstrass curve.

xdadd correspondence

theorem CatCrypt.Crypto.ECC.xdadd_affine_identity {F : Type u_1} [Field F] (A xp yp xq yq : F) (hp : yp ^ 2 = xp ^ 3 + A * xp ^ 2 + xp) (hq : yq ^ 2 = xq ^ 3 + A * xq ^ 2 + xq) : ((yq - yp) ^ 2 - (A + xp + xq) * (xq - xp) ^ 2) * ((yq + yp) ^ 2 - (A + xp + xq) * (xq - xp) ^ 2) = (xp * xq - 1) ^ 2 * (xq - xp) ^ 2

Core polynomial identity for differential addition (Costello–Smith §4).

Given two points (xp, yp) and (xq, yq) on the Montgomery curve y² = x³ + A x² + x, the product of the affine "plus" and "minus" x-numerators equals (xp · xq − 1)² · (xq − xp)². Proof is purely polynomial, using only the two curve equations.

theorem CatCrypt.Crypto.ECC.xdadd_affine_prod {F : Type u_1} [Field F] (A xp yp xq yq : F) (hp : yp ^ 2 = xp ^ 3 + A * xp ^ 2 + xp) (hq : yq ^ 2 = xq ^ 3 + A * xq ^ 2 + xq) (hxne : xq - xp ≠ 0) : ((yq - yp) ^ 2 / (xq - xp) ^ 2 - A - xp - xq) * ((yq + yp) ^ 2 / (xq - xp) ^ 2 - A - xp - xq) * (xq - xp) ^ 2 = (xp * xq - 1) ^ 2

Differential-addition x-coordinate identity. Combines the two affine secant x-coordinates (for P+Q and P-Q) into the product form (xp · xq − 1)². This is the form needed by xdadd_spec_W.

theorem CatCrypt.Crypto.ECC.montgomeryW_slope_secant {F : Type u_1} [Field F] [DecidableEq F] (A x₁ x₂ y₁ y₂ : F) (hx : x₁ ≠ x₂) : (montgomeryW A).toAffine.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)

Mathlib's secant slope specialised to Montgomery with x₁ ≠ x₂.

theorem CatCrypt.Crypto.ECC.montgomeryW_addX {F : Type u_1} [Field F] (A x₁ x₂ ℓ : F) : (montgomeryW A).toAffine.addX x₁ x₂ ℓ = ℓ ^ 2 - A - x₁ - x₂

Mathlib's affine addX specialised to Montgomery.

theorem CatCrypt.Crypto.ECC.xdadd_spec_W {F : Type u_1} [Field F] [DecidableEq F] (h2 : 2 ≠ 0) (A : F) (P Q : (montgomeryW A).toAffine.Point) : (xdadd (xProjW A P) (xProjW A Q) (xProjW A (P - Q))).1 * (xProjW A (P + Q)).2 = (xProjW A (P + Q)).1 * (xdadd (xProjW A P) (xProjW A Q) (xProjW A (P - Q))).2

xdadd_spec on (montgomeryW A).toAffine.Point. The x-only differential-addition formula xdadd computes the projective x-coordinate of P + Q, given the difference P - Q. Covers all cases including P = 0, Q = 0, P = ±Q, and generic.

MontyCurveGroup instance for WeierstrassCurve.Affine.Point

def CatCrypt.Crypto.ECC.montgomeryW_MontyCurveGroup {F : Type u_1} [Field F] [DecidableEq F] (h2 : 2 ≠ 0) (A a24 : F) (h24 : 4 * a24 = A + 2) : MontyCurveGroup F { A := A, a24 := a24 } (montgomeryW A).toAffine.Point

Main packaging. The Weierstrass-curve group on (montgomeryW A).toAffine.Point, together with the x-coordinate map xProjW A, satisfies the MontyCurveGroup specification for the Montgomery x-only formulas.

Hypotheses are h2 : (2 : F) ≠ 0 (excludes char-2 fields, where Montgomery form is degenerate) and h24 : 4 * a24 = A + 2 (definition of a24).

Equations

• CatCrypt.Crypto.ECC.montgomeryW_MontyCurveGroup h2 A a24 h24 = { xProj := CatCrypt.Crypto.ECC.xProjW A, xdbl_spec := ⋯, xdadd_spec := ⋯ }