Eisenstein

CompElliptic.lean

@@ -28,4 +28,11 @@ import CompElliptic.Hashing.TwoTermUniformity
 import CompElliptic.Hashing.WeilInstance
 import CompElliptic.Hashing.WeilSupport
 import CompElliptic.Hashing.WellDistributed
+import CompElliptic.Endomorphism
+import CompElliptic.CurveForms.Automorphisms
+import CompElliptic.Curves.PastaAut
+import CompElliptic.Rings.Eisenstein.Basic
+import CompElliptic.Rings.Eisenstein.Mod
+import CompElliptic.Rings.Eisenstein.Units
+import CompElliptic.Rings.Eisenstein.Orbits
 import CompElliptic.TrustBoundary

CompElliptic/CurveForms/Automorphisms.lean

@@ -0,0 +1,218 @@
+/-
+Copyright (c) 2026 CompElliptic Contributors.
+Released under the Apache License, Version 2.0, or the MIT license, at your option,
+as described in the files LICENSE-APACHE and LICENSE-MIT.
+Authors: Danny Willems
+-/
+import CompElliptic.Endomorphism
+import CompElliptic.Rings.Eisenstein.Units
+
+/-!
+# The six automorphisms of a `j = 0` short-Weierstrass curve
+
+For `y² = x³ + B` (that is, `A = 0`, so `j = 0`) over a field containing a
+primitive cube root of unity `z`, the maps
+
+    (x, y) ↦ (zᵏ · x, ± y),    k ∈ {0, 1, 2}
+
+are automorphisms of the group of points, and there are six of them. This module
+proves that shape and the group law it obeys.
+
+## Why the shape is what it is
+
+Each map has to preserve `y² = x³ + B`. Scaling `x` by `z` leaves `x³` alone
+exactly when `z³ = 1`, and negating `y` leaves `y²` alone always; the curve
+constrains nothing else, so the available maps are precisely a cube root on `x`
+and a sign on `y`. That is `μ₃ × μ₂`, and since `3` and `2` are coprime it is
+cyclic of order `6` — generated by `σ(x, y) = (z·x, -y)`, with `σ³` the negation
+map and `σ² = φ` the endomorphism used for GLV.
+
+## The connection to `ℤ[ω]`
+
+`μ₆` is also the unit group of the Eisenstein integers
+(`Rings.Eisenstein.isUnit_iff_mem_mu6Z`). That is not a coincidence: for a
+`j = 0` curve the endomorphism ring contains `ℤ[ω]`, `ω` acts as `φ`, and the
+units of `ℤ[ω]` act as exactly these six automorphisms. `autPt_comp` below is
+the group law that makes the correspondence a homomorphism: the `k` add mod `3`
+and the signs multiply, which is the multiplication law of `{±ωᵏ}`.
+
+## Main results
+
+* `autPt_x`, `autPt_y` — **the form**: the automorphism scales `x` by `zᵏ` and
+  applies a sign to `y`, and does nothing else.
+* `autPt_add` — each one is a homomorphism of the point group.
+* `autPt_comp`, `autPt_zero`, `autPt_three_mul` — the group law: composing
+  `(k₁, s₁)` with `(k₂, s₂)` gives `(k₁ + k₂, s₁ xor s₂)`, so the six maps form a
+  copy of `ℤ/3 × ℤ/2 ≅ μ₆`.
+* `autEquiv` — each one packaged as an additive automorphism, with the inverse
+  of `(k, s)` given by `(2k, s)`.
+-/
+
+namespace CompElliptic.CurveForms.Automorphisms
+
+open CompElliptic.CurveForms.ShortWeierstrass CompElliptic.Endomorphism
+
+variable {F : Type*} [Field F] [DecidableEq F] {z : F} {E : SWCurve F}
+
+/-- A power of a cube root of unity is a cube root of unity, so every `zᵏ` is an
+admissible `x`-scaling. -/
+theorem pow_cube (hz : z ^ 3 = 1) (k : ℕ) : (z ^ k) ^ 3 = 1 := by
+  rw [← pow_mul, mul_comm k 3, pow_mul, hz, one_pow]
+
+/-- The automorphism `(x, y) ↦ (zᵏ · x, ± y)`, with the sign selected by `s`.
+
+Built by composing the `x`-scaling `φ` with negation, both of which are already
+known to preserve the curve and the group law — so nothing new has to be proved
+about the chord-and-tangent formulas. -/
+def autPt (hA : E.A = 0) (hz : z ^ 3 = 1) (k : ℕ) (s : Bool) (P : SWPoint E) :
+    SWPoint E :=
+  phiPt hA (pow_cube hz k) (if s then -P else P)
+
+/-- **The form, on `x`.** The automorphism scales the `x`-coordinate by `zᵏ`. -/
+@[simp] theorem autPt_x (hA : E.A = 0) (hz : z ^ 3 = 1) (k : ℕ) (s : Bool)
+    (P : SWPoint E) : (autPt hA hz k s P).x = z ^ k * P.x := by
+  cases s <;> rfl
+
+/-- **The form, on `y`.** The automorphism only ever applies a sign to `y`; in
+particular it never mixes the coordinates. This is what makes the orbit of a
+point cheap to store: an orbit has three `x`-coordinates but only one `± y`
+pair. -/
+@[simp] theorem autPt_y (hA : E.A = 0) (hz : z ^ 3 = 1) (k : ℕ) (s : Bool)
+    (P : SWPoint E) : (autPt hA hz k s P).y = if s then -P.y else P.y := by
+  cases s <;> rfl
+
+/-- **Each of the six maps is an endomorphism of the point group.** -/
+theorem autPt_add (hA : E.A = 0) (hz : z ^ 3 = 1) (k : ℕ) (s : Bool)
+    (P Q : SWPoint E) :
+    autPt hA hz k s (P + Q) = autPt hA hz k s P + autPt hA hz k s Q := by
+  cases s with
+  | false => exact phiPt_add hA (pow_cube hz k) P Q
+  | true =>
+      show phiPt hA (pow_cube hz k) (-(P + Q)) = _
+      rw [neg_add]
+      exact phiPt_add hA (pow_cube hz k) (-P) (-Q)
+
+/-- The identity is the case `k = 0` with no sign flip. -/
+theorem autPt_zero (hA : E.A = 0) (hz : z ^ 3 = 1) (P : SWPoint E) :
+    autPt hA hz 0 false P = P := by
+  refine SWPoint.ext_pair ?_
+  simp
+
+/-- Three `x`-scalings undo themselves, because `z³ = 1`. -/
+theorem autPt_three_mul (hA : E.A = 0) (hz : z ^ 3 = 1) (k : ℕ) (P : SWPoint E) :
+    autPt hA hz (3 * k) false P = P := by
+  refine SWPoint.ext_pair ?_
+  have h : z ^ (3 * k) = 1 := by rw [pow_mul, hz, one_pow]
+  simp [h]
+
+/-- **The group law.** Composing `(k₁, s₁)` after `(k₂, s₂)` gives
+`(k₁ + k₂, s₁ xor s₂)`: the `x`-exponents add and the signs multiply. With
+`autPt_zero` and `autPt_three_mul` this exhibits the six maps as a copy of
+`ℤ/3 × ℤ/2 ≅ μ₆`, and it is the multiplication law of `{±ωᵏ}` in `ℤ[ω]`. -/
+theorem autPt_comp (hA : E.A = 0) (hz : z ^ 3 = 1) (k₁ k₂ : ℕ) (s₁ s₂ : Bool)
+    (P : SWPoint E) :
+    autPt hA hz k₁ s₁ (autPt hA hz k₂ s₂ P)
+      = autPt hA hz (k₁ + k₂) (xor s₁ s₂) P := by
+  refine SWPoint.ext_pair ?_
+  have hx : z ^ k₁ * (z ^ k₂ * P.x) = z ^ (k₁ + k₂) * P.x := by
+    rw [pow_add]; ring
+  cases s₁ <;> cases s₂ <;> simp [hx]
+
+/-- Each of the six maps, packaged as an additive automorphism of the point
+group. The inverse of `(k, s)` is `(2k, s)`: the exponents sum to `3k ≡ 0`, and
+a sign is its own inverse. -/
+def autEquiv (hA : E.A = 0) (hz : z ^ 3 = 1) (k : ℕ) (s : Bool) :
+    SWPoint E ≃+ SWPoint E where
+  toFun := autPt hA hz k s
+  invFun := autPt hA hz (2 * k) s
+  left_inv P := by
+    rw [autPt_comp, Bool.xor_self, show 2 * k + k = 3 * k by ring, autPt_three_mul]
+  right_inv P := by
+    rw [autPt_comp, Bool.xor_self, show k + 2 * k = 3 * k by ring, autPt_three_mul]
+  map_add' := autPt_add hA hz k s
+
+@[simp] theorem autEquiv_apply (hA : E.A = 0) (hz : z ^ 3 = 1) (k : ℕ) (s : Bool)
+    (P : SWPoint E) : autEquiv hA hz k s P = autPt hA hz k s P := rfl
+
+/-- `σ(x, y) = (z·x, -y)` generates: `σ² = φ` is the `x`-scaling used for GLV,
+and `σ³` is negation. -/
+theorem autPt_sigma_sq (hA : E.A = 0) (hz : z ^ 3 = 1) (P : SWPoint E) :
+    autPt hA hz 1 true (autPt hA hz 1 true P) = autPt hA hz 2 false P := by
+  rw [autPt_comp]; rfl
+
+theorem autPt_sigma_cube (hA : E.A = 0) (hz : z ^ 3 = 1) (P : SWPoint E) :
+    autPt hA hz 1 true (autPt hA hz 1 true (autPt hA hz 1 true P)) = -P := by
+  rw [autPt_sigma_sq, autPt_comp]
+  refine SWPoint.ext_pair ?_
+  simp [hz]
+
+/-! ## The six automorphisms are the six units of `ℤ[ω]` acting
+
+`μ₆` occurs twice over: as `Aut(E)` above, and as the unit group of the
+Eisenstein integers (`Rings.Eisenstein.isUnit_iff_mem_mu6Z`). The two are the
+same group acting, and this section makes that literal rather than a remark.
+
+A unit is `ε·ωᵏ` with `ε = ±1`; `unitIndex` reads off the pair `(k, ε)`, and
+`autOfUnit_mul` shows the resulting action is multiplicative. So the `x`-exponent
+tracks the power of `ω` and the `y`-sign tracks the sign of the unit. -/
+
+open CompElliptic.Rings CompElliptic.Rings.Eisenstein in
+/-- Read an Eisenstein unit `ε·ωᵏ` as its exponent and sign. Outside `μ₆` the
+value is meaningless; every statement below quantifies over `mu6Z`. -/
+def unitIndex (u : Eisenstein ℤ) : ℕ × Bool :=
+  if u = ⟨0, 1⟩ then (1, false)          -- ω
+  else if u = ⟨0, -1⟩ then (1, true)     -- -ω
+  else if u = ⟨-1, -1⟩ then (2, false)   -- ω²
+  else if u = ⟨1, 1⟩ then (2, true)      -- -ω²
+  else if u = ⟨-1, 0⟩ then (0, true)     -- -1
+  else (0, false)                        -- 1
+
+open CompElliptic.Rings CompElliptic.Rings.Eisenstein in
+/-- The six units give six different `(exponent, sign)` pairs. -/
+theorem unitIndex_injOn :
+    ∀ u ∈ mu6Z, ∀ v ∈ mu6Z, unitIndex u = unitIndex v → u = v := by decide
+
+open CompElliptic.Rings CompElliptic.Rings.Eisenstein in
+/-- Multiplying units adds exponents mod `3` and multiplies signs — the group law
+of `μ₆`, matching `autPt_comp`. -/
+theorem unitIndex_mul :
+    ∀ u ∈ mu6Z, ∀ v ∈ mu6Z,
+      (unitIndex (u * v)).1 % 3 = ((unitIndex u).1 + (unitIndex v).1) % 3 ∧
+      (unitIndex (u * v)).2 = xor (unitIndex u).2 (unitIndex v).2 := by decide
+
+/-- `z ^ k` depends only on `k mod 3`. -/
+theorem pow_mod_three (hz : z ^ 3 = 1) (k : ℕ) : z ^ (k % 3) = z ^ k := by
+  conv_rhs => rw [← Nat.div_add_mod k 3]
+  rw [pow_add, pow_mul, hz, one_pow, one_mul]
+
+/-- The automorphism depends only on `k mod 3`. -/
+theorem autPt_mod_three (hA : E.A = 0) (hz : z ^ 3 = 1) (k : ℕ) (s : Bool)
+    (P : SWPoint E) : autPt hA hz (k % 3) s P = autPt hA hz k s P := by
+  refine SWPoint.ext_pair ?_
+  simp [pow_mod_three hz]
+
+open CompElliptic.Rings CompElliptic.Rings.Eisenstein in
+/-- **The action of an Eisenstein unit on the curve.** `ε·ωᵏ` acts as
+`(x, y) ↦ (zᵏ · x, ε·y)`. -/
+def autOfUnit (hA : E.A = 0) (hz : z ^ 3 = 1) (u : Eisenstein ℤ) :
+    SWPoint E ≃+ SWPoint E :=
+  autEquiv hA hz (unitIndex u).1 (unitIndex u).2
+
+open CompElliptic.Rings CompElliptic.Rings.Eisenstein in
+/-- **The correspondence is a group action.** Acting by `u` then by `v` is acting
+by `u · v`, so `μ₆ → Aut(E)` is a homomorphism — and by `unitIndex_injOn` an
+injective one. The six units of `ℤ[ω]` are therefore exactly the six
+automorphisms of a `j = 0` curve, which is the fact the orbit structure of the
+recoding relies on. -/
+theorem autOfUnit_mul (hA : E.A = 0) (hz : z ^ 3 = 1) :
+    ∀ u ∈ mu6Z, ∀ v ∈ mu6Z, ∀ P : SWPoint E,
+      autOfUnit hA hz u (autOfUnit hA hz v P) = autOfUnit hA hz (u * v) P := by
+  intro u hu v hv P
+  obtain ⟨hk, hs⟩ := unitIndex_mul u hu v hv
+  have hx : autPt hA hz ((unitIndex u).1 + (unitIndex v).1)
+        (xor (unitIndex u).2 (unitIndex v).2) P
+      = autPt hA hz (unitIndex (u * v)).1 (unitIndex (u * v)).2 P := by
+    rw [hs, ← autPt_mod_three hA hz (unitIndex (u * v)).1, hk, autPt_mod_three]
+  exact (autPt_comp hA hz _ _ _ _ P).trans hx
+
+end CompElliptic.CurveForms.Automorphisms

