From 1752ff6890667b39c3aeac33f58da7834bc66e81 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Fri, 28 Aug 2026 19:28:23 -0300 Subject: [PATCH 1/4] Rings/Eisenstein: the ring Z[omega] and the unit-action orbit count Mechanically checks the finite claims behind Eisenstein recoding for GLV on j = 0 curves. No elliptic curves are involved: every finite statement is a kernel `decide` over a 64-element ring, so all censused results sit at the standard-axioms tier and no `native_decide` appears in the module. `Eisenstein R` is `R[X]/(X^2 + X + 1)` as a pair of coefficients. Modelling it parametrically rather than as a quotient type is what keeps the finite statements decidable: `Eisenstein` commutes with base change, so `Eisenstein (ZMod (2^w))` IS the quotient `Z[omega]/2^w` and inherits `Fintype` and `DecidableEq` from `ZMod`. It is deliberately not `Zsqrtd (-3)`, which is the suborder of index 2 and would be wrong precisely where the 2-adic structure matters, while still typechecking. Basic.lean: the `CommRing` instance, conjugation, the norm form of discriminant -3, its multiplicativity, functoriality, and the universal property `evalHom` -- evaluation at any root of `X^2 + X + 1`, which is the bridge to the curve side, since the GLV scalar satisfies exactly that relation. Mod.lean: 2 is inert, so `Z[omega]/2` is F_4; and an element is even exactly when both coordinates are, so halving is exact and coordinate-wise. Orbits.lean: the 48 odd classes, which are the units because inertness makes `Z[omega]/8` local with maximal ideal (2); the unit action on those is free, so `48 / 6 = 8` is a theorem and not a division; and eight representatives whose orbits are disjoint and cover all 48. It also settles the count over ALL nonzero residues, where the action is not free: -1 fixes the four 2-torsion classes while the other nonidentity units fix only zero, because `u - 1` then has odd norm and is invertible. So the count is Burnside's, 12 orbits including zero, and the three nonzero 2-torsion classes form one orbit of size 3 whose representative (4, 0) has two unit factorizations. `orbit_mul_unit` discharges the resulting obligation: the bucket does not depend on which factorization is chosen. The same norm computation gives more than the published argument. Since `N(u - 1)` is 1, 3 or 4 for the five nontrivial units, `2^w` can never divide `u - 1` for `w >= 2`, so the action is free on the units at every width and w = 3 is a cost choice rather than a structural one. Co-Authored-By: Claude --- CompElliptic.lean | 3 + CompElliptic/Rings/Eisenstein/Basic.lean | 242 ++++++++++++++++++++++ CompElliptic/Rings/Eisenstein/Mod.lean | 104 ++++++++++ CompElliptic/Rings/Eisenstein/Orbits.lean | 157 ++++++++++++++ CompElliptic/TrustBoundary.lean | 17 ++ 5 files changed, 523 insertions(+) create mode 100644 CompElliptic/Rings/Eisenstein/Basic.lean create mode 100644 CompElliptic/Rings/Eisenstein/Mod.lean create mode 100644 CompElliptic/Rings/Eisenstein/Orbits.lean diff --git a/CompElliptic.lean b/CompElliptic.lean index 3922c20..26fd792 100644 --- a/CompElliptic.lean +++ b/CompElliptic.lean @@ -28,4 +28,7 @@ import CompElliptic.Hashing.TwoTermUniformity import CompElliptic.Hashing.WeilInstance import CompElliptic.Hashing.WeilSupport import CompElliptic.Hashing.WellDistributed +import CompElliptic.Rings.Eisenstein.Basic +import CompElliptic.Rings.Eisenstein.Mod +import CompElliptic.Rings.Eisenstein.Orbits import CompElliptic.TrustBoundary diff --git a/CompElliptic/Rings/Eisenstein/Basic.lean b/CompElliptic/Rings/Eisenstein/Basic.lean new file mode 100644 index 0000000..c276aa3 --- /dev/null +++ b/CompElliptic/Rings/Eisenstein/Basic.lean @@ -0,0 +1,242 @@ +/- +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 Mathlib.Algebra.Ring.Hom.Defs +import Mathlib.Tactic.Ring +import Mathlib.Tactic.LinearCombination + +/-! +# The Eisenstein integers, parametrically: `R[ω]` with `ω² = -1 - ω` + +`Eisenstein R` is `R[X] / (X² + X + 1)`, presented concretely as a pair `⟨a, b⟩` +standing for `a + b·ω`. Specialised at `R = ℤ` it is the Eisenstein integers +`ℤ[ω]`, the ring of integers of `ℚ(ζ₃)`; specialised at `R = ZMod (2^w)` it *is* +the finite quotient `ℤ[ω]/2^w`. + +**Why parametric rather than a quotient type.** `Eisenstein` is a functor +`CommRing → CommRing` that commutes with base change: +`Eisenstein (R/I) = (Eisenstein R)/(I · Eisenstein R)`. Taking the quotient on +the *coefficients* rather than on the ring means `Eisenstein (ZMod (2^w))` +inherits `DecidableEq` and `Fintype` from `ZMod`, so the finite claims in +`Rings.Eisenstein.Orbits` are settled by kernel `decide` with no axiom cost. A +`Quotient`/`Ideal.Quotient` presentation would be mathematically equivalent and +computationally useless here. + +**Not `Zsqrtd (-3)`.** `ℤ[√-3]` is the suborder of `ℤ[ω]` of index 2; the +maximal order is `ℤ[ω] = ℤ[(1+√-3)/2]`. Since everything downstream is about +halving and 2-adic structure, modelling this as `Zsqrtd (-3)` would be wrong in +exactly the place it matters, while still typechecking. + +**Naming.** "Eisenstein" already occurs in this repository as Eisenstein's +polynomial irreducibility *criterion* (`Mathlib`'s `Polynomial.IsEisensteinAt`, +used in `Hashing/WeilSupport.lean`). That is a different Eisenstein object; +there is no relationship beyond the name. + +## Main definitions + +* `Eisenstein R` — the carrier, with its `CommRing` instance. +* `Eisenstein.omega` — the adjoined primitive cube root of unity, `⟨0, 1⟩`. +* `Eisenstein.conj`, `Eisenstein.norm` — conjugation and the norm form + `N(a + b·ω) = a² - a·b + b²`. +* `Eisenstein.map` — functoriality along a ring hom of coefficients. +* `Eisenstein.evalHom` — the universal property: evaluation at any `z` with + `z² + z + 1 = 0`. This is the bridge to the curve side, where the scalar + `LAMBDA` of the GLV endomorphism satisfies exactly that relation. + +## Main results + +* `Eisenstein.omega_sq` — `ω² = -1 - ω`, the defining relation. +* `Eisenstein.mul_conj` — `x · conj x = N x`. +* `Eisenstein.norm_mul` — `N` is multiplicative, which is what makes the unit + classification and the freeness arguments go through. +-/ + +namespace CompElliptic.Rings + +/-- An element `a + b·ω` of `R[ω] = R[X]/(X² + X + 1)`. -/ +structure Eisenstein (R : Type*) where + /-- The coefficient of `1`. -/ + a : R + /-- The coefficient of `ω`. -/ + b : R +deriving DecidableEq, Repr + +namespace Eisenstein + +variable {R : Type*} {S : Type*} + +/-- Two elements agree when both coordinates do. -/ +@[ext] +theorem ext {x y : Eisenstein R} (ha : x.a = y.a) (hb : x.b = y.b) : x = y := by + cases x; cases y; simp_all + +section Basic + +variable [CommRing R] + +/-! ### The operations + +Following `Mathlib`'s `Zsqrtd`: notation instances first, their coordinate +projections as `@[simp]` lemmas, then the `CommRing` whose fields *are* those +operations, so the two agree and there is no diamond. -/ + +instance : Zero (Eisenstein R) := ⟨⟨0, 0⟩⟩ +instance : One (Eisenstein R) := ⟨⟨1, 0⟩⟩ +instance : Add (Eisenstein R) := ⟨fun x y => ⟨x.a + y.a, x.b + y.b⟩⟩ +instance : Neg (Eisenstein R) := ⟨fun x => ⟨-x.a, -x.b⟩⟩ + +/-- Multiplication, with `ω² = -1 - ω` already substituted: +`(a₁ + b₁ω)(a₂ + b₂ω) = (a₁a₂ - b₁b₂) + (a₁b₂ + a₂b₁ - b₁b₂)ω`. Written out +rather than derived, so that it reduces in the kernel — which is what makes the +finite claims in `Rings.Eisenstein.Orbits` provable by `decide`. -/ +instance : Mul (Eisenstein R) := + ⟨fun x y => ⟨x.a * y.a - x.b * y.b, x.a * y.b + y.a * x.b - x.b * y.b⟩⟩ + +omit [CommRing R] in +@[simp] theorem mk_a (u v : R) : (⟨u, v⟩ : Eisenstein R).a = u := rfl + +omit [CommRing R] in +@[simp] theorem mk_b (u v : R) : (⟨u, v⟩ : Eisenstein R).b = v := rfl +@[simp] theorem zero_a : (0 : Eisenstein R).a = 0 := rfl +@[simp] theorem zero_b : (0 : Eisenstein R).b = 0 := rfl +@[simp] theorem one_a : (1 : Eisenstein R).a = 1 := rfl +@[simp] theorem one_b : (1 : Eisenstein R).b = 0 := rfl +@[simp] theorem add_a (x y : Eisenstein R) : (x + y).a = x.a + y.a := rfl +@[simp] theorem add_b (x y : Eisenstein R) : (x + y).b = x.b + y.b := rfl +@[simp] theorem neg_a (x : Eisenstein R) : (-x).a = -x.a := rfl +@[simp] theorem neg_b (x : Eisenstein R) : (-x).b = -x.b := rfl +@[simp] theorem mul_a (x y : Eisenstein R) : (x * y).a = x.a * y.a - x.b * y.b := rfl +@[simp] theorem mul_b (x y : Eisenstein R) : + (x * y).b = x.a * y.b + y.a * x.b - x.b * y.b := rfl + +/-- `R[ω]` is a commutative ring. Every axiom reduces, after `ext`, to a +polynomial identity in `R` that `ring` closes. -/ +instance instCommRing : CommRing (Eisenstein R) := by + refine + { add := (· + ·), zero := (0 : Eisenstein R), neg := Neg.neg, mul := (· * ·), + one := (1 : Eisenstein R) + sub := fun x y => x + -y + npow := @npowRec _ ⟨(1 : Eisenstein R)⟩ ⟨(· * ·)⟩ + nsmul := @nsmulRec _ ⟨(0 : Eisenstein R)⟩ ⟨(· + ·)⟩ + zsmul := @zsmulRec _ ⟨(0 : Eisenstein R)⟩ ⟨(· + ·)⟩ ⟨Neg.neg⟩ + (@nsmulRec _ ⟨(0 : Eisenstein R)⟩ ⟨(· + ·)⟩) + add_assoc := ?_ + zero_add := ?_ + add_zero := ?_ + neg_add_cancel := ?_ + add_comm := ?_ + left_distrib := ?_ + right_distrib := ?_ + zero_mul := ?_ + mul_zero := ?_ + mul_assoc := ?_ + one_mul := ?_ + mul_one := ?_ + mul_comm := ?_ } <;> + intros <;> + ext <;> + simp <;> + ring + +@[simp] theorem sub_a (x y : Eisenstein R) : (x - y).a = x.a - y.a := by + simp [sub_eq_add_neg] +@[simp] theorem sub_b (x y : Eisenstein R) : (x - y).b = x.b - y.b := by + simp [sub_eq_add_neg] + +/-- The adjoined primitive cube root of unity. -/ +def omega : Eisenstein R := ⟨0, 1⟩ + +@[simp] theorem omega_a : (omega : Eisenstein R).a = 0 := rfl +@[simp] theorem omega_b : (omega : Eisenstein R).b = 1 := rfl + +/-- The defining relation `ω² = -1 - ω`. -/ +theorem omega_sq : (omega : Eisenstein R) ^ 2 = -1 - omega := by + ext <;> simp [pow_two] + +/-- `ω² + ω + 1 = 0`: the form in which the relation is matched against the +curve-side scalar (`LAMBDA_quad` in the GLV endomorphism work). -/ +theorem omega_quad : (omega : Eisenstein R) ^ 2 + omega + 1 = 0 := by + ext <;> simp [pow_two] + +/-- `ω³ = 1`, so `ω` really is a cube root of unity. -/ +theorem omega_cube : (omega : Eisenstein R) ^ 3 = 1 := by + ext <;> simp [pow_succ] + +/-- Conjugation, the nontrivial automorphism `ω ↦ ω²`. -/ +def conj (x : Eisenstein R) : Eisenstein R := ⟨x.a - x.b, -x.b⟩ + +@[simp] theorem conj_a (x : Eisenstein R) : (conj x).a = x.a - x.b := rfl +@[simp] theorem conj_b (x : Eisenstein R) : (conj x).b = -x.b := rfl + +/-- The norm form `N(a + b·ω) = a² - a·b + b²`: the positive-definite quadratic +form of discriminant `-3`. -/ +def norm (x : Eisenstein R) : R := x.a ^ 2 - x.a * x.b + x.b ^ 2 + +@[simp] theorem norm_mk (u v : R) : + norm (⟨u, v⟩ : Eisenstein R) = u ^ 2 - u * v + v ^ 2 := rfl + +/-- `x · conj x = N x`, so the norm is realised inside the ring. -/ +theorem mul_conj (x : Eisenstein R) : x * conj x = ⟨norm x, 0⟩ := by + ext <;> simp [norm, pow_two] <;> ring + +/-- **The norm is multiplicative.** This single fact drives the unit +classification, the inertness of `2`, and the freeness of the `μ₆` action. -/ +theorem norm_mul (x y : Eisenstein R) : norm (x * y) = norm x * norm y := by + simp only [norm, mul_a, mul_b]; ring + +@[simp] theorem norm_one : norm (1 : Eisenstein R) = 1 := by simp [norm] +@[simp] theorem norm_zero : norm (0 : Eisenstein R) = 0 := by simp [norm] +@[simp] theorem norm_omega : norm (omega : Eisenstein R) = 1 := by simp [norm] + +end Basic + +section Map + +variable [CommRing R] [CommRing S] + +/-- **Functoriality.** `Eisenstein` is a functor `CommRing → CommRing`, acting on +a coefficient hom coordinate-wise. Composed with `ZMod.castHom` this is the +reduction `ℤ[ω] → ℤ[ω]/n` used throughout `Rings.Eisenstein.Mod`. -/ +def map (f : R →+* S) : Eisenstein R →+* Eisenstein S where + toFun x := ⟨f x.a, f x.b⟩ + map_one' := by ext <;> simp + map_mul' := by intros; ext <;> simp + map_zero' := by ext <;> simp + map_add' := by intros; ext <;> simp + +@[simp] theorem map_apply_a (f : R →+* S) (x : Eisenstein R) : (map f x).a = f x.a := rfl +@[simp] theorem map_apply_b (f : R →+* S) (x : Eisenstein R) : (map f x).b = f x.b := rfl + +/-- **The universal property.** `R[ω]` is initial among `R`-algebras carrying a +root of `X² + X + 1`: given a coefficient hom `f : R →+* S` and any `z : S` with +`z² + z + 1 = 0`, evaluation `a + b·ω ↦ f a + f b · z` is a ring hom. + +This is the bridge to the curve side. The GLV endomorphism's scalar satisfies +`LAMBDA² + LAMBDA + 1 = 0` in the scalar field, so a GLV pair `(k₁, k₂)` is +literally the image of `k₁ + k₂·ω` under this map, so such a pair *is* an +Eisenstein integer rather than merely resembling one. -/ +def evalHom (f : R →+* S) (z : S) (hz : z ^ 2 + z + 1 = 0) : Eisenstein R →+* S where + toFun x := f x.a + f x.b * z + map_one' := by simp + map_mul' := by + intro x y + simp only [mul_a, mul_b, map_sub, map_add, map_mul] + linear_combination (-(f x.b * f y.b)) * hz + map_zero' := by simp + map_add' := by intros; simp; ring + +@[simp] theorem evalHom_apply (f : R →+* S) (z : S) (hz : z ^ 2 + z + 1 = 0) + (x : Eisenstein R) : evalHom f z hz x = f x.a + f x.b * z := rfl + +/-- Evaluation sends `ω` to the chosen root. -/ +@[simp] theorem evalHom_omega (f : R →+* S) (z : S) (hz : z ^ 2 + z + 1 = 0) : + evalHom f z hz omega = z := by simp + +end Map + +end Eisenstein + +end CompElliptic.Rings diff --git a/CompElliptic/Rings/Eisenstein/Mod.lean b/CompElliptic/Rings/Eisenstein/Mod.lean new file mode 100644 index 0000000..d50313a --- /dev/null +++ b/CompElliptic/Rings/Eisenstein/Mod.lean @@ -0,0 +1,104 @@ +/- +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.Rings.Eisenstein.Basic +import Mathlib.Data.ZMod.Basic + +/-! +# The finite quotients `ℤ[ω]/n`, computably + +`Eisenstein (ZMod n)` **is** `ℤ[ω]/n`, because `Eisenstein` commutes with base +change (`Basic.lean`). Reducing the coefficients rather than quotienting the ring +means `Fintype` and `DecidableEq` are inherited from `ZMod n`, so the finite +claims in `Rings.Eisenstein.Orbits` are settled by kernel `decide`. + +## Main results + +* `Eisenstein.card_eq` — `#(ℤ[ω]/n) = n²`. +* `Eisenstein.two_dvd_iff` — an element is even exactly when both + coordinates are, so halving is exact and coordinate-wise. +* `Eisenstein.mod_two_eq_zero_or_isUnit`, `Eisenstein.mul_eq_zero_mod_two` — + `ℤ[ω]/2` is the field `𝔽₄`, i.e. `2` is inert. This is what makes + "odd" and "unit" the same predicate mod `2^w`, and it is why `ℤ[ω]/2^w` is a + local ring with maximal ideal `(2)`. +-/ + +namespace CompElliptic.Rings.Eisenstein + +variable {R : Type*} + +/-- `R[ω]` is just a pair of coefficients. -/ +def equivProd (R : Type*) : Eisenstein R ≃ R × R where + toFun x := (x.a, x.b) + invFun p := ⟨p.1, p.2⟩ + left_inv := by intro x; cases x; rfl + right_inv := by intro p; cases p; rfl + +/-- `R[ω]` is computably finite whenever `R` is: it is a pair of coefficients, so +the enumeration is the product enumeration — no choice, and it reduces in the +kernel. Named so the trust census can pin its computability. -/ +instance instFintype [Fintype R] : Fintype (Eisenstein R) := + Fintype.ofEquiv _ (equivProd R).symm + +/-- `#R[ω] = (#R)²`. For `R = ZMod (2^w)` this is the `4^w` the odd-class count is taken from. -/ +theorem card_eq [Fintype R] : + Fintype.card (Eisenstein R) = Fintype.card R * Fintype.card R := by + rw [Fintype.card_congr (equivProd R), Fintype.card_prod] + +section Two + +variable [CommRing R] + +/-- The numeral `2` is the coefficient pair `⟨2, 0⟩`; `ω` plays no part in it. -/ +theorem two_eq : (2 : Eisenstein R) = ⟨2, 0⟩ := by + have h : (2 : Eisenstein R) = 1 + 1 := by norm_num + rw [h] + ext + · show (1 : R) + 1 = 2; norm_num + · show (0 : R) + 0 = 0; simp + +@[simp] theorem two_a : (2 : Eisenstein R).a = 2 := by rw [two_eq] +@[simp] theorem two_b : (2 : Eisenstein R).b = 0 := by rw [two_eq] + +/-- `2 ∣ a + b·ω` exactly when `2 ∣ a` and `2 ∣ b`. The forward +direction is immediate because `2` is a rational integer, so multiplication by it +is coordinate-wise: `2 · ⟨c, d⟩ = ⟨2c, 2d⟩`. Halving is therefore exact and needs +no reasoning about `ω` — which is what lets the Eisenstein recoder halve in the +ring exactly as the coordinate-wise recoder halves each component. -/ +theorem two_dvd_iff (x : Eisenstein R) : + (2 : Eisenstein R) ∣ x ↔ (2 : R) ∣ x.a ∧ (2 : R) ∣ x.b := by + constructor + · rintro ⟨y, rfl⟩ + exact ⟨⟨y.a, by simp⟩, ⟨y.b, by simp⟩⟩ + · rintro ⟨⟨c, hc⟩, ⟨d, hd⟩⟩ + exact ⟨⟨c, d⟩, by ext <;> simp [hc, hd]⟩ + +end Two + +/-! ## `2` is inert, so `ℤ[ω]/2 = 𝔽₄` + +`X² + X + 1` has no root in `𝔽₂` (both `0` and `1` evaluate to `1`), so it is +irreducible there and `2` stays prime in `ℤ[ω]`. Stated below in the two +computational forms the rest of the development uses: the quotient has four +elements, and it has no zero divisors. Both are `decide` over at most `16` pairs, +so they add no axiom. -/ + +/-- **Cardinality.** `ℤ[ω]/2` has four elements — it is `𝔽₄`, not +`𝔽₂ × 𝔽₂`, which is the content of `2` being inert rather than split. -/ +theorem card_mod_two : Fintype.card (Eisenstein (ZMod 2)) = 4 := by decide + +/-- **No zero divisors.** `ℤ[ω]/2` is a domain, hence (being finite) a +field. Equivalently `2` is a prime element of `ℤ[ω]`. -/ +theorem mul_eq_zero_mod_two (x y : Eisenstein (ZMod 2)) : + x * y = 0 → x = 0 ∨ y = 0 := by revert x y; decide + +/-- **Every nonzero class is invertible.** The residue field is `𝔽₄`, +so a class is a unit exactly when it is nonzero. This is the fact that lets +"odd" (not divisible by `2`) and "unit" be used interchangeably mod `2^w`. -/ +theorem exists_inv_mod_two (x : Eisenstein (ZMod 2)) (hx : x ≠ 0) : + ∃ y, x * y = 1 := by revert x; decide + +end CompElliptic.Rings.Eisenstein diff --git a/CompElliptic/Rings/Eisenstein/Orbits.lean b/CompElliptic/Rings/Eisenstein/Orbits.lean new file mode 100644 index 0000000..85b2509 --- /dev/null +++ b/CompElliptic/Rings/Eisenstein/Orbits.lean @@ -0,0 +1,157 @@ +/- +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.Rings.Eisenstein.Mod + +/-! +# The unit action on `ℤ[ω]/8`, and the orbit count + +The finite core of the Eisenstein-recoding argument. Everything here is a kernel +`decide` over a 64-element ring, so nothing below leaves the standard axioms. + +## Two different orbit counts + +Tabulating the odd classes and bucketing every nonzero residue are *different* +problems, and only the first involves a free action. Both are settled here. + +* **On the ODD classes** — those not divisible by `2`, which are exactly the + units, since `2` is inert. There the `μ₆` action is FREE, so the `48` odd + classes fall into exactly `48 / 6 = 8` orbits and eight representatives + suffice. +* **On ALL nonzero residues** the action is *not* free. `-1` fixes the four + `2`-torsion classes, so the count is a Burnside count: `(B² + 8) / 6` orbits + including zero, hence `(B² + 2) / 6 = 11` buckets at `B = 8`. The three + nonzero `2`-torsion classes form a single orbit of size `3` whose + representative `(B/2, 0)` admits TWO unit factorizations, so a bucket + assignment has to agree on either choice or the result would be wrong; + `orbit_mul_unit` is that obligation. + +The structural reason the exception is exactly `-1`: a unit `u` fixes `x` iff +`(u - 1)·x = 0`, and for `u ∈ {±ω, ±ω²}` the element `u - 1` has ODD norm +(`N(ω - 1) = N(ω² - 1) = 3`, `N(-ω - 1) = N(-ω² - 1) = 1`) hence is invertible +mod `2^w`, forcing `x = 0`. Only `u = -1` has `N(u - 1) = N(-2) = 4`, even — and +its fixed set is the `2`-torsion. + +That same norm computation shows `μ₆ → (ℤ[ω]/2^w)ˣ` is injective for every +`w ≥ 2`, since `8 ∣ (u - 1)` would force `64 ∣ N(u - 1) ∈ {1, 3, 4}`. So the +freeness is not special to `w = 3`, which is a cost choice rather than a +structural one. +-/ + +namespace CompElliptic.Rings.Eisenstein + +/-- `ℤ[ω]/8`, the ring the width-3 recoding works in. -/ +abbrev Eis8 : Type := Eisenstein (ZMod 8) + +/-- The six units `{±1, ±ω, ±ω²}` of `ℤ[ω]`, reduced mod `8`. These are exactly +the six automorphisms available on a `j = 0` curve. -/ +def mu6 : Finset Eis8 := {⟨1, 0⟩, ⟨-1, 0⟩, ⟨0, 1⟩, ⟨0, -1⟩, ⟨-1, -1⟩, ⟨1, 1⟩} + +/-- The six units stay distinct mod `8`: `μ₆ → (ℤ[ω]/8)ˣ` is injective. This is +the reduction-injectivity that makes the action free on the units. -/ +theorem mu6_card : mu6.card = 6 := by decide + +/-- A class is ODD when it is not divisible by `2`. Since `2` is inert and the +residue field is `𝔽₄`, these are exactly the units of `ℤ[ω]/8`. -/ +def IsOdd (x : Eis8) : Prop := ¬ (2 ∣ x.a.val ∧ 2 ∣ x.b.val) + +instance : DecidablePred IsOdd := fun _ => by unfold IsOdd; infer_instance + +/-- The orbit of `x` under the unit action — the "bucket" the recoder assigns. -/ +def orbit (x : Eis8) : Finset Eis8 := mu6.image (· * x) + +/-! ## There are 48 odd classes -/ + +/-- `#(ℤ[ω]/8)ˣ = 48`. Conceptually this is `64 - 16`: `2` is +inert, so `ℤ[ω]/8` is a LOCAL ring whose maximal ideal is `(2)`, and the units +are precisely the complement of that ideal. -/ +theorem card_odd : (Finset.univ.filter IsOdd).card = 48 := by decide + +/-- The even classes are the other `16`, i.e. `2 · ℤ[ω]/8`. -/ +theorem card_even : (Finset.univ.filter (fun x => ¬ IsOdd x)).card = 16 := by decide + +/-! ## The action is free on the odd classes -/ + +set_option maxRecDepth 8000 in +/-- On the odd classes the `μ₆` action is FREE: no nonidentity unit fixes an odd +class. This is what licenses the division `48 / 6 = 8`. Without it a table built +from eight representatives would be incomplete, which is a soundness failure +rather than a performance one. -/ +theorem mu6_free_on_odd : + ∀ u ∈ mu6, ∀ x : Eis8, IsOdd x → u * x = x → u = ⟨1, 0⟩ := by decide + +set_option maxRecDepth 8000 in +/-- Every odd class therefore has a full orbit of six. -/ +theorem card_orbit_of_odd : ∀ x : Eis8, IsOdd x → (orbit x).card = 6 := by decide + +/-! ## Eight representatives cover all 48 -/ + +/-- Eight odd classes, one per orbit: the lexicographically least element of each +orbit. Any eight pairwise non-associate odd classes would do — see +`reps_cover` — so this is *a* valid table, and the article's specific table can +be checked against it by a single `decide` once its digits are read off the +published page. -/ +def reps : Finset Eis8 := + {⟨0, 1⟩, ⟨0, 3⟩, ⟨1, 2⟩, ⟨1, 3⟩, ⟨1, 4⟩, ⟨1, 5⟩, ⟨1, 6⟩, ⟨2, 5⟩} + +theorem reps_card : reps.card = 8 := by decide + +theorem reps_odd : ∀ r ∈ reps, IsOdd r := by decide + +/-- The eight orbits are pairwise disjoint: the representatives are pairwise +non-associate. -/ +theorem reps_pairwise_disjoint : + ∀ r ∈ reps, ∀ s ∈ reps, r ≠ s → Disjoint (orbit r) (orbit s) := by decide + +/-- The eight representatives' orbits cover every odd class exactly. With +`reps_pairwise_disjoint` and `card_orbit_of_odd` this makes `48 / 6 = 8` a +theorem rather than a division. -/ +theorem reps_cover : reps.biUnion orbit = Finset.univ.filter IsOdd := by decide + +/-- There are exactly eight orbits of odd classes. -/ +theorem card_orbits_odd : + ((Finset.univ.filter IsOdd).image orbit).card = 8 := by decide + +/-! ## The Burnside count over all nonzero residues -/ + +/-- The fixed set of `-1` is the `2`-torsion: four classes, not just zero. This +is the single exception that breaks freeness on the non-unit classes. -/ +theorem fix_neg_one : + Finset.univ.filter (fun x : Eis8 => (⟨-1, 0⟩ : Eis8) * x = x) + = {⟨0, 0⟩, ⟨0, 4⟩, ⟨4, 0⟩, ⟨4, 4⟩} := by decide + +/-- Each of the four remaining nonidentity units fixes only zero, because `u - 1` +has odd norm and is therefore invertible mod `8`. -/ +theorem fix_others : + ∀ u ∈ ({⟨0, 1⟩, ⟨0, -1⟩, ⟨-1, -1⟩, ⟨1, 1⟩} : Finset Eis8), + Finset.univ.filter (fun x : Eis8 => u * x = x) = {⟨0, 0⟩} := by decide + +/-- Burnside: `(B² + 8) / 6 = 12` orbits including zero, so `(B² + 2) / 6 = 11` +nonzero buckets. Of those, `8` are the free unit orbits above and `3` are not. -/ +theorem card_orbits_all : (Finset.univ.image orbit).card = 12 := by decide + +theorem card_orbits_nonzero : + ((Finset.univ.filter (fun x : Eis8 => x ≠ 0)).image orbit).card = 11 := by decide + +/-- The three nonzero `2`-torsion classes form ONE orbit, of size `3` rather than +`6` — the visible symptom of the stabilizer being nontrivial. -/ +theorem orbit_two_torsion : orbit ⟨4, 0⟩ = {⟨0, 4⟩, ⟨4, 0⟩, ⟨4, 4⟩} := by decide + +/-- **The two unit factorizations.** `(B/2, 0) = (4, 0)` is fixed by both `1` and +`-1`, so it has two distinct representations as `unit × representative`. -/ +theorem stabilizer_two_torsion : + mu6.filter (fun u => u * (⟨4, 0⟩ : Eis8) = ⟨4, 0⟩) = {⟨1, 0⟩, ⟨-1, 0⟩} := by decide + +set_option maxRecDepth 100000 in +set_option maxHeartbeats 2000000 in +/-- **The correctness obligation.** The bucket is well defined: it +does not depend on which unit factorization is chosen, because multiplying by any +unit leaves the orbit unchanged. This is what makes the ambiguity at `(4, 0)` +harmless; had the two factorizations landed in different buckets, the recoding +would produce a wrong result. -/ +theorem orbit_mul_unit : ∀ u ∈ mu6, ∀ x : Eis8, orbit (u * x) = orbit x := by decide + +end CompElliptic.Rings.Eisenstein diff --git a/CompElliptic/TrustBoundary.lean b/CompElliptic/TrustBoundary.lean index 9810f6b..180cc41 100644 --- a/CompElliptic/TrustBoundary.lean +++ b/CompElliptic/TrustBoundary.lean @@ -12,6 +12,7 @@ import CompElliptic.Curves.Pasta.Fast.Projective import CompElliptic.Curves.Pasta.Fast.Msm import CompElliptic.Curves.Pasta.Fast.ProjectiveMontEquiv import CompElliptic.Fields.Sqrt +import CompElliptic.Rings.Eisenstein.Orbits import CompElliptic.Meta.AxiomCheck /-! @@ -53,6 +54,22 @@ assert_axioms CompElliptic.CurveOrder.card_eq_of_prime_witness_of_card_lt_three_ assert_axioms CompElliptic.Fields.TonelliShanks.sqrt?_mul_self assert_axioms CompElliptic.Fields.TonelliShanks.sqrt?_isSome_of_isSquare +/-! ## The Eisenstein ring `ℤ[ω]` and its unit action — standard axioms only + +The finite claims (`card_odd`, the freeness and Burnside counts, the covering) +are quantified statements, but over a 64-element ring, so they are discharged by +KERNEL `decide` and add no axiom. That is deliberate: a quantified result must +not reach for `native_decide`, and here it does not have to. -/ + +assert_axioms CompElliptic.Rings.Eisenstein.norm_mul +assert_axioms CompElliptic.Rings.Eisenstein.two_dvd_iff +assert_axioms CompElliptic.Rings.Eisenstein.mul_eq_zero_mod_two +assert_axioms CompElliptic.Rings.Eisenstein.card_odd +assert_axioms CompElliptic.Rings.Eisenstein.mu6_free_on_odd +assert_axioms CompElliptic.Rings.Eisenstein.reps_cover +assert_axioms CompElliptic.Rings.Eisenstein.card_orbits_all +assert_axioms CompElliptic.Rings.Eisenstein.orbit_mul_unit + /-! ## Concrete closed facts checked by the kernel (Pratt certificates) — standard axioms only -/ assert_axioms CompElliptic.Fields.Pasta.PALLAS_BASE_is_prime From 24e038e0d4a0f7eceb535430caafd1670455c69f Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Fri, 28 Aug 2026 19:28:23 -0300 Subject: [PATCH 2/4] Rings/Eisenstein: the unit group over Z, and 2 as a prime Completes the ring layer with the arithmetic proved over Z rather than checked mod 8. Everything follows from one identity, `4*N = (2a - b)^2 + 3*b^2`, which makes the norm positive definite and bounds the solutions of `N = 1` to a box small enough to enumerate. `isUnit_iff_norm_eq_one` and `isUnit_iff_mem_mu6Z`: the unit group of Z[omega] is exactly mu_6 = {+-1, +-omega, +-omega^2}, six elements. Those are the six automorphisms of a j = 0 curve, which is why the orbit structure in Orbits.lean is the curve's own symmetry group acting. `prime_two` states inertness abstractly rather than as a 16-case check: 2 is a prime element of Z[omega]. The concrete input stays the decidable `mul_eq_zero_mod_two`, transported along the reduction to F_4. `not_two_pow_dvd_unit_sub_one` proves what the Orbits docstrings so far only asserted. For a nontrivial unit u, `N(u - 1)` is 1, 3 or 4, while `2^w | u - 1` would force `4^w | N(u - 1)` and so `4^w <= 4`. Hence the reduction mu_6 -> (Z[omega]/2^w)^x is injective, and the unit action free on the odd classes, for EVERY width w >= 2. The bound is tight: at w = 1 the argument fails at `4 <= 4`, and indeed -1 is congruent to 1 mod 2, so the six units collapse to three. Five further results join the census, all at the standard-axioms tier. Co-Authored-By: Claude --- CompElliptic.lean | 1 + CompElliptic/Rings/Eisenstein/Units.lean | 205 +++++++++++++++++++++++ CompElliptic/TrustBoundary.lean | 5 + 3 files changed, 211 insertions(+) create mode 100644 CompElliptic/Rings/Eisenstein/Units.lean diff --git a/CompElliptic.lean b/CompElliptic.lean index 26fd792..3307228 100644 --- a/CompElliptic.lean +++ b/CompElliptic.lean @@ -30,5 +30,6 @@ import CompElliptic.Hashing.WeilSupport import CompElliptic.Hashing.WellDistributed import CompElliptic.Rings.Eisenstein.Basic import CompElliptic.Rings.Eisenstein.Mod +import CompElliptic.Rings.Eisenstein.Units import CompElliptic.Rings.Eisenstein.Orbits import CompElliptic.TrustBoundary diff --git a/CompElliptic/Rings/Eisenstein/Units.lean b/CompElliptic/Rings/Eisenstein/Units.lean new file mode 100644 index 0000000..1ef2b75 --- /dev/null +++ b/CompElliptic/Rings/Eisenstein/Units.lean @@ -0,0 +1,205 @@ +/- +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.Rings.Eisenstein.Mod +import Mathlib.Tactic.IntervalCases +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity + +/-! +# The units of `ℤ[ω]`, and `2` as a prime + +The arithmetic of `ℤ[ω]` that the finite claims in `Rings.Eisenstein.Orbits` +rest on, proved over `ℤ` rather than checked mod `8`. + +Everything here follows from one fact: the norm `N(a + b·ω) = a² - a·b + b²` is +multiplicative (`norm_mul`), and over `ℤ` it is positive definite, because +`4·N = (2a - b)² + 3b²`. That identity is the whole file — it bounds the +solutions of `N = 1` to a box small enough to enumerate, which is what makes the +unit group finite and equal to `μ₆`. + +## Main results + +* `Eisenstein.isUnit_iff_norm_eq_one` — `x` is a unit iff `N x = 1`. +* `Eisenstein.norm_eq_one_iff`, `Eisenstein.isUnit_iff_mem_mu6Z` — the unit group + is exactly `μ₆ = {±1, ±ω, ±ω²}`, six elements. These are the six automorphisms + of a `j = 0` curve, which is why the orbit structure of + `Rings.Eisenstein.Orbits` is the curve's own symmetry group acting. +* `Eisenstein.prime_two` — abstractly, `2` is a prime + element of `ℤ[ω]` (it is *inert*, not split). The concrete input is the + `16`-case check `mul_eq_zero_mod_two` in `Mod.lean`; here it is transported + along the reduction `ℤ[ω] → ℤ[ω]/2 = 𝔽₄`. +* `Eisenstein.not_two_pow_dvd_unit_sub_one` — **the reason the freeness is not + special to `w = 3`.** For a nontrivial unit `u`, `N(u - 1) ∈ {1, 3, 4}`, whereas + `2^w ∣ u - 1` would force `4^w ∣ N(u - 1)`. Since `4^w ≥ 16` for `w ≥ 2`, the + reduction `μ₆ → (ℤ[ω]/2^w)ˣ` is injective at every width `w ≥ 2`, so the unit + action is free on the odd classes for every width. The article's `w = 3` is a + cost choice, not a structural one. (At `w = 1` it genuinely fails: `-1 ≡ 1` + mod `2`, and the six units collapse to three.) +-/ + +namespace CompElliptic.Rings.Eisenstein + +/-! ## The norm as a monoid hom, and divisibility -/ + +section Hom + +variable {R : Type*} [CommRing R] + +/-- The norm packaged as a monoid hom `(R[ω], ×) → (R, ×)`, so that `map_pow` +and friends apply. -/ +def normHom : Eisenstein R →* R where + toFun := norm + map_one' := norm_one + map_mul' := norm_mul + +@[simp] theorem normHom_apply (x : Eisenstein R) : normHom x = norm x := rfl + +/-- `N(xⁿ) = (N x)ⁿ`. -/ +theorem norm_pow (x : Eisenstein R) (n : ℕ) : norm (x ^ n) = norm x ^ n := + map_pow normHom x n + +/-- The norm carries divisibility from `R[ω]` down to `R`. This is the step that +turns "`2^w` divides `u - 1`" into an arithmetic impossibility. -/ +theorem norm_dvd_norm {x y : Eisenstein R} (h : x ∣ y) : norm x ∣ norm y := by + obtain ⟨c, rfl⟩ := h + exact ⟨norm c, norm_mul x c⟩ + +/-- `4·N(a + b·ω) = (2a - b)² + 3b²`: completing the square. Over `ℤ` this makes +the norm positive definite, and it is the bound that makes `N = 1` finite. -/ +theorem four_mul_norm (x : Eisenstein R) : + 4 * norm x = (2 * x.a - x.b) ^ 2 + 3 * x.b ^ 2 := by + simp only [norm]; ring + +end Hom + +/-! ## Over `ℤ`: positive definiteness and the unit group -/ + +/-- The norm is nonnegative on `ℤ[ω]`: it is the quadratic form of discriminant +`-3`, which is definite. -/ +theorem norm_nonneg (x : Eisenstein ℤ) : 0 ≤ norm x := by + have h := four_mul_norm x + nlinarith [sq_nonneg (2 * x.a - x.b), sq_nonneg x.b] + +/-- `N 2 = 4`, so `2` is not a unit. -/ +theorem norm_two : norm (2 : Eisenstein ℤ) = 4 := by + rw [two_eq]; norm_num [norm] + +/-- **`x` is a unit exactly when its norm is `1`.** Forward: `N` is +multiplicative, so `N x` is a unit of `ℤ`, hence `±1`, hence `1` by +positive definiteness. Backward: `x · conj x = N x = 1` exhibits the inverse. -/ +theorem isUnit_iff_norm_eq_one (x : Eisenstein ℤ) : IsUnit x ↔ norm x = 1 := by + constructor + · rintro ⟨u, rfl⟩ + have h : norm (u : Eisenstein ℤ) * norm (↑u⁻¹ : Eisenstein ℤ) = 1 := by + rw [← norm_mul]; simp + have hu : IsUnit (norm (u : Eisenstein ℤ)) := by + rw [isUnit_iff_exists_and_exists] + exact ⟨⟨_, h⟩, ⟨_, by rw [mul_comm]; exact h⟩⟩ + rcases Int.isUnit_iff.mp hu with h1 | h1 + · exact h1 + · have := norm_nonneg (u : Eisenstein ℤ); omega + · intro h + have hx : x * conj x = 1 := by rw [mul_conj, h]; rfl + rw [isUnit_iff_exists_and_exists] + exact ⟨⟨conj x, hx⟩, ⟨conj x, by rw [mul_comm]; exact hx⟩⟩ + +/-- **The unit group is `μ₆`.** `N = 1` forces `(2a - b)² + 3b² = 4`, so +`|b| ≤ 1` and `|a| ≤ 1`, and the box has exactly six solutions. -/ +theorem norm_eq_one_iff (x : Eisenstein ℤ) : + norm x = 1 ↔ x = ⟨1, 0⟩ ∨ x = ⟨-1, 0⟩ ∨ x = ⟨0, 1⟩ ∨ x = ⟨0, -1⟩ ∨ + x = ⟨1, 1⟩ ∨ x = ⟨-1, -1⟩ := by + obtain ⟨a, b⟩ := x + simp only [norm_mk, Eisenstein.mk.injEq] + constructor + · intro h + have hb : -1 ≤ b ∧ b ≤ 1 := by + constructor <;> nlinarith [sq_nonneg (2 * a - b)] + have ha : -1 ≤ a ∧ a ≤ 1 := by + constructor <;> nlinarith [sq_nonneg b, sq_nonneg (2 * a - b)] + obtain ⟨hb1, hb2⟩ := hb + obtain ⟨ha1, ha2⟩ := ha + interval_cases a <;> interval_cases b <;> revert h <;> decide + · rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | + ⟨rfl, rfl⟩) <;> norm_num + +/-- The six units of `ℤ[ω]`: `{1, -1, ω, -ω, -ω², ω²}`. These are exactly the +six automorphisms `(x, y) ↦ (ζ₃ᵏ·x, ±y)` of a `j = 0` curve, which is why the +recoding's orbit structure is the curve's own symmetry. -/ +def mu6Z : Finset (Eisenstein ℤ) := + {⟨1, 0⟩, ⟨-1, 0⟩, ⟨0, 1⟩, ⟨0, -1⟩, ⟨1, 1⟩, ⟨-1, -1⟩} + +theorem mu6Z_card : mu6Z.card = 6 := by decide + +/-- The unit group of `ℤ[ω]` is `μ₆`, and it has order `6`. -/ +theorem isUnit_iff_mem_mu6Z (x : Eisenstein ℤ) : IsUnit x ↔ x ∈ mu6Z := by + rw [isUnit_iff_norm_eq_one, norm_eq_one_iff] + simp [mu6Z] + +/-! ## `2` is prime in `ℤ[ω]` -/ + +/-- Reduction `ℤ[ω] → ℤ[ω]/2 = 𝔽₄`, coefficient-wise. -/ +def redTwo : Eisenstein ℤ →+* Eisenstein (ZMod 2) := + Eisenstein.map (Int.castRingHom (ZMod 2)) + +/-- Being even is being zero in the residue field. -/ +theorem two_dvd_iff_redTwo_eq_zero (x : Eisenstein ℤ) : + (2 : Eisenstein ℤ) ∣ x ↔ redTwo x = 0 := by + rw [two_dvd_iff] + constructor + · rintro ⟨ha, hb⟩ + ext <;> simp [redTwo, map, (ZMod.intCast_zmod_eq_zero_iff_dvd _ 2).mpr, ha, hb] + · intro h + have ha : ((x.a : ZMod 2)) = 0 := congrArg Eisenstein.a h + have hb : ((x.b : ZMod 2)) = 0 := congrArg Eisenstein.b h + exact ⟨(ZMod.intCast_zmod_eq_zero_iff_dvd _ 2).mp ha, + (ZMod.intCast_zmod_eq_zero_iff_dvd _ 2).mp hb⟩ + +/-- `2` is a prime element of `ℤ[ω]`: it is INERT, so +`ℤ[ω]/2` is the field `𝔽₄` rather than a product. This is what makes "even" and +"odd" mean the same in `ℤ[ω]` as coordinate-wise, makes halving exact, and makes +`ℤ[ω]/2^w` a local ring whose units are exactly the odd classes — the fact +behind `card_odd = 48`. -/ +theorem prime_two : Prime (2 : Eisenstein ℤ) := by + refine ⟨?_, ?_, ?_⟩ + · intro h + rw [show (0 : Eisenstein ℤ) = ⟨0, 0⟩ from rfl, two_eq] at h + simp at h + · rw [isUnit_iff_norm_eq_one, norm_two] + norm_num + · intro x y hxy + rw [two_dvd_iff_redTwo_eq_zero] at hxy ⊢ + rw [two_dvd_iff_redTwo_eq_zero] + rw [map_mul] at hxy + exact mul_eq_zero_mod_two _ _ hxy + +/-! ## Why the freeness holds at every width `w ≥ 2` -/ + +/-- For each of the five nontrivial units, `N(u - 1)` is `1`, `3` or `4` — in +particular nonzero and at most `4`. The three values are `N(-2) = 4`, +`N(ω - 1) = N(ω² - 1) = 3` and `N(-ω - 1) = N(-ω² - 1) = 1`. -/ +theorem norm_sub_one_of_mem_mu6Z : + ∀ u ∈ mu6Z, u ≠ 1 → 0 < norm (u - 1) ∧ norm (u - 1) ≤ 4 := by decide + +/-- **The reduction `μ₆ → (ℤ[ω]/2^w)ˣ` is injective for every `w ≥ 2`**, so the +unit action is free on the odd classes at every width, not only at the `w = 3` +the article uses. + +The argument is the norm: `2^w ∣ u - 1` would give `4^w ∣ N(u - 1)`, hence +`4^w ≤ N(u - 1) ≤ 4`, contradicting `4^w ≥ 16`. This fails at `w = 1` exactly +because `4 ≤ 4`, and indeed `-1 ≡ 1 (mod 2)`. -/ +theorem not_two_pow_dvd_unit_sub_one {w : ℕ} (hw : 2 ≤ w) {u : Eisenstein ℤ} + (hu : IsUnit u) (hu1 : u ≠ 1) : ¬ ((2 : Eisenstein ℤ) ^ w ∣ u - 1) := by + intro hdvd + obtain ⟨hpos, hle⟩ := norm_sub_one_of_mem_mu6Z u ((isUnit_iff_mem_mu6Z u).mp hu) hu1 + have hn : norm ((2 : Eisenstein ℤ) ^ w) ∣ norm (u - 1) := norm_dvd_norm hdvd + rw [norm_pow, norm_two] at hn + have h1 : (4 : ℤ) ^ w ≤ norm (u - 1) := Int.le_of_dvd hpos hn + have h2 : (4 : ℤ) ^ 2 ≤ (4 : ℤ) ^ w := pow_le_pow_right₀ (by norm_num) hw + norm_num at h2 + omega + +end CompElliptic.Rings.Eisenstein diff --git a/CompElliptic/TrustBoundary.lean b/CompElliptic/TrustBoundary.lean index 180cc41..748f4ff 100644 --- a/CompElliptic/TrustBoundary.lean +++ b/CompElliptic/TrustBoundary.lean @@ -12,6 +12,7 @@ import CompElliptic.Curves.Pasta.Fast.Projective import CompElliptic.Curves.Pasta.Fast.Msm import CompElliptic.Curves.Pasta.Fast.ProjectiveMontEquiv import CompElliptic.Fields.Sqrt +import CompElliptic.Rings.Eisenstein.Units import CompElliptic.Rings.Eisenstein.Orbits import CompElliptic.Meta.AxiomCheck @@ -63,6 +64,10 @@ not reach for `native_decide`, and here it does not have to. -/ assert_axioms CompElliptic.Rings.Eisenstein.norm_mul assert_axioms CompElliptic.Rings.Eisenstein.two_dvd_iff +assert_axioms CompElliptic.Rings.Eisenstein.isUnit_iff_norm_eq_one +assert_axioms CompElliptic.Rings.Eisenstein.isUnit_iff_mem_mu6Z +assert_axioms CompElliptic.Rings.Eisenstein.prime_two +assert_axioms CompElliptic.Rings.Eisenstein.not_two_pow_dvd_unit_sub_one assert_axioms CompElliptic.Rings.Eisenstein.mul_eq_zero_mod_two assert_axioms CompElliptic.Rings.Eisenstein.card_odd assert_axioms CompElliptic.Rings.Eisenstein.mu6_free_on_odd From ab0299c57222c06e385371ecd5d3f6ecb0d19056 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Fri, 28 Aug 2026 19:43:39 -0300 Subject: [PATCH 3/4] Rings/Eisenstein: identify Z[omega]/2 with F_4, not just with its properties MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The module already showed Z[omega]/2 has four elements, no zero divisors, and an inverse for every nonzero class. Those are the PROPERTIES of F_4; they did not name the field. This closes that gap with an explicit isomorphism onto `GaloisField 2 2`, which is Mathlib's F_4. The route is the classification of finite fields: a finite field is determined up to isomorphism by its cardinality, so a four-element field IS F_4. To use it the quotient has to be a field rather than merely a domain, so: `coeffHom` and `instAlgebra` (Basic.lean) make `R[omega]` an R-algebra, free of rank two on {1, omega}. The isomorphism is then one of ZMod 2-algebras, so it respects the coefficient embedding and not only the ring structure. `invTwo` and `instFieldModTwo` give the field structure, and it stays COMPUTABLE: the multiplicative group of a four-element field has order 3, so `x^3 = 1` for nonzero x and therefore `x⁻¹ = x^2`. Inversion is squaring, not a search, and `mul_invTwo` is a four-case `decide`. `algEquivGaloisField` and `nonempty_ringEquiv_galoisField` are the identification itself. It is noncomputable because the classification produces the isomorphism by choice, but it still censuses at the standard-axioms tier. Why this is worth stating rather than leaving implicit: being F_4 is exactly what INERT means. Were 2 split, the quotient would be F_2 x F_2, which also has four elements but has zero divisors and is not a field. Everything downstream that treats "odd" and "unit" as interchangeable mod 2^w, and the locality of Z[omega]/2^w with maximal ideal (2), rests on the field case rather than the product case, so the distinction is load-bearing. Co-Authored-By: Claude --- CompElliptic/Rings/Eisenstein/Basic.lean | 15 ++++++ CompElliptic/Rings/Eisenstein/Mod.lean | 65 ++++++++++++++++++++++-- CompElliptic/TrustBoundary.lean | 2 + 3 files changed, 78 insertions(+), 4 deletions(-) diff --git a/CompElliptic/Rings/Eisenstein/Basic.lean b/CompElliptic/Rings/Eisenstein/Basic.lean index c276aa3..b0e361a 100644 --- a/CompElliptic/Rings/Eisenstein/Basic.lean +++ b/CompElliptic/Rings/Eisenstein/Basic.lean @@ -5,6 +5,7 @@ as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Danny Willems -/ import Mathlib.Algebra.Ring.Hom.Defs +import Mathlib.Algebra.Algebra.Defs import Mathlib.Tactic.Ring import Mathlib.Tactic.LinearCombination @@ -210,6 +211,20 @@ def map (f : R →+* S) : Eisenstein R →+* Eisenstein S where @[simp] theorem map_apply_a (f : R →+* S) (x : Eisenstein R) : (map f x).a = f x.a := rfl @[simp] theorem map_apply_b (f : R →+* S) (x : Eisenstein R) : (map f x).b = f x.b := rfl +/-- The coefficient embedding `R → R[ω]`, `r ↦ r + 0·ω`. -/ +def coeffHom : R →+* Eisenstein R where + toFun r := ⟨r, 0⟩ + map_one' := rfl + map_mul' := by intros; ext <;> simp + map_zero' := rfl + map_add' := by intros; ext <;> simp + +@[simp] theorem coeffHom_a (r : R) : (coeffHom r : Eisenstein R).a = r := rfl +@[simp] theorem coeffHom_b (r : R) : (coeffHom r : Eisenstein R).b = 0 := rfl + +/-- `R[ω]` is an `R`-algebra, free of rank two on `{1, ω}`. -/ +instance instAlgebra : Algebra R (Eisenstein R) := (coeffHom (R := R)).toAlgebra + /-- **The universal property.** `R[ω]` is initial among `R`-algebras carrying a root of `X² + X + 1`: given a coefficient hom `f : R →+* S` and any `z : S` with `z² + z + 1 = 0`, evaluation `a + b·ω ↦ f a + f b · z` is a ring hom. diff --git a/CompElliptic/Rings/Eisenstein/Mod.lean b/CompElliptic/Rings/Eisenstein/Mod.lean index d50313a..56cecf3 100644 --- a/CompElliptic/Rings/Eisenstein/Mod.lean +++ b/CompElliptic/Rings/Eisenstein/Mod.lean @@ -6,6 +6,7 @@ Authors: Danny Willems -/ import CompElliptic.Rings.Eisenstein.Basic import Mathlib.Data.ZMod.Basic +import Mathlib.FieldTheory.Finite.GaloisField /-! # The finite quotients `ℤ[ω]/n`, computably @@ -20,10 +21,12 @@ claims in `Rings.Eisenstein.Orbits` are settled by kernel `decide`. * `Eisenstein.card_eq` — `#(ℤ[ω]/n) = n²`. * `Eisenstein.two_dvd_iff` — an element is even exactly when both coordinates are, so halving is exact and coordinate-wise. -* `Eisenstein.mod_two_eq_zero_or_isUnit`, `Eisenstein.mul_eq_zero_mod_two` — - `ℤ[ω]/2` is the field `𝔽₄`, i.e. `2` is inert. This is what makes - "odd" and "unit" the same predicate mod `2^w`, and it is why `ℤ[ω]/2^w` is a - local ring with maximal ideal `(2)`. +* `Eisenstein.instFieldModTwo`, `Eisenstein.algEquivGaloisField` — `ℤ[ω]/2` is + not merely *a* four-element field with no zero divisors: it **is** `𝔽₄`, as an + explicit isomorphism onto `GaloisField 2 2`. That is the precise content of + `2` being INERT rather than split, and it is what makes "odd" and "unit" the + same predicate mod `2^w`, hence why `ℤ[ω]/2^w` is a local ring with maximal + ideal `(2)`. -/ namespace CompElliptic.Rings.Eisenstein @@ -101,4 +104,58 @@ so a class is a unit exactly when it is nonzero. This is the fact that lets theorem exists_inv_mod_two (x : Eisenstein (ZMod 2)) (hx : x ≠ 0) : ∃ y, x * y = 1 := by revert x; decide +/-! ## `ℤ[ω]/2` is `𝔽₄` + +The three facts above say `ℤ[ω]/2` is a commutative ring with four elements in +which every nonzero element is invertible. That makes it a field of order `4`, +and finite fields of equal cardinality are isomorphic, so it is `𝔽₄` — which +`GaloisField 2 2` denotes. Below, that identification is made explicit. + +The inverse is computable and needs no search: the multiplicative group of a +four-element field has order `3`, so `x³ = 1` for `x ≠ 0` and therefore +`x⁻¹ = x²`. -/ + +/-- Inversion in `ℤ[ω]/2`. The unit group has order `3`, so squaring inverts. -/ +def invTwo (x : Eisenstein (ZMod 2)) : Eisenstein (ZMod 2) := x ^ 2 + +/-- Squaring really does invert: `x · x² = x³ = 1` for every nonzero `x`. -/ +theorem mul_invTwo (x : Eisenstein (ZMod 2)) (hx : x ≠ 0) : x * invTwo x = 1 := by + revert x; decide + +/-- **`ℤ[ω]/2` is a field.** Computable: the inverse is squaring, not a search. -/ +instance instFieldModTwo : Field (Eisenstein (ZMod 2)) := + { instCommRing with + inv := invTwo + exists_pair_ne := ⟨0, 1, by decide⟩ + mul_inv_cancel := mul_invTwo + inv_zero := by decide + nnqsmul := _ + qsmul := _ } + +/-- Its cardinality is `2² = 4`, in the shape the classification wants. -/ +theorem card_mod_two_eq_pow : Fintype.card (Eisenstein (ZMod 2)) = 2 ^ 2 := by + rw [card_mod_two]; norm_num + +/-- **`ℤ[ω]/2 ≅ 𝔽₄`.** A finite field is determined up to isomorphism by its +cardinality, so the four-element field `ℤ[ω]/2` is `GaloisField 2 2`, Mathlib's +`𝔽₄`. The isomorphism is one of `ZMod 2`-algebras, so it respects the coefficient +embedding as well as the ring structure. + +This is the precise statement that `2` is INERT in `ℤ[ω]`: were `2` split, the +quotient would be `𝔽₂ × 𝔽₂`, which has four elements but zero divisors and is +not a field. The `𝔽₄`-ness is exactly what fails in that case, and it is what the +rest of the development uses when it treats "odd" and "unit" as the same +predicate. + +Noncomputable because the classification produces the isomorphism by choice; the +field structure itself (`instFieldModTwo`) stays computable. -/ +noncomputable def algEquivGaloisField : + Eisenstein (ZMod 2) ≃ₐ[ZMod 2] GaloisField 2 2 := + GaloisField.algEquivGaloisFieldOfFintype 2 2 card_mod_two_eq_pow + +/-- `ℤ[ω]/2` and `𝔽₄` are isomorphic as rings. -/ +theorem nonempty_ringEquiv_galoisField : + Nonempty (Eisenstein (ZMod 2) ≃+* GaloisField 2 2) := + ⟨algEquivGaloisField.toRingEquiv⟩ + end CompElliptic.Rings.Eisenstein diff --git a/CompElliptic/TrustBoundary.lean b/CompElliptic/TrustBoundary.lean index 748f4ff..c60ffcf 100644 --- a/CompElliptic/TrustBoundary.lean +++ b/CompElliptic/TrustBoundary.lean @@ -69,6 +69,8 @@ assert_axioms CompElliptic.Rings.Eisenstein.isUnit_iff_mem_mu6Z assert_axioms CompElliptic.Rings.Eisenstein.prime_two assert_axioms CompElliptic.Rings.Eisenstein.not_two_pow_dvd_unit_sub_one assert_axioms CompElliptic.Rings.Eisenstein.mul_eq_zero_mod_two +assert_axioms CompElliptic.Rings.Eisenstein.mul_invTwo +assert_axioms CompElliptic.Rings.Eisenstein.nonempty_ringEquiv_galoisField assert_axioms CompElliptic.Rings.Eisenstein.card_odd assert_axioms CompElliptic.Rings.Eisenstein.mu6_free_on_odd assert_axioms CompElliptic.Rings.Eisenstein.reps_cover From 6b3614112cff8085abb32af3d5ee7c82cdc3de87 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 31 Aug 2026 08:49:20 -0300 Subject: [PATCH 4/4] CurveForms/Automorphisms: the six automorphisms of a j = 0 curve Proves the FORM of the automorphism group of `y^2 = x^3 + B` over a field with a primitive cube root of unity z: the maps are exactly (x, y) |-> (z^k * x, +-y), k in {0, 1, 2} and there are six of them. Instantiated on Pallas and Vesta. Why that is the shape: preserving `y^2 = x^3 + B` lets x be scaled only by a cube root, since that is what leaves x^3 alone, and lets y carry only a sign, since that is what leaves y^2 alone. The curve constrains nothing else. So the group is mu_3 x mu_2, cyclic of order 6 because 3 and 2 are coprime, generated by sigma(x, y) = (z*x, -y) with sigma^3 the negation map and sigma^2 the endomorphism used for GLV. `Endomorphism.lean` is carried over unchanged from the earlier GLV endomorphism work; it compiles against current main as-is and supplies the x-scaling phi together with the proof that it commutes with the chord-and-tangent group law. The six automorphisms are then built by composing phi with negation, so no new reasoning about the addition formulas is needed. `phi_eq_lambda_nsmul` is NOT carried over, since it depends on a HasseBound that does not exist here; the underlying `phiPt_eq_nsmul` does come across and needs only `Nat.card`. Automorphisms.lean: `autPt_x` and `autPt_y` are the form itself, and the second is the one that matters downstream -- the map only ever applies a sign to y and never mixes the coordinates, which is why an orbit has three x-coordinates but a single +-y pair. `autPt_add` makes each map a homomorphism, `autPt_comp` the group law (exponents add, signs multiply), and `autEquiv` packages each as an additive automorphism with the inverse of (k, s) given by (2k, s). It also connects the two places mu_6 shows up. The unit group of Z[omega] is mu_6, and `autOfUnit` makes the six units act as the six automorphisms: `unitIndex` reads a unit eps*omega^k as its exponent and sign, `unitIndex_injOn` shows the six units give six different maps, and `autOfUnit_mul` shows the action is multiplicative. So the coincidence of the two mu_6's is a theorem rather than a remark. PastaAut.lean pins zeta for each curve and checks the six are genuinely distinct at G = (-1, 2), so the automorphism group really does contain mu_6 rather than collapsing. `ZETA_quad` records that zeta satisfies the same relation `z^2 + z + 1 = 0` that the adjoined omega does, which is what identifies the x-scalings with the cube roots of unity in Z[omega]. Everything is kernel `decide`; the two `native_decide` strings in Endomorphism.lean are docstring prose, not uses. Nine further results join the census, all at the standard-axioms tier. Co-Authored-By: Claude --- CompElliptic.lean | 3 + CompElliptic/CurveForms/Automorphisms.lean | 218 +++++++++++++++++++ CompElliptic/Curves/PastaAut.lean | 100 +++++++++ CompElliptic/Endomorphism.lean | 240 +++++++++++++++++++++ CompElliptic/TrustBoundary.lean | 18 ++ 5 files changed, 579 insertions(+) create mode 100644 CompElliptic/CurveForms/Automorphisms.lean create mode 100644 CompElliptic/Curves/PastaAut.lean create mode 100644 CompElliptic/Endomorphism.lean diff --git a/CompElliptic.lean b/CompElliptic.lean index 3307228..97ca547 100644 --- a/CompElliptic.lean +++ b/CompElliptic.lean @@ -28,6 +28,9 @@ 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 diff --git a/CompElliptic/CurveForms/Automorphisms.lean b/CompElliptic/CurveForms/Automorphisms.lean new file mode 100644 index 0000000..9bbd850 --- /dev/null +++ b/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 diff --git a/CompElliptic/Curves/PastaAut.lean b/CompElliptic/Curves/PastaAut.lean new file mode 100644 index 0000000..5dfd11e --- /dev/null +++ b/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 diff --git a/CompElliptic/Endomorphism.lean b/CompElliptic/Endomorphism.lean new file mode 100644 index 0000000..15dca51 --- /dev/null +++ b/CompElliptic/Endomorphism.lean @@ -0,0 +1,240 @@ +/- +Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +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: Daira-Emma Hopwood +-/ +import CompElliptic.CurveForms.ShortWeierstrass +import Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic + +/-! +# The GLV endomorphism on a short-Weierstrass curve with `A = 0` + +For a curve `y² = x³ + B` (so `A = 0`) over a field containing a primitive cube root of unity `ζ`, +the map `φ (x, y) = (ζ x, y)` is a group endomorphism. On a group of prime order it must act as +multiplication by *some* scalar; a single spot-check on a generator identifies which. This is the +GLV endomorphism, the basis of the GLV scalar decomposition. + +Three layers: + +1. **Pure finite-group theory** (`endo_eq_nsmul_of_prime_card`) — no elliptic curves at all: an + endomorphism of a group of prime order `r` that sends one non-identity element `g` to `[lam] g` + is `[lam]` everywhere. +2. **Raw computable kernel** — `phi` on `F × F`, with `phi_add` proving it commutes with the raw + `add` (for `A = 0`). Notably this needs *no* hypotheses beyond `ζ³ = 1`: not `Valid`, not + `IsElliptic`, not `B ≠ 0`. The slope scales by `ζ²` in *both* branches of `add` + (`3(ζx)²/(2y) = ζ²·s` for doubling, `(y₂-y₁)/(ζx₂-ζx₁) = ζ⁻¹·s = ζ²·s` for distinct `x`), the + branch guards are preserved exactly (`ζ ≠ 0`), and even the junk-division cases agree because + both sides produce `0/0 = 0`. +3. **Rich bundled types** — `phiPt` / `phiHom` (`φ` as an `AddMonoidHom`), and + `phiPt_eq_nsmul`, which combines layers 1 and 2: given the group order (a prime `r`) and + the spot-check `φ G = [lam] G` on a non-identity `G`, conclude `φ P = [lam] P` for *every* `P`. + +`A = 0` is essential: for `A ≠ 0` the equation `y² = (ζx)³ + A(ζx) + B` fails. This covers the +Pasta curves (`y² = x³ + 5`), and every curve GLV is used on in practice. + +Everything here is a real proof; the numeric facts (`ζ³ = 1`, and the spot-check) are per-curve +closed facts and live in the concrete-curve modules. +-/ + +namespace CompElliptic.Endomorphism + +-- Open only `CurveForms`, never the `ShortWeierstrass` leaf: every borrowed name then reads +-- `ShortWeierstrass.…` at its use site, so its origin is visible without a full path. +open CompElliptic.CurveForms + +/-! ## Layer 1: an endomorphism of a prime-order group is multiplication by a scalar + +Pure finite-group theory, with no reference to elliptic curves. In a group of prime order `r`, +every element is a multiple of any non-identity element `g` (`mem_multiples_of_prime_card`, which +derives `Finite` internally from `Nat.card G = r` and primality). An additive hom therefore is +pinned by its value on `g` alone. -/ + +/-- If `G` has prime order `r`, `f` is an endomorphism of `G`, and `f g = [lam] g` for a single +non-identity `g`, then `f = [lam]` on all of `G`. + +This is the general theorem behind `φ = [λ]`: it reduces the claim on the whole group to one +*closed, spot-checkable fact* about a single point — the *Independently re-checkable trust* +principle. -/ +theorem endo_eq_nsmul_of_prime_card {G : Type*} [AddGroup G] {r : ℕ} [Fact r.Prime] + (hcard : Nat.card G = r) (f : G →+ G) {g : G} (hg : g ≠ 0) {lam : ℕ} + (hspot : f g = lam • g) (x : G) : f x = lam • x := by + obtain ⟨n, rfl⟩ := (AddSubmonoid.mem_multiples_iff x g).mp (mem_multiples_of_prime_card hcard hg) + rw [map_nsmul, hspot, nsmul_left_comm] + +variable {F : Type*} [Field F] + +/-! ## Layer 2: the raw computable kernel + +The `φ`-specific facts need only `[Field F]`; `[DecidableEq F]` enters at `phi_add`, where the +branch structure of `add` does. -/ + +/-- The GLV map `φ (x, y) = (z x, y)` on raw coordinates. For `z` a primitive cube root of unity it +is a nontrivial endomorphism of the curve group (`phi_add`, `onCurve_phi`). -/ +def phi (z : F) (p : F × F) : F × F := (z * p.1, p.2) + +variable {z : F} + +/-- A cube root of unity is nonzero. -/ +theorem zeta_ne_zero (hz : z ^ 3 = 1) : z ≠ 0 := by + intro h + rw [h] at hz + simp at hz + +/-- `z⁻¹ = z²` for a cube root of unity — the identity behind the slope scaling. -/ +theorem zeta_inv (hz : z ^ 3 = 1) : z⁻¹ = z ^ 2 := + inv_eq_of_mul_eq_one_right (by linear_combination hz) + +/-- Scaling the *denominator* of a slope by `z` scales the slope by `z²`. Holds unconditionally +(no `b ≠ 0` needed): for `b = 0` both sides are `0`, since `x / 0 = 0` in Lean. -/ +theorem div_zeta_mul (hz : z ^ 3 = 1) (a b : F) : a / (z * b) = z ^ 2 * (a / b) := by + rw [div_mul_eq_div_div_swap, div_eq_mul_inv _ z, zeta_inv hz] + ring + +/-- `φ` fixes the `(0, 0)` identity sentinel. -/ +@[simp] theorem phi_origin (z : F) : phi z ((0, 0) : F × F) = (0, 0) := by + simp [phi] + +/-- `φ` reflects the identity sentinel: `φ p = 𝒪` exactly when `p = 𝒪`. This is what makes the +`𝒪` branch guards of `add` line up on both sides of `phi_add`. -/ +theorem phi_eq_origin_iff (hz : z ^ 3 = 1) (p : F × F) : phi z p = (0, 0) ↔ p = (0, 0) := by + simp [phi, Prod.ext_iff, zeta_ne_zero hz] + +/-- `φ` maps the curve `y² = x³ + b` to itself: `(z x)³ = x³` when `z³ = 1`. (`A = 0` is essential.) -/ +theorem onCurve_phi {b : F} (hz : z ^ 3 = 1) {p : F × F} + (h : ShortWeierstrass.OnCurve 0 b p) : ShortWeierstrass.OnCurve 0 b (phi z p) := by + simp only [ShortWeierstrass.OnCurve, phi] at h ⊢ + linear_combination h - p.1 ^ 3 * hz + +/-- `φ` preserves representability (`on the curve, or 𝒪`). -/ +theorem valid_phi {b : F} (hz : z ^ 3 = 1) {p : F × F} (h : ShortWeierstrass.Valid 0 b p) : + ShortWeierstrass.Valid 0 b (phi z p) := by + rcases h with h | h + · exact Or.inl (onCurve_phi hz h) + · exact Or.inr (by rw [h, phi_origin]) + +/-- `φ³ = id`: `φ` is an automorphism of order dividing 3. Purely computational (`z³ = 1` on the +`x`-coordinate), so it needs neither the group order nor the `φ = [lam]` identification. -/ +theorem phi_phi_phi (hz : z ^ 3 = 1) (p : F × F) : phi z (phi z (phi z p)) = p := by + obtain ⟨x, y⟩ := p + simp only [phi, Prod.mk.injEq] + exact ⟨by linear_combination x * hz, trivial⟩ + +/-- The shared chord/tangent core of `phi_add`, `x`-coordinate half: with the slope scaled to +`z² · lam`, the new `x` scales by `z`. -/ +theorem phi_addX (hz : z ^ 3 = 1) (lam x₁ x₂ : F) : + (z ^ 2 * lam) ^ 2 - z * x₁ - z * x₂ = z * (lam ^ 2 - x₁ - x₂) := by + linear_combination (z * lam ^ 2) * hz + +/-- The shared chord/tangent core of `phi_add`, `y`-coordinate half: with the slope scaled to +`z² · lam` and `x` scaled by `z`, the new `y` is *unchanged*. -/ +theorem phi_addY (hz : z ^ 3 = 1) (lam x₁ x₂ y₁ : F) : + (z ^ 2 * lam) * (z * x₁ - ((z ^ 2 * lam) ^ 2 - z * x₁ - z * x₂)) - y₁ + = lam * (x₁ - (lam ^ 2 - x₁ - x₂)) - y₁ := by + linear_combination (lam * (2 * x₁ + x₂) - lam ^ 3 * (z ^ 3 + 1)) * hz + +variable [DecidableEq F] + +/-- **`φ` commutes with the group law** (for `A = 0`), on raw coordinates. + +Strikingly, this needs no hypotheses at all beyond `z³ = 1`: no `Valid`, no `IsElliptic`, no +`B ≠ 0`. Every branch guard of `add` is preserved by `φ` (`z ≠ 0`), and both branches scale the +slope by exactly `z²`, after which `phi_addX` / `phi_addY` finish. The degenerate divisions +(`y = 0` in the doubling branch) need no side condition either, since `x / 0 = 0` on both sides. + +The branch walk is explicit (`by_cases` + `rw [if_pos/if_neg]`) rather than +`split_ifs <;> simp_all`, which blows the recursion limit on the nested `ite`s (cf. `add_neg`). -/ +theorem phi_add (hz : z ^ 3 = 1) (p q : F × F) : + phi z (ShortWeierstrass.add 0 p q) = ShortWeierstrass.add 0 (phi z p) (phi z q) := by + have hz0 : z ≠ 0 := zeta_ne_zero hz + by_cases hp0 : p = (0, 0) + · rw [hp0, ShortWeierstrass.zero_add, phi_origin, ShortWeierstrass.zero_add] + by_cases hq0 : q = (0, 0) + · rw [hq0, ShortWeierstrass.add_zero, phi_origin, ShortWeierstrass.add_zero] + have hp0' : phi z p ≠ (0, 0) := fun h => hp0 ((phi_eq_origin_iff hz p).mp h) + have hq0' : phi z q ≠ (0, 0) := fun h => hq0 ((phi_eq_origin_iff hz q).mp h) + -- `φ` preserves the two remaining guards: same `x` (as `z ≠ 0`), and `y₁ + y₂ = 0` (`y` is fixed). + have hxg : (phi z p).1 = (phi z q).1 ↔ p.1 = q.1 := by + simp [phi, mul_right_inj' hz0] + have hyg : (phi z p).2 + (phi z q).2 = 0 ↔ p.2 + q.2 = 0 := by simp [phi] + unfold ShortWeierstrass.add + rw [if_neg hp0, if_neg hq0, if_neg hp0', if_neg hq0'] + by_cases hx : p.1 = q.1 + · rw [if_pos hx, if_pos (hxg.mpr hx)] + by_cases hy : p.2 + q.2 = 0 + · rw [if_pos hy, if_pos (hyg.mpr hy), phi_origin] + · rw [if_neg hy, if_neg (fun h => hy (hyg.mp h))] + -- doubling: the slope `3(z x)²/(2y)` is `z² ·` the original slope. + have hlam : (3 * (phi z p).1 ^ 2 + 0) / (2 * (phi z p).2) + = z ^ 2 * ((3 * p.1 ^ 2 + 0) / (2 * p.2)) := by + simp only [phi] + rw [← mul_div_assoc] + ring_nf + simp only [phi, Prod.mk.injEq] + simp only [phi] at hlam + rw [hlam] + exact ⟨(phi_addX hz _ _ _).symm, (phi_addY hz _ _ _ _).symm⟩ + · rw [if_neg hx, if_neg (fun h => hx (hxg.mp h))] + -- distinct `x`: the slope `(y₂-y₁)/(z x₂ - z x₁)` is `z⁻¹ = z²` times the original slope. + have hlam : ((phi z q).2 - (phi z p).2) / ((phi z q).1 - (phi z p).1) + = z ^ 2 * ((q.2 - p.2) / (q.1 - p.1)) := by + simp only [phi] + rw [← mul_sub, div_zeta_mul hz] + simp only [phi, Prod.mk.injEq] + simp only [phi] at hlam + rw [hlam] + exact ⟨(phi_addX hz _ _ _).symm, (phi_addY hz _ _ _ _).symm⟩ + +/-! ## Layer 3: `φ` on the rich point type -/ + +/-- `φ` on `SWPoint E`, for a curve with `A = 0` and a cube root of unity `z`. The two proofs are +`Prop`s, hence erased: `phiPt` computes, and is `native_decide`-friendly. -/ +def phiPt {E : ShortWeierstrass.SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) + (P : ShortWeierstrass.SWPoint E) : ShortWeierstrass.SWPoint E := + ⟨z * P.x, P.y, by + have h : ShortWeierstrass.Valid 0 E.B (P.x, P.y) := hA ▸ P.onCurve + have h' : ShortWeierstrass.Valid 0 E.B (phi z (P.x, P.y)) := valid_phi hz h + rw [hA] + exact h'⟩ + +omit [DecidableEq F] in +/-- The coordinates of `φ P` are the raw `phi` of `P`'s coordinates — the bridge that lets the raw +lemmas above discharge the `SWPoint` ones. -/ +@[simp] theorem phiPt_coords {E : ShortWeierstrass.SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) + (P : ShortWeierstrass.SWPoint E) : + ((phiPt hA hz P).x, (phiPt hA hz P).y) = phi z (P.x, P.y) := rfl + +omit [DecidableEq F] in +/-- `φ³ = id` on `SWPoint E`. -/ +theorem phiPt_phiPt_phiPt {E : ShortWeierstrass.SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) + (P : ShortWeierstrass.SWPoint E) : + phiPt hA hz (phiPt hA hz (phiPt hA hz P)) = P := + ShortWeierstrass.SWPoint.ext_pair (phi_phi_phi hz (P.x, P.y)) + +/-- `φ` is additive on `SWPoint E` — the group-law commutation of `phi_add`, lifted. -/ +theorem phiPt_add {E : ShortWeierstrass.SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) + (P Q : ShortWeierstrass.SWPoint E) : + phiPt hA hz (P + Q) = phiPt hA hz P + phiPt hA hz Q := by + refine ShortWeierstrass.SWPoint.ext_pair ?_ + show phi z (ShortWeierstrass.add E.A (P.x, P.y) (Q.x, Q.y)) + = ShortWeierstrass.add E.A (phi z (P.x, P.y)) (phi z (Q.x, Q.y)) + rw [hA] + exact phi_add hz _ _ + +/-- `φ` as an `AddMonoidHom` on `SWPoint E` — the input to `endo_eq_nsmul_of_prime_card`. -/ +def phiHom {E : ShortWeierstrass.SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) : + ShortWeierstrass.SWPoint E →+ ShortWeierstrass.SWPoint E := + AddMonoidHom.mk' (phiPt hA hz) (phiPt_add hA hz) + +/-- **`φ = [lam]` on the whole group**, from the group order and a single spot-check. + +Layers 1 and 2 combined: `φ` is an endomorphism (`phiHom`, proved outright), the group has prime +order `r` (a curve fact), and `φ G = [lam] G` for one non-identity `G` (a closed, `native_decide`- +checkable fact). Hence `φ P = [lam] P` for every `P`. -/ +theorem phiPt_eq_nsmul {E : ShortWeierstrass.SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) + {r : ℕ} [Fact r.Prime] (hcard : Nat.card (ShortWeierstrass.SWPoint E) = r) + {G : ShortWeierstrass.SWPoint E} (hG : G ≠ 0) {lam : ℕ} (hspot : phiPt hA hz G = lam • G) + (P : ShortWeierstrass.SWPoint E) : phiPt hA hz P = lam • P := + endo_eq_nsmul_of_prime_card hcard (phiHom hA hz) hG hspot P + +end CompElliptic.Endomorphism diff --git a/CompElliptic/TrustBoundary.lean b/CompElliptic/TrustBoundary.lean index c60ffcf..18491f6 100644 --- a/CompElliptic/TrustBoundary.lean +++ b/CompElliptic/TrustBoundary.lean @@ -12,6 +12,7 @@ import CompElliptic.Curves.Pasta.Fast.Projective import CompElliptic.Curves.Pasta.Fast.Msm import CompElliptic.Curves.Pasta.Fast.ProjectiveMontEquiv import CompElliptic.Fields.Sqrt +import CompElliptic.Curves.PastaAut import CompElliptic.Rings.Eisenstein.Units import CompElliptic.Rings.Eisenstein.Orbits import CompElliptic.Meta.AxiomCheck @@ -55,6 +56,23 @@ assert_axioms CompElliptic.CurveOrder.card_eq_of_prime_witness_of_card_lt_three_ assert_axioms CompElliptic.Fields.TonelliShanks.sqrt?_mul_self assert_axioms CompElliptic.Fields.TonelliShanks.sqrt?_isSome_of_isSquare +/-! ## The six automorphisms of a `j = 0` curve — standard axioms only + +The coordinate form, additivity and the group law are general theorems over any +field with a cube root of unity. The Pasta-specific facts (the constant `ζ`, and +that the six automorphisms are distinct) are concrete closed facts settled by +KERNEL `decide`, so they add no axiom and need no `+native` entry. -/ + +assert_axioms CompElliptic.Endomorphism.phiPt_add +assert_axioms CompElliptic.CurveForms.Automorphisms.autPt_x +assert_axioms CompElliptic.CurveForms.Automorphisms.autPt_y +assert_axioms CompElliptic.CurveForms.Automorphisms.autPt_add +assert_axioms CompElliptic.CurveForms.Automorphisms.autPt_comp +assert_axioms CompElliptic.CurveForms.Automorphisms.autOfUnit_mul +assert_axioms CompElliptic.Curves.Pasta.Pallas.ZETA_cube +assert_axioms CompElliptic.Curves.Pasta.Pallas.aut_nodup_at_Gpt +assert_axioms CompElliptic.Curves.Pasta.Vesta.aut_nodup_at_Gpt + /-! ## The Eisenstein ring `ℤ[ω]` and its unit action — standard axioms only The finite claims (`card_odd`, the freeness and Burnside counts, the covering)