CompElliptic/Curves/PastaAut.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2026 CompElliptic Contributors.
+Released under the Apache License, Version 2.0, or the MIT license, at your option,
+as described in the files LICENSE-APACHE and LICENSE-MIT.
+Authors: Danny Willems
+-/
+import CompElliptic.Curves.PastaOrder
+import CompElliptic.CurveForms.Automorphisms
+
+/-!
+# The six automorphisms of Pallas and Vesta
+
+Both Pasta curves are `y² = x³ + 5`, so `A = 0` and `j = 0`, and both base fields
+contain a primitive cube root of unity. `CurveForms.Automorphisms` then supplies
+six automorphisms `(x, y) ↦ (ζᵏ · x, ± y)`; this module pins the constant `ζ` for
+each curve and checks that the six are genuinely distinct, so the automorphism
+group really does contain a copy of `μ₆` rather than collapsing.
+
+Distinctness is a concrete closed fact, so it is settled by kernel `decide` at
+the test point `G = (-1, 2)`: the three `x`-coordinates `ζᵏ · (-1)` are distinct
+because `ζ` has order `3`, and the two `y`-coordinates `± 2` are distinct because
+the field has odd characteristic.
+
+`ZETA_quad` records that `ζ` satisfies `ζ² + ζ + 1 = 0` — the same relation the
+adjoined `ω` of `Rings.Eisenstein` satisfies. That is the arithmetic content of
+the statement that the six automorphisms of a `j = 0` curve are the six units of
+`ℤ[ω]` acting: the `x`-exponent is the power of `ω` and the `y`-sign is the sign
+of the unit, and `Automorphisms.autPt_comp` is the resulting multiplication law.
+-/
+
+namespace CompElliptic.Curves.Pasta
+
+open CompElliptic.CurveForms.ShortWeierstrass CompElliptic.CurveForms.Automorphisms
+
+namespace Pallas
+
+/-- A primitive cube root of unity in the Pallas base field `𝔽ₚ`. -/
+def ZETA : Fields.Pasta.PallasBaseField :=
+  0x2d33357cb532458ed3552a23a8554e5005270d29d19fc7d27b7fd22f0201b547
+
+theorem A_zero : curve.A = 0 := rfl
+
+theorem ZETA_cube : ZETA ^ 3 = 1 := by decide
+
+theorem ZETA_ne_one : ZETA ≠ 1 := by decide
+
+/-- `ζ² + ζ + 1 = 0`: the defining relation of the adjoined `ω` in
+`Rings.Eisenstein`. This is what identifies the `x`-scalings with the cube roots
+of unity in `ℤ[ω]`. -/
+theorem ZETA_quad : ZETA ^ 2 + ZETA + 1 = 0 := by decide
+
+/-- The six automorphisms of Pallas, as additive automorphisms of the point
+group: `(x, y) ↦ (ζᵏ · x, ± y)` for `k ∈ {0, 1, 2}`. -/
+def aut (k : ℕ) (s : Bool) : SWPoint curve ≃+ SWPoint curve :=
+  autEquiv A_zero ZETA_cube k s
+
+/-- The parameters of the six automorphisms. -/
+def autParams : List (ℕ × Bool) :=
+  [(0, false), (0, true), (1, false), (1, true), (2, false), (2, true)]
+
+/-- **The six are genuinely six.** Their values at `G = (-1, 2)` are pairwise
+distinct, so the six parameter pairs give six different automorphisms and the
+automorphism group contains a copy of `μ₆`. -/
+theorem aut_nodup_at_Gpt :
+    (autParams.map fun ks =>
+      ((autPt A_zero ZETA_cube ks.1 ks.2 Gpt).x,
+       (autPt A_zero ZETA_cube ks.1 ks.2 Gpt).y)).Nodup := by
+  simp only [autParams, List.map_cons, List.map_nil, autPt_x, autPt_y]
+  decide
+
+end Pallas
+
+namespace Vesta
+
+/-- A primitive cube root of unity in the Vesta base field `𝔽_q`. -/
+def ZETA : Fields.Pasta.VestaBaseField :=
+  0x06819a58283e528e511db4d81cf70f5a0fed467d47c033af2aa9d2e050aa0e4f
+
+theorem A_zero : curve.A = 0 := rfl
+
+theorem ZETA_cube : ZETA ^ 3 = 1 := by decide
+
+theorem ZETA_ne_one : ZETA ≠ 1 := by decide
+
+theorem ZETA_quad : ZETA ^ 2 + ZETA + 1 = 0 := by decide
+
+/-- The six automorphisms of Vesta. -/
+def aut (k : ℕ) (s : Bool) : SWPoint curve ≃+ SWPoint curve :=
+  autEquiv A_zero ZETA_cube k s
+
+theorem aut_nodup_at_Gpt :
+    (Pallas.autParams.map fun ks =>
+      ((autPt A_zero ZETA_cube ks.1 ks.2 Gpt).x,
+       (autPt A_zero ZETA_cube ks.1 ks.2 Gpt).y)).Nodup := by
+  simp only [Pallas.autParams, List.map_cons, List.map_nil, autPt_x, autPt_y]
+  decide
+
+end Vesta
+
+end CompElliptic.Curves.Pasta