From d15e6d2c0580b0e3743198b31184a52ab81d3d05 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 13 Jul 2026 10:42:10 +0200 Subject: [PATCH 1/6] feat(Endomorphism): the GLV endomorphism for short-Weierstrass A = 0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit For `y² = x³ + B` over a field with a primitive cube root of unity `ζ`, the map `φ (x, y) = (ζ x, y)` is a group endomorphism, and on a prime-order group it must act as multiplication by some scalar. This is the basis of the GLV scalar decomposition; the concrete Pasta constants follow separately. Three layers, mirroring `CurveOrder.lean`: * 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 `g` to `[lam] g` is `[lam]` everywhere, via Mathlib's `mem_multiples_of_prime_card` (which derives `Finite` internally from `Nat.card G = r` and primality, so no `IsCyclic` / `zpowers` machinery is needed). This is what reduces `φ = [λ]` on the whole group to a single closed, spot-checkable fact about one point. * Raw computable kernel: `phi` on `F × F`, with `phi_add` proving it commutes with the raw `add`. This needs *no* hypotheses beyond `ζ³ = 1`: not `Valid`, not `IsElliptic`, not `B ≠ 0`. The slope scales by `ζ²` in *both* branches (`3(ζx)²/(2y) = ζ²·s` doubling, `(y₂-y₁)/(ζx₂-ζx₁) = ζ⁻¹·s = ζ²·s` for distinct `x`), the branch guards are preserved exactly (`ζ ≠ 0`), and the degenerate divisions agree because both sides produce `0/0 = 0`. The branch walk is explicit, not `split_ifs <;> simp_all`, which blows the recursion limit on the nested `ite`s (cf. `add_neg`). * Rich bundled types: `SWPoint.phiPt` / `SWPoint.phiHom` (`φ` as an `AddMonoidHom`), and the capstone `SWPoint.phiPt_eq_nsmul` combining the two layers above. `A = 0` is essential (for `A ≠ 0`, `y² = (ζx)³ + A(ζx) + B` fails), which covers the Pasta curves and every curve GLV is used on in practice. No `sorry`; every declaration depends only on `propext` / `Classical.choice` / `Quot.sound`. No `decide` or `native_decide` here: the numeric facts (`ζ³ = 1` and the spot-check) are per-curve closed facts, and land with the curves. --- CompElliptic.lean | 1 + CompElliptic/CurveForms/Endomorphism.lean | 217 ++++++++++++++++++++++ 2 files changed, 218 insertions(+) create mode 100644 CompElliptic/CurveForms/Endomorphism.lean diff --git a/CompElliptic.lean b/CompElliptic.lean index 513c96c..98853df 100644 --- a/CompElliptic.lean +++ b/CompElliptic.lean @@ -13,6 +13,7 @@ import CompElliptic.Encodings.Pasta import CompElliptic.Fields.Pasta import CompElliptic.Fields.Sqrt import CompElliptic.CurveForms.ShortWeierstrass +import CompElliptic.CurveForms.Endomorphism import CompElliptic.CurveOrder import CompElliptic.Curves.Pasta import CompElliptic.Curves.PastaOrder diff --git a/CompElliptic/CurveForms/Endomorphism.lean b/CompElliptic/CurveForms/Endomorphism.lean new file mode 100644 index 0000000..568a525 --- /dev/null +++ b/CompElliptic/CurveForms/Endomorphism.lean @@ -0,0 +1,217 @@ +/- +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** — `SWPoint.phiPt` / `SWPoint.phiHom` (`φ` as an `AddMonoidHom`), and + `SWPoint.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.CurveForms.ShortWeierstrass + +/-! ## 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 : OnCurve 0 b p) : + OnCurve 0 b (phi z p) := by + simp only [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 : Valid 0 b p) : + 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]) + +/-- 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 (add 0 p q) = 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, zero_add, phi_origin, zero_add] + by_cases hq0 : q = (0, 0) + · rw [hq0, add_zero, phi_origin, 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 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 SWPoint.phiPt {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) (P : SWPoint E) : SWPoint E := + ⟨z * P.x, P.y, by + have h : Valid 0 E.B (P.x, P.y) := hA ▸ P.onCurve + have h' : Valid 0 E.B (phi z (P.x, P.y)) := valid_phi hz h + rw [hA] + exact h'⟩ + +omit [DecidableEq F] in +@[simp] theorem SWPoint.phiPt_coords {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) + (P : SWPoint E) : + ((SWPoint.phiPt hA hz P).x, (SWPoint.phiPt hA hz P).y) = phi z (P.x, P.y) := rfl + +/-- `φ` is additive on `SWPoint E` — the group-law commutation of `phi_add`, lifted. -/ +theorem SWPoint.phiPt_add {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) (P Q : SWPoint E) : + SWPoint.phiPt hA hz (P + Q) = SWPoint.phiPt hA hz P + SWPoint.phiPt hA hz Q := by + refine SWPoint.ext_pair ?_ + show phi z (add E.A (P.x, P.y) (Q.x, Q.y)) + = 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 SWPoint.phiHom {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) : SWPoint E →+ SWPoint E := + AddMonoidHom.mk' (SWPoint.phiPt hA hz) (SWPoint.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 SWPoint.phiPt_eq_nsmul {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) + {r : ℕ} [Fact r.Prime] (hcard : Nat.card (SWPoint E) = r) + {G : SWPoint E} (hG : G ≠ 0) {lam : ℕ} (hspot : SWPoint.phiPt hA hz G = lam • G) + (P : SWPoint E) : SWPoint.phiPt hA hz P = lam • P := + endo_eq_nsmul_of_prime_card hcard (SWPoint.phiHom hA hz) hG hspot P + +end CompElliptic.CurveForms.ShortWeierstrass From 5bfda01e3cb9919b028771b76986a83c62a58fd2 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 13 Jul 2026 10:42:32 +0200 Subject: [PATCH 2/6] docs(design): the GLV endomorphism implementation plan MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Records the design for GLV on the Pasta curves: the endomorphism itself (this PR), the concrete Pallas / Vesta constants and the `φ = [λ]` spot-check, the Plausible property-test harness, and the scalar decomposition that follows. Includes the findings that shaped it: the slope scales by `ζ²` in both branches of `add` (so `phi_add` needs no side conditions); `mem_multiples_of_prime_card` removes the need for any cyclic-group machinery; the `ζ` / `λ` numeric facts are kernel-`decide`-able, so only the point spot-check needs `native_decide` (`binNsmul` is well-founded recursion, so kernel `decide` gets stuck, not merely slow); and Plausible's stock generators cap at 100, so a crypto-size field needs a uniform `Arbitrary (ZMod n)` built on `Gen.choose`. Also notes that the `plausible` *tactic* closes goals with `sorry` when it finds no counterexample, so only `#test` / `#eval Testable.check` are usable here. --- design/glv-endomorphism-plan.md | 418 ++++++++++++++++++++++++++++++++ 1 file changed, 418 insertions(+) create mode 100644 design/glv-endomorphism-plan.md diff --git a/design/glv-endomorphism-plan.md b/design/glv-endomorphism-plan.md new file mode 100644 index 0000000..fa95269 --- /dev/null +++ b/design/glv-endomorphism-plan.md @@ -0,0 +1,418 @@ +# GLV endomorphism: implementation plan + +Status as of 2026-07-13: nothing GLV-related exists in the repo. A grep for +`glv|endomorph|lambda|cube root` returns one unrelated TODO line about windowed +scalar multiplication. This document is the design for the first step. + +Every Lean fragment below was compiled against this repo's pinned Mathlib +(`lake env lean`) before being written down. The prototypes lived in a scratch +directory, not in the repo, so nothing here is committed code yet. + +## Context + +The goal is the GLV endomorphism on the Pasta curves: the map +`phi(x, y) = (zeta * x, y)`, where `zeta` is a primitive cube root of unity in +the base field, which acts on the prime-order group as multiplication by a +scalar `lambda` (a primitive cube root of unity in the scalar field). The first +step is the endomorphism itself plus the field and curve properties it rests +on, verified both by proof and by property-based tests. Scalar decomposition +(`k = k1 + k2 * lambda`) is deliberately deferred to a follow-on. + +### What already exists to build on + +| Piece | File | +| --- | --- | +| Pasta base/scalar fields `ZMod p` / `ZMod q`, Pratt certificates | `CompElliptic/Fields/Pasta.lean` | +| Short-Weierstrass kernel (`OnCurve`, `add`, `neg`, `Valid`), `SWCurve` / `SWPoint`, `AddCommGroup` | `CompElliptic/CurveForms/ShortWeierstrass.lean` | +| Fast `n` smul `P` (binary double-and-add, `native_decide`-friendly at 2^254) | `CompElliptic/ScalarMul.lean` | +| Pallas/Vesta as `SWCurve`, test point `G = (-1, 2)` | `CompElliptic/Curves/Pasta.lean` | +| Group order `= q` (Pallas) / `= p` (Vesta), given the `HasseBound` hypothesis | `CompElliptic/CurveOrder.lean`, `CompElliptic/Curves/PastaOrder.lean` | + +Plausible is already available transitively via Mathlib and is listed in +`lake-manifest.json`, so the property-based tests need no new dependency. + +## Findings + +### 1. phi is an additive endomorphism, and it needs no hypotheses at all + +The slope scales by `zeta^2` in *both* branches of `add`, so a single algebraic +core covers doubling and the generic case: + +- distinct x: `(y2 - y1) / (zeta*x2 - zeta*x1) = zeta^-1 * s = zeta^2 * s`, + since `zeta^-1 = zeta^2` when `zeta^3 = 1`; +- doubling (with `A = 0`): `3*(zeta*x)^2 / (2*y) = zeta^2 * (3*x^2 / (2*y))`. + +Then in both branches `x3 |-> zeta^4 * s^2 - zeta*x1 - zeta*x2 = zeta * x3` +(using `zeta^4 = zeta`) and `y3 |-> zeta^3 * s * (x1 - x3) - y1 = y3`. + +The branch guards are preserved exactly: `zeta != 0` gives +`(zeta*x, y) = (0,0) <-> (x,y) = (0,0)`, and `zeta*x1 = zeta*x2 <-> x1 = x2`, +while `y` is untouched. The two junk-division cases (`y = 0`, `x1 = x2`) are +also consistent, because both sides produce `0/0 = 0`. + +Consequently `phi_add` requires no `Valid` hypothesis, no `IsElliptic`, and no +`b != 0`. Only `A = 0` and `zeta^3 = 1`. + +(Correction, from implementing it: the plan originally claimed `phi_add` would +depend on *no axioms whatsoever*. It does not. As implemented, every declaration +in the module reports `[propext, Classical.choice, Quot.sound]`, pulled in +through Mathlib's `Field` and division machinery. That is the same footprint the +existing group-law lemmas have, so nothing is lost, but the stronger claim was +wrong.) + +The one real constraint is that **`A = 0` is required**: for `A != 0`, +`y^2 = (zeta*x)^3 + A*(zeta*x) + B` fails. + +The slope-scaling step is a clean, hypothesis-free lemma: + +```lean +theorem zeta_inv {z : F} (hz : z ^ 3 = 1) : z⁻¹ = z ^ 2 := + inv_eq_of_mul_eq_one_right (by linear_combination hz) + +theorem div_zeta_mul {z : F} (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 +``` + +### 2. phi = [lambda] needs no cyclic-group machinery + +`IsCyclic`, `zpowers`, `Finite` and `Fintype` are all unnecessary. Mathlib has a +direct additive lemma that derives `Finite` internally from `Nat.card G = p` +plus primality. + +| Lemma | File | Signature | +| --- | --- | --- | +| `mem_multiples_of_prime_card` | `Mathlib/GroupTheory/SpecificGroups/Cyclic/Basic.lean:155` (`to_additive` of `mem_powers_of_prime_card`) | `{G} [AddGroup G] {p} [Fact p.Prime] (h : Nat.card G = p) {g g' : G} (hg : g != 0) : g' in AddSubmonoid.multiples g` | +| `AddSubmonoid.mem_multiples_iff` | `Mathlib/Algebra/Group/Submonoid/Membership.lean` | `x in AddSubmonoid.multiples z <-> exists n : Nat, n smul z = x` | +| `map_nsmul` | `Mathlib/Algebra/Group/Hom/Defs.lean` | `[AddMonoidHomClass F G H] (f : F) (n : Nat) (a : G) : f (n smul a) = n smul f a` | +| `nsmul_left_comm` | Mathlib (`Algebra/Group/Defs` area) | `(a : M) (m n : Nat) : n smul m smul a = m smul n smul a` | + +That yields a five-line capstone (compiled; `#print axioms` reports +`[propext, Classical.choice, Quot.sound]`): + +```lean +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] +``` + +Using `mem_multiples` (over `Nat`) rather than `mem_zmultiples` (over `Int`) is +what keeps `lam : Nat`, which is what `binNsmul` and `native_decide` want. + +Also verified as existing but **not needed**: `isAddCyclic_of_prime_card`, +`zmultiples_eq_top_of_prime_card`, `mem_zmultiples_of_prime_card`, +`AddMonoidHom.map_addCyclic`, `IsAddCyclic.exists_generator`. + +Threading `hHasse`: the `SWPoint` capstone takes `hcard : Nat.card (SWPoint E) = r` +as an ordinary argument, so the per-curve theorem just takes `hHasse` and feeds +it to `Pallas.card_eq hHasse`. No new machinery. + +### 3. The numeric obligations are mostly kernel `decide` + +Verified with `#print axioms` (all `[propext, Classical.choice, Quot.sound]`, +about 0.4s total with `set_option maxRecDepth 10000`): + +- `ZETA ^ 3 = 1`, `ZETA != 1`, `ZETA ^ 2 + ZETA + 1 = 0` (in `PallasBaseField` / + `VestaBaseField`): plain `by decide`. +- `LAMBDA < PALLAS_SCALAR_CARD`, `(LAMBDA : PallasScalarField) ^ 3 = 1`, + `(LAMBDA : PallasScalarField) ^ 2 + LAMBDA + 1 = 0`: plain `by decide`. + +This matters: because `zeta^3 = 1` is kernel-proved, the *definition* of `phiPt` +carries no `native_decide` axiom. + +The point spot-check `phiPt Gpt = LAMBDA smul Gpt` **must** be `native_decide`. +Kernel `decide` gets genuinely stuck (not merely slow): `binNsmul` is +well-founded recursion, so its equations do not reduce definitionally, and +`decide` bails at `instDecidableEqSWPoint`. This is the same reason the existing +`scalarCard_nsmul_Gpt` uses `native_decide`. Both the Pallas and Vesta +spot-checks pass by `native_decide`. + +Final axiom footprint of `Pallas.phi_eq_lambda_nsmul` (measured): the three +standard axioms, plus the pre-existing `PastaOrder` `native_decide` axioms, plus +one new one for the spot-check. No new *kind* of trust. + +### 4. Plausible for crypto-size fields + +Current API (plausible rev `86210d4`, Lean 4.30 era), confirmed by reading the +source: + +- `Plausible.Arbitrary a` (`Plausible/Arbitrary.lean`): just `arbitrary : Gen a`. +- `Plausible.Shrinkable a` (`Plausible/Shrinkable.lean`): `shrink : a -> List a`, + with a `{}` default of `fun _ => []`. +- `Plausible.SampleableExt a` (`Plausible/Sampleable.lean`): there is a + `@[default_instance] selfContained` built from `[Repr a] [Shrinkable a] + [Arbitrary a]`. So you write only `Arbitrary` and `Shrinkable`; `SampleableExt` + comes free. +- `Testable`'s forall-instance is `varTestable [SampleableExt a] ...`; the base + case is `decidableTestable [PrintableProp p] [Decidable p]`. The body + proposition **must be `Decidable`**. `PrintableProp` has a low-priority + catch-all instance, so it is never an obligation. + +**The size problem.** `Fin.Arbitrary`, `Nat.Arbitrary` and `BitVec.Arbitrary` all +clamp with `min (<- getSize) n`, and `getSize <= maxSize = 100`, so they produce +values in `[0, 100]`. Useless for a 254-bit field. There is no +`Arbitrary (ZMod n)` anywhere; Mathlib's `Mathlib/Testing/Plausible/Sampleable.lean` +adds only `Rat` and `PNat`. + +**But `Gen.choose Nat 0 (n-1)` is genuinely uniform for a 254-bit `n`.** Traced: +`BoundedRandom Nat -> rand (Fin _) -> randFin -> randNat` (`Init/Data/Random.lean:102`), +and `randNat` uses the Haskell `randomIvalInteger` algorithm: `randNatAux` +accumulates about nine successive 31-bit `StdGen` draws into a `k * 1000` +magnitude value before reducing mod `k`, giving under 1/1000 bias. It is not +limited to a single 31-bit draw, so no manual 64-bit composition is needed. + +The generator (compiled and tested; sampled values measured at `log2` = 253, 252, +250, 246, i.e. full width and independent of the `size` parameter): + +```lean +open Plausible + +instance instArbitraryZMod (n : ℕ) [NeZero n] : Arbitrary (ZMod n) where + arbitrary := do + let ⟨v, _⟩ ← Gen.choose Nat 0 (n - 1) (Nat.zero_le _) + return (v : ZMod n) + +instance instShrinkableZMod (n : ℕ) : Shrinkable (ZMod n) := {} -- no shrinking +``` + +`Repr (ZMod n)` already exists (`ZMod.repr`, `Mathlib/Data/ZMod/Defs.lean:157`), +so `SampleableExt` is inferred. Give the trivial `Shrinkable` deliberately: +halving the `ZMod.val` representative of a field element is algebraically +meaningless (it produces an unrelated element, not a simpler one) and just burns +time. Counterexamples then report as `(0 shrinks)` with the raw 254-bit witness. + +**`#test` versus the `plausible` tactic.** + +- `#test` is `macro tk:"#test " e:term : command => `(command| #eval%$tk Testable.check $e)` + (`Plausible/Testable.lean:620`). It is an `#eval`, so `lake build` runs it, and a + counterexample is a `Lean.throwError`, hence a build failure. That is the + behaviour we want. +- `#test` takes no `Configuration`. To set `numInst` or `randomSeed`, write + `#eval Plausible.Testable.check p { numInst := 25, randomSeed := some 42 }`. +- **Do not use the `plausible` tactic in library code.** It closes the goal with + `sorry` when it finds no counterexample (confirmed: `declaration uses 'sorry'`). + It is a disproof search, not a proof. Only `#test` and `#eval Testable.check` + are safe under the no-`sorry` policy. + +**Performance (measured, baseline import cost subtracted).** + +| Workload | Time | +| --- | --- | +| 200 interpreted 254-bit `SWPoint` scalar mults (`#eval`) | 10.3s, about 51ms each | +| `Testable.check`, 200 instances x 2 scalar mults | 24s (about 0.12s/instance) | +| The real GLV `#test`s, 25 instances each, 4-8 mults | 6.5s | +| All the `decide` field-level numeric facts | 0.4s | + +So roughly 50ms per interpreted 254-bit scalar multiplication. At the default +`numInst = 100`, a property with two scalar mults costs about 10s; three or four +such properties would add about a minute to every build of that module. Hence the +separate, non-default test library below. + +## Implementation plan + +### 1. `CompElliptic/CurveForms/Endomorphism.lean` (new, about 140 lines) + +Imports `CompElliptic.CurveForms.ShortWeierstrass` and +`Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic`. Reopens the namespace +`CompElliptic.CurveForms.ShortWeierstrass`: this is a *layer* on the short +Weierstrass form, not a new form, which is why it is not a new `CurveForms/` +form module. It must not go in `CurveOrder.lean`, which would be circular +(`CurveOrder` imports `ShortWeierstrass`). + +Three layers, mirroring `CurveOrder.lean`'s own structure. Every proof here is a +real proof: no `decide`, no `native_decide`. + +```lean +-- Section 1: pure finite-group theory (no curves) +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 +-- mem_multiples_of_prime_card + AddSubmonoid.mem_multiples_iff + map_nsmul + nsmul_left_comm + +-- Section 2: raw computable kernel (A = 0) +def phi (z : F) (p : F × F) : F × F := (z * p.1, p.2) +theorem zeta_ne_zero {z : F} (hz : z ^ 3 = 1) : z ≠ 0 +theorem zeta_inv {z : F} (hz : z ^ 3 = 1) : z⁻¹ = z ^ 2 +theorem div_zeta_mul {z : F} (hz : z ^ 3 = 1) (a b : F) : a / (z * b) = z ^ 2 * (a / b) +@[simp] theorem phi_origin (z : F) : phi z ((0, 0) : F × F) = (0, 0) +theorem phi_eq_origin_iff {z : F} (hz : z ^ 3 = 1) (p : F × F) : phi z p = (0, 0) ↔ p = (0, 0) +theorem onCurve_phi {b z : F} (hz : z ^ 3 = 1) {p} (h : OnCurve 0 b p) : OnCurve 0 b (phi z p) + -- linear_combination h - p.1 ^ 3 * hz +theorem valid_phi {b z : F} (hz : z ^ 3 = 1) {p} (h : Valid 0 b p) : Valid 0 b (phi z p) +theorem phi_addXY {z : F} (hz : z ^ 3 = 1) (lam x1 y1 x2 : F) : ... -- shared chord/tangent core +theorem phi_add {z : F} (hz : z ^ 3 = 1) (p q : F × F) : + phi z (add 0 p q) = add 0 (phi z p) (phi z q) -- no Valid hyps; zero axioms + +-- Section 3: SWPoint level +def SWPoint.phiPt {E : SWCurve F} (hA : E.A = 0) {z : F} (hz : z ^ 3 = 1) : SWPoint E → SWPoint E +theorem SWPoint.phiPt_add ... +def SWPoint.phiHom ... : SWPoint E →+ SWPoint E +theorem SWPoint.phiPt_eq_nsmul {E : SWCurve F} (hA : E.A = 0) {z : F} (hz : z ^ 3 = 1) + {r : ℕ} [Fact r.Prime] (hcard : Nat.card (SWPoint E) = r) + {G : SWPoint E} (hG : G ≠ 0) {lam : ℕ} (hspot : SWPoint.phiPt hA hz G = lam • G) + (P : SWPoint E) : SWPoint.phiPt hA hz P = lam • P + := endo_eq_nsmul_of_prime_card hcard (SWPoint.phiHom hA hz) hG hspot P +``` + +`phiPt` takes the two proofs as arguments; they are `Prop`s, hence erased, so +`native_decide` on `phiPt ... Gpt = LAMBDA smul Gpt` works (verified). + +The `phi_addXY` core needs exactly two `linear_combination`s (both verified): + +```lean +⟨by linear_combination (-(z * lam ^ 2)) * hz, + by linear_combination (lam ^ 3 * (1 + z ^ 3) - 2 * lam * x1 - lam * x2) * hz⟩ +``` + +Write `phi_add`'s branch walk with explicit `by_cases` plus `rw [if_pos/if_neg ...]` +(as `add_eq_addXY` does), **not** `split_ifs <;> simp_all`: the nested `ite`s blow +the recursion limit, exactly as the `add_neg` docstring already warns. + +### 2. `CompElliptic/Curves/PastaEndo.lean` (new, about 70 lines) + +Imports `CompElliptic.Curves.PastaOrder` and `CompElliptic.CurveForms.Endomorphism`. +Needs `set_option maxRecDepth 10000` for the `decide`s. + +```lean +namespace CompElliptic.Curves.Pasta.Pallas + +def ZETA : PallasBaseField := 0x2d33357cb532458ed3552a23a8554e5005270d29d19fc7d27b7fd22f0201b547 +def LAMBDA : ℕ := 0x397e65a7d7c1ad71aee24b27e308f0a61259527ec1d4752e619d1840af55f1b1 + +theorem A_zero : curve.A = 0 := rfl -- real proof +theorem ZETA_cube : ZETA ^ 3 = 1 := by decide -- kernel, axiom-clean +theorem ZETA_ne_one : ZETA ≠ 1 := by decide +theorem ZETA_quad : ZETA ^ 2 + ZETA + 1 = 0 := by decide -- primitivity +theorem LAMBDA_lt : LAMBDA < PALLAS_SCALAR_CARD := by decide +theorem LAMBDA_cube : (LAMBDA : PallasScalarField) ^ 3 = 1 := by decide +theorem LAMBDA_quad : (LAMBDA : PallasScalarField) ^ 2 + LAMBDA + 1 = 0 := by decide + +/-- The GLV endomorphism `φ(x, y) = (ζ·x, y)` on the Pallas group. -/ +def phi (P : SWPoint curve) : SWPoint curve := SWPoint.phiPt A_zero ZETA_cube P + +theorem phi_Gpt : phi Gpt = LAMBDA • Gpt := by native_decide -- the ONE new native_decide + +/-- **φ = [λ] on the whole Pallas group** (assuming Hasse's bound). -/ +theorem phi_eq_lambda_nsmul (hHasse : HasseBound curve) (P : SWPoint curve) : + phi P = LAMBDA • P := + SWPoint.phiPt_eq_nsmul A_zero ZETA_cube (card_eq hHasse) Gpt_ne_zero phi_Gpt P + +end CompElliptic.Curves.Pasta.Pallas +``` + +Vesta is identical with the *crossed* pair (the two fields swap roles): + +``` +Vesta.ZETA : VestaBaseField := 0x06819a58283e528e511db4d81cf70f5a0fed467d47c033af2aa9d2e050aa0e4f +Vesta.LAMBDA : ℕ := 0x12ccca834acdba712caad5dc57aab1b01d1f8bd237ad31491dad5ebdfdfe4ab9 +``` + +plus `Vesta.card_eq hHasse : Nat.card (SWPoint curve) = PALLAS_BASE_CARD` and the +existing `Fact (Nat.Prime PALLAS_BASE_CARD)`. + +Each `zeta` pairs with exactly ONE of the two `lambda`s, so the wrong pairing is +a live hazard. That is precisely why `phi_Gpt` is a checked fact rather than a +comment. (The constants above were computed and cross-checked numerically +against the group law before being written down; the Pallas pair matches the +`pasta_curves` `ENDO_BASE` / `ENDO_SCALAR` convention.) + +Optional corollaries, cheap (from `phi_eq_lambda_nsmul` + `LAMBDA_quad` + +`card_nsmul_eq_zero'`), and worth having because they are what GLV decomposition +actually consumes: + +- `phi (phi (phi P)) = P` (`φ³ = id`) +- `phi (phi P) + phi P + P = 0` (the `φ² + φ + 1 = 0` relation) + +If `lambda` should later live in `PallasScalarField` rather than `Nat`, the route +is `AddCommGroup.zmodModule : (∀ x : G, n • x = 0) → Module (ZMod n) G`, with the +hypothesis discharged by `card_nsmul_eq_zero'` plus `card_eq hHasse`. Deferring +that is fine: `lam : Nat` is what keeps `binNsmul` and `native_decide` fast. + +### 3. `CompElliptic.lean` (edit) + +Add `import CompElliptic.CurveForms.Endomorphism` and +`import CompElliptic.Curves.PastaEndo`. + +### 4. `CompEllipticTests/` (new test library) + +- `CompEllipticTests/Arbitrary.lean`: the `Arbitrary (ZMod n)` and + `Shrinkable (ZMod n)` instances from finding 4. Keep them inside the test + library so the global instance cannot leak into library elaboration. +- `CompEllipticTests/PastaEndo.lean`: the properties. + - Cheap (default `numInst`, microseconds): + `#test ∀ x : PallasBaseField, ZETA * (ZETA * (ZETA * x)) = x` and + `#test ∀ x : PallasBaseField, ZETA^2 * x + ZETA * x + x = 0`. + - Expensive (`numInst := 25`, fixed `randomSeed`): `phi` additive on random + group elements (`j.val • Gpt`, `k.val • Gpt`), and + `phi (k.val • Gpt) = LAMBDA • (k.val • Gpt)`. Both pass (6.5s combined). + - Uniform random group elements come free: `k : PallasScalarField` mapped to + `k.val • Gpt` is uniform over the whole prime-order group, at the cost of one + scalar mult. No point-decompression or sqrt generator is needed. +- `CompEllipticTests.lean`: root module importing both. + +Prefer field-level properties wherever possible (they are free) and reserve the +group-level ones for low `numInst`. + +### 5. `lakefile.lean` (edit) + +```lean +lean_lib CompEllipticTests -- deliberately NOT @[default_target] +``` + +No `require plausible` is needed: it is already a transitive dependency via +Mathlib and `import Plausible` resolves (verified). Leaving the test library off +the default target keeps plain `lake build`, and hence the existing `lean-action` +CI job, unaffected by the roughly 50ms-per-scalar-mult interpreted cost. + +### 6. `.github/workflows/ci.yml` (edit) + +Add a third job, "Property tests (plausible)", running `lake build CompEllipticTests` +after the Mathlib cache fetch, so the fast "Build (lake)" job stays fast and can +remain the required branch-protection check. + +### 7. `TODO.md` (edit) + +Add a GLV endomorphism entry under the short-Weierstrass form section, plus a +follow-on entry for **GLV scalar decomposition**: `k = k1 + k2 * lambda (mod r)` +with `|k1|, |k2| ~ sqrt(r)`, via the short lattice basis of +`{(a, b) : a + b*lambda = 0 (mod r)}`. That is a separate, mostly arithmetic job. +The balanced-basis constants are `native_decide`-checkable closed facts, and the +correctness statement `k • P = k1 • P + k2 • (phi P)` follows immediately from +`phi_eq_lambda_nsmul`. The bound on `|k1|, |k2|` is the only genuinely new work. + +## Dependency order + +1. `CurveForms/Endomorphism.lean` section 1 (group theory): independent, 5 lines. +2. Section 2, the raw kernel: independent of section 1. +3. Section 3, the `SWPoint` layer: needs sections 1 and 2. +4. `Curves/PastaEndo.lean`, Pallas: needs section 3 and the existing `PastaOrder`. +5. Vesta: a copy of step 4. +6. Test library, lakefile, CI: independent of steps 1-5 except for the constants. + +## Verification + +- `lake build` must stay green and `sorry`-free, and must keep its current speed + (the test library is not a default target). +- `lake build CompEllipticTests` runs the `#test`s; a counterexample throws and + fails the build. +- `#print axioms` on each new declaration: + - `phi_add` and the section-1 group-theory lemma: no new axioms. + - `ZETA_cube` and friends: the three standard axioms only. + - `Pallas.phi_eq_lambda_nsmul` / `Vesta.phi_eq_lambda_nsmul`: the three standard + axioms, the pre-existing `PastaOrder` `native_decide` axioms, and exactly one + new `native_decide` axiom (the `phi_Gpt` spot-check). + +## Risks and open items + +- **`precompileModules := true`** on the test library was not tested. It should let + the interpreter call native code for CompElliptic's own definitions, but the + inner loop is Mathlib's `ZMod` and `Field` instance dictionaries, which stay + interpreted, so expect only a modest gain. Measure before relying on it. +- `maxRecDepth 10000` sufficed for every `decide` tried. If a future `decide` on a + bigger literal chokes, `native_decide` is the fallback; it remains a per-curve + closed numeric fact, so it stays within the trust discipline. +- The placement of `endo_eq_nsmul_of_prime_card` is a style call. It is + form-agnostic, so it could live in `CurveOrder.lean`, but `CurveOrder` imports + `ShortWeierstrass`, so splitting the feature across two files would buy nothing. From 4da4cecd7660afe3a1e0643c0e2ac0feba41fb56 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 13 Jul 2026 10:53:15 +0200 Subject: [PATCH 3/6] feat(PastaEndo): the GLV endomorphism on Pallas and Vesta MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Instantiates `CurveForms/Endomorphism.lean` at the two Pasta curves. Both are `y² = x³ + 5`, so `A = 0` and the endomorphism applies, and `p ≡ q ≡ 1 mod 3`, so both fields have primitive cube roots of unity. The payoff is `phi_eq_lambda_nsmul`: `φ = [λ]` on the whole group, assuming Hasse's bound (via `card_eq`). Everything general was proved outright in `Endomorphism.lean`; only closed numeric facts remain here: * the field-level facts (`ζ³ = 1`, `ζ ≠ 1`, `ζ² + ζ + 1 = 0`, and the `λ` analogues) are kernel-`decide`d, so the *definition* of `φ` carries no `native_decide`; * the single point fact `φ G = [λ] G` (`phi_Gpt`) is `native_decide`d. Kernel `decide` cannot do it — not merely slowly, but at all: `binNsmul` is defined by well-founded recursion, so its equations do not reduce definitionally and `decide` gets stuck at `instDecidableEqSWPoint`. This is the same reason `PastaOrder.lean`'s `[order] G = 𝒪` witness is `native_decide`. `λ` is a `ℕ` (not a scalar-field element) so that `LAMBDA • _` is the fast `binNsmul` action, which is what makes the spot-check `native_decide`-able. The `(ζ, λ) `pairing is not free: each field has *two* primitive cube roots of unity, and a given `ζ` acts as `[λ]` for exactly one of the two candidates. The wrong pairing still yields a perfectly good endomorphism, just `[λ²]` rather than `[λ]` — a silent, wrong-by-a-cube-root bug. `phi_Gpt` is precisely the check that rules this out, which is why it is machine-checked rather than a comment; the other cube root was confirmed to fail it, so the check has teeth. The Pasta cycle crosses the two curves' constants (Pallas's `ζ` lives in `𝔽ₚ` and its `λ` in `𝔽_q`; Vesta's the other way round). Also adds `phi_phi_phi` / `SWPoint.phiPt_phiPt_phiPt` (`φ³ = id`) to `Endomorphism.lean`: purely computational from `ζ³ = 1`, so it needs neither the group order nor the `φ = [λ]` identification. Axiom footprint of `phi_eq_lambda_nsmul`: the standard three, the pre-existing `PastaOrder` `native_decide` axioms, and exactly one new one (`phi_Gpt`). No new *kind* of trust. --- CompElliptic.lean | 1 + CompElliptic/CurveForms/Endomorphism.lean | 14 +++ CompElliptic/Curves/PastaEndo.lean | 138 ++++++++++++++++++++++ 3 files changed, 153 insertions(+) create mode 100644 CompElliptic/Curves/PastaEndo.lean diff --git a/CompElliptic.lean b/CompElliptic.lean index 98853df..b7de770 100644 --- a/CompElliptic.lean +++ b/CompElliptic.lean @@ -17,3 +17,4 @@ import CompElliptic.CurveForms.Endomorphism import CompElliptic.CurveOrder import CompElliptic.Curves.Pasta import CompElliptic.Curves.PastaOrder +import CompElliptic.Curves.PastaEndo diff --git a/CompElliptic/CurveForms/Endomorphism.lean b/CompElliptic/CurveForms/Endomorphism.lean index 568a525..072eee9 100644 --- a/CompElliptic/CurveForms/Endomorphism.lean +++ b/CompElliptic/CurveForms/Endomorphism.lean @@ -109,6 +109,13 @@ theorem valid_phi {b : F} (hz : z ^ 3 = 1) {p : F × F} (h : Valid 0 b p) : · 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) : @@ -190,6 +197,13 @@ omit [DecidableEq F] in (P : SWPoint E) : ((SWPoint.phiPt hA hz P).x, (SWPoint.phiPt hA hz P).y) = phi z (P.x, P.y) := rfl +omit [DecidableEq F] in +/-- `φ³ = id` on `SWPoint E`. -/ +theorem SWPoint.phiPt_phiPt_phiPt {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) + (P : SWPoint E) : + SWPoint.phiPt hA hz (SWPoint.phiPt hA hz (SWPoint.phiPt hA hz P)) = P := + 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 SWPoint.phiPt_add {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) (P Q : SWPoint E) : SWPoint.phiPt hA hz (P + Q) = SWPoint.phiPt hA hz P + SWPoint.phiPt hA hz Q := by diff --git a/CompElliptic/Curves/PastaEndo.lean b/CompElliptic/Curves/PastaEndo.lean new file mode 100644 index 0000000..8d82fa0 --- /dev/null +++ b/CompElliptic/Curves/PastaEndo.lean @@ -0,0 +1,138 @@ +/- +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.Curves.PastaOrder +import CompElliptic.CurveForms.Endomorphism + +/-! +# The GLV endomorphism on the Pasta curves (Pallas and Vesta) + +Instantiates `CurveForms/Endomorphism.lean` at the two Pasta curves. Both are `y² = x³ + 5`, so +`A = 0` and the endomorphism `φ (x, y) = (ζ x, y)` applies, where `ζ` is a primitive cube root of +unity in the *base* field (`p ≡ q ≡ 1 mod 3`, so both fields have them). + +The payoff is `phi_eq_lambda_nsmul`: **`φ = [λ]` on the whole group**, where `λ` is a primitive cube +root of unity in the *scalar* field. Everything general was proved outright in +`Endomorphism.lean`; here only *closed numeric facts* remain, in the *Independently re-checkable +trust* style: + +* the field-level facts (`ζ³ = 1`, `ζ ≠ 1`, `ζ² + ζ + 1 = 0`, and the `λ` analogues) are + kernel-`decide`d, so the *definition* of `φ` carries no `native_decide`; +* the single point fact `φ G = [λ] G` is `native_decide`d. Kernel `decide` cannot do it — not + merely slowly, but at all: `binNsmul` is defined by well-founded recursion, so its equations do + not reduce definitionally and `decide` gets stuck at `instDecidableEqSWPoint`. This is the same + reason `PastaOrder.lean`'s `[order] G = 𝒪` witness is `native_decide`. + +**The (ζ, λ) pairing is not free.** Each field has *two* primitive cube roots of unity, and a given +`ζ` acts as `[λ]` for exactly one of the two candidate `λ`s (the other `ζ` pairs with the other +`λ`). Pairing them wrongly gives a `φ` that is still a perfectly good endomorphism, just equal to +`[λ²]` rather than `[λ]` — a silent, wrong-by-a-cube-root bug. `phi_Gpt` is precisely the check +that rules this out, which is why it is a machine-checked fact and not a comment. + +Note the Pasta cycle shows up here too: Pallas's `ζ` lives in `𝔽ₚ` and its `λ` in `𝔽_q`, while +Vesta's `ζ` lives in `𝔽_q` and its `λ` in `𝔽ₚ` — so the two curves' constants are *crossed*. +-/ + +set_option maxRecDepth 10000 + +namespace CompElliptic.Curves.Pasta + +open CompElliptic.CurveForms.ShortWeierstrass CompElliptic.CurveOrder CompElliptic.Fields.Pasta + +namespace Pallas + +/-- A primitive cube root of unity in the Pallas *base* field `𝔽ₚ`; `φ` scales `x` by it. -/ +def ZETA : PallasBaseField := + 0x2d33357cb532458ed3552a23a8554e5005270d29d19fc7d27b7fd22f0201b547 + +/-- The matching primitive cube root of unity in the Pallas *scalar* field `𝔽_q`, as a `ℕ` (so that +`LAMBDA • _` is the fast `binNsmul` action). `φ` acts as `[LAMBDA]` — pinned by `phi_Gpt`. -/ +def LAMBDA : ℕ := + 0x397e65a7d7c1ad71aee24b27e308f0a61259527ec1d4752e619d1840af55f1b1 + +/-- Pallas is `y² = x³ + 5`, so `A = 0` — the hypothesis the endomorphism needs. -/ +theorem A_zero : curve.A = 0 := rfl + +theorem ZETA_cube : ZETA ^ 3 = 1 := by decide + +/-- `ζ ≠ 1`, so `φ` is not the identity map (together with `ZETA_cube`, `ζ` is *primitive*). -/ +theorem ZETA_ne_one : ZETA ≠ 1 := by decide + +/-- Primitivity in the form actually used downstream: `ζ² + ζ + 1 = 0`. -/ +theorem ZETA_quad : ZETA ^ 2 + ZETA + 1 = 0 := by decide + +/-- `λ` is a canonical (reduced) representative of its scalar-field class. -/ +theorem LAMBDA_lt : LAMBDA < PALLAS_SCALAR_CARD := by decide + +theorem LAMBDA_cube : (LAMBDA : PallasScalarField) ^ 3 = 1 := by decide + +/-- `λ² + λ + 1 = 0`: the relation `φ² + φ + 1 = 0` that GLV decomposition rests on. -/ +theorem LAMBDA_quad : (LAMBDA : PallasScalarField) ^ 2 + LAMBDA + 1 = 0 := by decide + +/-- **The GLV endomorphism on Pallas**: `φ (x, y) = (ζ x, y)`. -/ +def phi (P : SWPoint curve) : SWPoint curve := SWPoint.phiPt A_zero ZETA_cube P + +/-- The spot-check that pins the `(ζ, λ)` pairing: `φ G = [λ] G` on the test point `G = (-1, 2)`. + +This is the *one* closed fact the whole `φ = [λ]` theorem rests on beyond the general proofs, and +it is exactly what would fail if `ζ` were paired with the wrong cube root of unity. -/ +theorem phi_Gpt : phi Gpt = LAMBDA • Gpt := by native_decide + +/-- **`φ = [λ]` on the whole Pallas group** (assuming Hasse's bound). + +`φ` is an endomorphism (proved outright, `SWPoint.phiHom`); the group has prime order +`PALLAS_SCALAR_CARD` (`Pallas.card_eq`, the one place Hasse is assumed); and `φ G = [λ] G` for the +non-identity `G` (`phi_Gpt`). By `endo_eq_nsmul_of_prime_card`, `φ` is `[λ]` everywhere. -/ +theorem phi_eq_lambda_nsmul (hHasse : HasseBound curve) (P : SWPoint curve) : + phi P = LAMBDA • P := + SWPoint.phiPt_eq_nsmul A_zero ZETA_cube (card_eq hHasse) Gpt_ne_zero phi_Gpt P + +end Pallas + +namespace Vesta + +/-- A primitive cube root of unity in the Vesta *base* field `𝔽_q` (`= PallasScalarField`; the Pasta +cycle crosses the two curves' constants). -/ +def ZETA : VestaBaseField := + 0x06819a58283e528e511db4d81cf70f5a0fed467d47c033af2aa9d2e050aa0e4f + +/-- The matching primitive cube root of unity in the Vesta *scalar* field `𝔽ₚ`, as a `ℕ`. -/ +def LAMBDA : ℕ := + 0x12ccca834acdba712caad5dc57aab1b01d1f8bd237ad31491dad5ebdfdfe4ab9 + +/-- Vesta is `y² = x³ + 5`, so `A = 0`. -/ +theorem A_zero : curve.A = 0 := rfl + +theorem ZETA_cube : ZETA ^ 3 = 1 := by decide + +/-- `ζ ≠ 1`, so `φ` is not the identity map. -/ +theorem ZETA_ne_one : ZETA ≠ 1 := by decide + +/-- Primitivity: `ζ² + ζ + 1 = 0`. -/ +theorem ZETA_quad : ZETA ^ 2 + ZETA + 1 = 0 := by decide + +/-- `λ` is a canonical (reduced) representative of its scalar-field class. -/ +theorem LAMBDA_lt : LAMBDA < PALLAS_BASE_CARD := by decide + +theorem LAMBDA_cube : (LAMBDA : VestaScalarField) ^ 3 = 1 := by decide + +/-- `λ² + λ + 1 = 0`. -/ +theorem LAMBDA_quad : (LAMBDA : VestaScalarField) ^ 2 + LAMBDA + 1 = 0 := by decide + +/-- **The GLV endomorphism on Vesta**: `φ (x, y) = (ζ x, y)`. -/ +def phi (P : SWPoint curve) : SWPoint curve := SWPoint.phiPt A_zero ZETA_cube P + +/-- The spot-check pinning the `(ζ, λ)` pairing on Vesta: `φ G = [λ] G`. -/ +theorem phi_Gpt : phi Gpt = LAMBDA • Gpt := by native_decide + +/-- **`φ = [λ]` on the whole Vesta group** (assuming Hasse's bound). -/ +theorem phi_eq_lambda_nsmul (hHasse : HasseBound curve) (P : SWPoint curve) : + phi P = LAMBDA • P := + SWPoint.phiPt_eq_nsmul A_zero ZETA_cube (card_eq hHasse) Gpt_ne_zero phi_Gpt P + +end Vesta + +end CompElliptic.Curves.Pasta From 4829d52642b6f99c6319a92f0fac040a3d400b7d Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 13 Jul 2026 10:53:16 +0200 Subject: [PATCH 4/6] docs(TODO): record the GLV endomorphism, and what remains MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The form-level endomorphism and the Pallas/Vesta instantiation are done; the Plausible property-test harness and the GLV scalar decomposition are not. Notes the constraints found along the way (`A = 0` is essential; the `(ζ, λ)` pairing must be checked, not assumed; Plausible's stock generators are useless at 254 bits and its tactic form emits `sorry`). --- TODO.md | 41 +++++++++++++++++++++++++++++++++ design/glv-endomorphism-plan.md | 9 ++++---- 2 files changed, 46 insertions(+), 4 deletions(-) diff --git a/TODO.md b/TODO.md index 943b4ef..775e7d5 100644 --- a/TODO.md +++ b/TODO.md @@ -143,6 +143,47 @@ types + transport) has been consolidated into these and removed. - [ ] Small-cofactor variant (`#G = h·r` for known `h`): a straightforward Layer-1 generalization, deferred. Needed for Jubjub (cofactor 8), which also needs the Edwards form first. +## CompElliptic — GLV endomorphism (`CurveForms/Endomorphism.lean`, `Curves/PastaEndo.lean`) + +Design notes and the wider plan: [`design/glv-endomorphism-plan.md`](design/glv-endomorphism-plan.md). + +- [x] The endomorphism, form-level (`CurveForms/Endomorphism.lean`), in three layers mirroring + `CurveOrder.lean`. (1) Pure finite-group theory: `endo_eq_nsmul_of_prime_card` — an endomorphism + of a group of prime order `r` sending one non-identity `g` to `[lam] g` is `[lam]` everywhere, + via Mathlib's `mem_multiples_of_prime_card` (which derives `Finite` from `Nat.card G = r` plus + primality, so no `IsCyclic` / `zpowers` machinery is needed). This is what reduces `φ = [λ]` on + the whole group to one closed spot-checkable fact. (2) Raw kernel: `phi z (x, y) = (z x, y)`, + with `phi_add` (commutes with `add`), `onCurve_phi`, `valid_phi`, `phi_phi_phi` (`φ³ = id`). + `phi_add` needs **no** hypotheses beyond `ζ³ = 1` — not `Valid`, not `IsElliptic`, not `B ≠ 0`: + the slope scales by `ζ²` in *both* branches, the branch guards are preserved (`ζ ≠ 0`), and the + degenerate divisions agree (`0/0 = 0` on both sides). (3) `SWPoint.phiPt` / `phiHom` (`φ` as an + `AddMonoidHom`) and the capstone `SWPoint.phiPt_eq_nsmul`. No `sorry`, no `decide` / + `native_decide`; standard axioms only. **`A = 0` is essential** (for `A ≠ 0`, + `y² = (ζx)³ + A(ζx) + B` fails) — fine for Pasta and every curve GLV is used on. +- [x] Pallas/Vesta constants and `φ = [λ]` (`Curves/PastaEndo.lean`): `ZETA` (base field) and + `LAMBDA` (scalar field, as `ℕ` so `LAMBDA • _` is the fast `binNsmul`), with the field-level + facts (`ζ³ = 1`, `ζ ≠ 1`, `ζ² + ζ + 1 = 0`, and the `λ` analogues) kernel-`decide`d — so the + *definition* of `φ` carries no `native_decide` — and the single point fact `φ G = [λ] G` + (`phi_Gpt`) by `native_decide`. Capstone `phi_eq_lambda_nsmul` (assuming `HasseBound`, via + `card_eq`). The `(ζ, λ)` pairing is *not* free: each field has two primitive cube roots and a + given `ζ` acts as `[λ]` for exactly one of them, the wrong pairing yielding `[λ²]` — a silent + wrong-by-a-cube-root bug that `phi_Gpt` is precisely there to rule out (verified to have teeth: + the other cube root provably fails it). Pasta's cycle crosses the two curves' constants. +- [ ] Property-based tests (Plausible; already a transitive dep via Mathlib, so no new dependency). + Needs a uniform `Arbitrary (ZMod n)` built on `Gen.choose` — the stock generators cap at ~100, + useless at 254 bits — and random group elements come free as `k.val • Gpt`. Put them in a + separate `lean_lib CompEllipticTests` that is **not** a default target, plus its own CI job: an + interpreted 254-bit scalar mult costs ≈ 50 ms, so a group-level property at the default 100 + instances is ≈ 10 s and would slow every build. NB the `plausible` *tactic* closes goals with + `sorry` when it finds no counterexample, so only `#test` / `#eval Testable.check` are usable. +- [ ] GLV scalar decomposition: `k ≡ k₁ + k₂·λ (mod r)` with `|k₁|, |k₂| ≈ √r`, via the short + lattice basis of `{(a, b) : a + bλ ≡ 0 mod r}`. The balanced-basis constants are + `native_decide`-checkable closed facts, and the correctness statement + `k • P = k₁ • P + k₂ • (φ P)` follows immediately from `phi_eq_lambda_nsmul`. The bound on + `|k₁|, |k₂|` is the only genuinely new work. +- [ ] The `φ² + φ + 1 = 0` relation on points (from `phi_eq_lambda_nsmul` + `LAMBDA_quad` + + `card_nsmul_eq_zero'`), if the decomposition proofs want it in that form. + ## CompElliptic — other forms & the group abstraction (later) - [x] Coordinate-system abstraction (`CoordinateSystem.lean`): carrier + `Valid` + `Rel` + ops → diff --git a/design/glv-endomorphism-plan.md b/design/glv-endomorphism-plan.md index fa95269..df6257e 100644 --- a/design/glv-endomorphism-plan.md +++ b/design/glv-endomorphism-plan.md @@ -313,10 +313,11 @@ plus `Vesta.card_eq hHasse : Nat.card (SWPoint curve) = PALLAS_BASE_CARD` and th existing `Fact (Nat.Prime PALLAS_BASE_CARD)`. Each `zeta` pairs with exactly ONE of the two `lambda`s, so the wrong pairing is -a live hazard. That is precisely why `phi_Gpt` is a checked fact rather than a -comment. (The constants above were computed and cross-checked numerically -against the group law before being written down; the Pallas pair matches the -`pasta_curves` `ENDO_BASE` / `ENDO_SCALAR` convention.) +a live hazard: the wrong pairing still gives a perfectly good endomorphism, just +`[lambda^2]` rather than `[lambda]`. That is precisely why `phi_Gpt` is a checked +fact rather than a comment. The constants were computed and cross-checked +numerically against the group law before being written down, and the check was +confirmed to have teeth (the other cube root of unity provably fails `phi_Gpt`). Optional corollaries, cheap (from `phi_eq_lambda_nsmul` + `LAMBDA_quad` + `card_nsmul_eq_zero'`), and worth having because they are what GLV decomposition From eb10b345e138d868de0f62b2e0591eb95aa01b08 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 13 Jul 2026 11:25:43 +0200 Subject: [PATCH 5/6] refactor(Endomorphism): follow the repo's module, namespace, and check conventions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review pass against the conventions actually used on main. Move `CurveForms/Endomorphism.lean` to `Endomorphism.lean`, namespace `CompElliptic.Endomorphism`. TODO.md states that `CurveForms/` holds one module per curve *form*, and that namespaces mirror the directory path throughout; the endomorphism is neither a curve form nor was its namespace (`CompElliptic.CurveForms.ShortWeierstrass`) mirroring its path. `CurveOrder.lean` is the precedent for exactly this shape of module — a cross-cutting layer over the short-Weierstrass form, at top level, with its own namespace, opening `ShortWeierstrass`, split into "pure group theory" and "curve" layers, and instantiated by a `Curves/Pasta*.lean` — so follow it. The layer-3 declarations lose their `SWPoint.` prefix accordingly (it would have created a bogus `CompElliptic.Endomorphism.SWPoint` namespace). Drop `set_option maxRecDepth 10000` from `PastaEndo.lean`: it is not needed (every `decide` there compiles without it), and main uses no `set_option` anywhere. Add the `native_decide` sanity checks the concrete-curve modules all carry (`Curves/Pasta.lean` has 14, `Fields/Pasta.lean` 6; `PastaEndo.lean` had none): `φ` fixes `𝒪`, moves `G`, cubes to the identity, is additive on a concrete pair, and — the one that matters — is *not* `[λ²]`. That last check is what gives `phi_Gpt` its teeth: `λ²` is the other primitive cube root of unity in the scalar field, and pairing `ζ` with it would yield a well-typed, perfectly valid endomorphism that is simply the wrong one. It is now machine-checked, not merely asserted. Add the missing docstrings (`ZETA_cube`, `LAMBDA_cube` on both curves, `phiPt_coords`). --- CompElliptic.lean | 2 +- CompElliptic/Curves/PastaEndo.lean | 50 +++++++++++++++---- .../{CurveForms => }/Endomorphism.lean | 42 +++++++++------- 3 files changed, 64 insertions(+), 30 deletions(-) rename CompElliptic/{CurveForms => }/Endomorphism.lean (86%) diff --git a/CompElliptic.lean b/CompElliptic.lean index b7de770..19cd436 100644 --- a/CompElliptic.lean +++ b/CompElliptic.lean @@ -13,7 +13,7 @@ import CompElliptic.Encodings.Pasta import CompElliptic.Fields.Pasta import CompElliptic.Fields.Sqrt import CompElliptic.CurveForms.ShortWeierstrass -import CompElliptic.CurveForms.Endomorphism +import CompElliptic.Endomorphism import CompElliptic.CurveOrder import CompElliptic.Curves.Pasta import CompElliptic.Curves.PastaOrder diff --git a/CompElliptic/Curves/PastaEndo.lean b/CompElliptic/Curves/PastaEndo.lean index 8d82fa0..320ccdc 100644 --- a/CompElliptic/Curves/PastaEndo.lean +++ b/CompElliptic/Curves/PastaEndo.lean @@ -5,12 +5,12 @@ as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood -/ import CompElliptic.Curves.PastaOrder -import CompElliptic.CurveForms.Endomorphism +import CompElliptic.Endomorphism /-! # The GLV endomorphism on the Pasta curves (Pallas and Vesta) -Instantiates `CurveForms/Endomorphism.lean` at the two Pasta curves. Both are `y² = x³ + 5`, so +Instantiates `Endomorphism.lean` at the two Pasta curves. Both are `y² = x³ + 5`, so `A = 0` and the endomorphism `φ (x, y) = (ζ x, y)` applies, where `ζ` is a primitive cube root of unity in the *base* field (`p ≡ q ≡ 1 mod 3`, so both fields have them). @@ -36,11 +36,10 @@ Note the Pasta cycle shows up here too: Pallas's `ζ` lives in `𝔽ₚ` and its Vesta's `ζ` lives in `𝔽_q` and its `λ` in `𝔽ₚ` — so the two curves' constants are *crossed*. -/ -set_option maxRecDepth 10000 - namespace CompElliptic.Curves.Pasta -open CompElliptic.CurveForms.ShortWeierstrass CompElliptic.CurveOrder CompElliptic.Fields.Pasta +open CompElliptic.CurveForms.ShortWeierstrass CompElliptic.CurveOrder + CompElliptic.Endomorphism CompElliptic.Fields.Pasta namespace Pallas @@ -56,6 +55,8 @@ def LAMBDA : ℕ := /-- Pallas is `y² = x³ + 5`, so `A = 0` — the hypothesis the endomorphism needs. -/ theorem A_zero : curve.A = 0 := rfl +/-- `ζ` is a cube root of unity — the hypothesis `φ` is built on. Kernel-`decide`d, so the +*definition* of `φ` carries no `native_decide`. -/ theorem ZETA_cube : ZETA ^ 3 = 1 := by decide /-- `ζ ≠ 1`, so `φ` is not the identity map (together with `ZETA_cube`, `ζ` is *primitive*). -/ @@ -67,13 +68,15 @@ theorem ZETA_quad : ZETA ^ 2 + ZETA + 1 = 0 := by decide /-- `λ` is a canonical (reduced) representative of its scalar-field class. -/ theorem LAMBDA_lt : LAMBDA < PALLAS_SCALAR_CARD := by decide +/-- `λ` is a cube root of unity in the scalar field — the scalar-side counterpart of +`ZETA_cube`, and the reason `φ³ = id` is consistent with `φ = [λ]`. -/ theorem LAMBDA_cube : (LAMBDA : PallasScalarField) ^ 3 = 1 := by decide /-- `λ² + λ + 1 = 0`: the relation `φ² + φ + 1 = 0` that GLV decomposition rests on. -/ theorem LAMBDA_quad : (LAMBDA : PallasScalarField) ^ 2 + LAMBDA + 1 = 0 := by decide /-- **The GLV endomorphism on Pallas**: `φ (x, y) = (ζ x, y)`. -/ -def phi (P : SWPoint curve) : SWPoint curve := SWPoint.phiPt A_zero ZETA_cube P +def phi (P : SWPoint curve) : SWPoint curve := phiPt A_zero ZETA_cube P /-- The spot-check that pins the `(ζ, λ)` pairing: `φ G = [λ] G` on the test point `G = (-1, 2)`. @@ -83,12 +86,29 @@ theorem phi_Gpt : phi Gpt = LAMBDA • Gpt := by native_decide /-- **`φ = [λ]` on the whole Pallas group** (assuming Hasse's bound). -`φ` is an endomorphism (proved outright, `SWPoint.phiHom`); the group has prime order +`φ` is an endomorphism (proved outright, `phiHom`); the group has prime order `PALLAS_SCALAR_CARD` (`Pallas.card_eq`, the one place Hasse is assumed); and `φ G = [λ] G` for the non-identity `G` (`phi_Gpt`). By `endo_eq_nsmul_of_prime_card`, `φ` is `[λ]` everywhere. -/ theorem phi_eq_lambda_nsmul (hHasse : HasseBound curve) (P : SWPoint curve) : phi P = LAMBDA • P := - SWPoint.phiPt_eq_nsmul A_zero ZETA_cube (card_eq hHasse) Gpt_ne_zero phi_Gpt P + phiPt_eq_nsmul A_zero ZETA_cube (card_eq hHasse) Gpt_ne_zero phi_Gpt P + +-- `φ` fixes `𝒪`. +example : phi 0 = 0 := by native_decide + +-- `φ` is nontrivial: it moves `G` (it is not the identity map, cf. `ZETA_ne_one`). +example : phi Gpt ≠ Gpt := by native_decide + +-- `φ³ = id` on `G` (the computational shadow of `phi_phi_phi`). +example : phi (phi (phi Gpt)) = Gpt := by native_decide + +-- `φ` is additive on a concrete pair (the computational shadow of `phi_add`). +example : phi (Gpt + (2 : ℕ) • Gpt) = phi Gpt + phi ((2 : ℕ) • Gpt) := by native_decide + +-- **The `(ζ, λ)` pairing has teeth.** `λ²` is the *other* primitive cube root of unity in `𝔽_q`, +-- and `φ` is emphatically not `[λ²]`. Pairing `ζ` with it would give a well-typed, perfectly valid +-- endomorphism that is simply the wrong one — which is what `phi_Gpt` exists to rule out. +example : phi Gpt ≠ (LAMBDA ^ 2 % PALLAS_SCALAR_CARD) • Gpt := by native_decide end Pallas @@ -106,6 +126,7 @@ def LAMBDA : ℕ := /-- Vesta is `y² = x³ + 5`, so `A = 0`. -/ theorem A_zero : curve.A = 0 := rfl +/-- `ζ` is a cube root of unity — the hypothesis `φ` is built on. -/ theorem ZETA_cube : ZETA ^ 3 = 1 := by decide /-- `ζ ≠ 1`, so `φ` is not the identity map. -/ @@ -117,13 +138,14 @@ theorem ZETA_quad : ZETA ^ 2 + ZETA + 1 = 0 := by decide /-- `λ` is a canonical (reduced) representative of its scalar-field class. -/ theorem LAMBDA_lt : LAMBDA < PALLAS_BASE_CARD := by decide +/-- `λ` is a cube root of unity in the scalar field. -/ theorem LAMBDA_cube : (LAMBDA : VestaScalarField) ^ 3 = 1 := by decide /-- `λ² + λ + 1 = 0`. -/ theorem LAMBDA_quad : (LAMBDA : VestaScalarField) ^ 2 + LAMBDA + 1 = 0 := by decide /-- **The GLV endomorphism on Vesta**: `φ (x, y) = (ζ x, y)`. -/ -def phi (P : SWPoint curve) : SWPoint curve := SWPoint.phiPt A_zero ZETA_cube P +def phi (P : SWPoint curve) : SWPoint curve := phiPt A_zero ZETA_cube P /-- The spot-check pinning the `(ζ, λ)` pairing on Vesta: `φ G = [λ] G`. -/ theorem phi_Gpt : phi Gpt = LAMBDA • Gpt := by native_decide @@ -131,7 +153,15 @@ theorem phi_Gpt : phi Gpt = LAMBDA • Gpt := by native_decide /-- **`φ = [λ]` on the whole Vesta group** (assuming Hasse's bound). -/ theorem phi_eq_lambda_nsmul (hHasse : HasseBound curve) (P : SWPoint curve) : phi P = LAMBDA • P := - SWPoint.phiPt_eq_nsmul A_zero ZETA_cube (card_eq hHasse) Gpt_ne_zero phi_Gpt P + phiPt_eq_nsmul A_zero ZETA_cube (card_eq hHasse) Gpt_ne_zero phi_Gpt P + +-- As for Pallas: `φ` fixes `𝒪`, is nontrivial, cubes to the identity, is additive, and is *not* +-- `[λ²]` (the other primitive cube root of unity in the scalar field). +example : phi 0 = 0 := by native_decide +example : phi Gpt ≠ Gpt := by native_decide +example : phi (phi (phi Gpt)) = Gpt := by native_decide +example : phi (Gpt + (2 : ℕ) • Gpt) = phi Gpt + phi ((2 : ℕ) • Gpt) := by native_decide +example : phi Gpt ≠ (LAMBDA ^ 2 % PALLAS_BASE_CARD) • Gpt := by native_decide end Vesta diff --git a/CompElliptic/CurveForms/Endomorphism.lean b/CompElliptic/Endomorphism.lean similarity index 86% rename from CompElliptic/CurveForms/Endomorphism.lean rename to CompElliptic/Endomorphism.lean index 072eee9..ae16fc1 100644 --- a/CompElliptic/CurveForms/Endomorphism.lean +++ b/CompElliptic/Endomorphism.lean @@ -26,8 +26,8 @@ Three layers: (`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** — `SWPoint.phiPt` / `SWPoint.phiHom` (`φ` as an `AddMonoidHom`), and - `SWPoint.phiPt_eq_nsmul`, which combines layers 1 and 2: given the group order (a prime `r`) and +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 @@ -37,7 +37,9 @@ Everything here is a real proof; the numeric facts (`ζ³ = 1`, and the spot-che closed facts and live in the concrete-curve modules. -/ -namespace CompElliptic.CurveForms.ShortWeierstrass +namespace CompElliptic.Endomorphism + +open CompElliptic.CurveForms.ShortWeierstrass /-! ## Layer 1: an endomorphism of a prime-order group is multiplication by a scalar @@ -144,9 +146,9 @@ theorem phi_add (hz : z ^ 3 = 1) (p q : F × F) : phi z (add 0 p q) = 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, zero_add, phi_origin, zero_add] + · rw [hp0, CurveForms.ShortWeierstrass.zero_add, phi_origin, CurveForms.ShortWeierstrass.zero_add] by_cases hq0 : q = (0, 0) - · rw [hq0, add_zero, phi_origin, add_zero] + · rw [hq0, CurveForms.ShortWeierstrass.add_zero, phi_origin, CurveForms.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). @@ -185,7 +187,7 @@ theorem phi_add (hz : z ^ 3 = 1) (p q : F × F) : /-- `φ` 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 SWPoint.phiPt {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) (P : SWPoint E) : SWPoint E := +def phiPt {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) (P : SWPoint E) : SWPoint E := ⟨z * P.x, P.y, by have h : Valid 0 E.B (P.x, P.y) := hA ▸ P.onCurve have h' : Valid 0 E.B (phi z (P.x, P.y)) := valid_phi hz h @@ -193,20 +195,22 @@ def SWPoint.phiPt {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) (P : SWPoint E exact h'⟩ omit [DecidableEq F] in -@[simp] theorem SWPoint.phiPt_coords {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) +/-- 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 : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) (P : SWPoint E) : - ((SWPoint.phiPt hA hz P).x, (SWPoint.phiPt hA hz P).y) = phi z (P.x, P.y) := rfl + ((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 SWPoint.phiPt_phiPt_phiPt {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) +theorem phiPt_phiPt_phiPt {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) (P : SWPoint E) : - SWPoint.phiPt hA hz (SWPoint.phiPt hA hz (SWPoint.phiPt hA hz P)) = P := + phiPt hA hz (phiPt hA hz (phiPt hA hz P)) = P := 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 SWPoint.phiPt_add {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) (P Q : SWPoint E) : - SWPoint.phiPt hA hz (P + Q) = SWPoint.phiPt hA hz P + SWPoint.phiPt hA hz Q := by +theorem phiPt_add {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) (P Q : SWPoint E) : + phiPt hA hz (P + Q) = phiPt hA hz P + phiPt hA hz Q := by refine SWPoint.ext_pair ?_ show phi z (add E.A (P.x, P.y) (Q.x, Q.y)) = add E.A (phi z (P.x, P.y)) (phi z (Q.x, Q.y)) @@ -214,18 +218,18 @@ theorem SWPoint.phiPt_add {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) (P Q : exact phi_add hz _ _ /-- `φ` as an `AddMonoidHom` on `SWPoint E` — the input to `endo_eq_nsmul_of_prime_card`. -/ -def SWPoint.phiHom {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) : SWPoint E →+ SWPoint E := - AddMonoidHom.mk' (SWPoint.phiPt hA hz) (SWPoint.phiPt_add hA hz) +def phiHom {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) : SWPoint E →+ 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 SWPoint.phiPt_eq_nsmul {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) +theorem phiPt_eq_nsmul {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) {r : ℕ} [Fact r.Prime] (hcard : Nat.card (SWPoint E) = r) - {G : SWPoint E} (hG : G ≠ 0) {lam : ℕ} (hspot : SWPoint.phiPt hA hz G = lam • G) - (P : SWPoint E) : SWPoint.phiPt hA hz P = lam • P := - endo_eq_nsmul_of_prime_card hcard (SWPoint.phiHom hA hz) hG hspot P + {G : SWPoint E} (hG : G ≠ 0) {lam : ℕ} (hspot : phiPt hA hz G = lam • G) + (P : SWPoint E) : phiPt hA hz P = lam • P := + endo_eq_nsmul_of_prime_card hcard (phiHom hA hz) hG hspot P -end CompElliptic.CurveForms.ShortWeierstrass +end CompElliptic.Endomorphism From 24ed30d14b00722a1b44e77a2d9d41f56b69ae80 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 13 Jul 2026 17:42:26 +0200 Subject: [PATCH 6/6] style(Endomorphism): qualify borrowed names instead of opening leaf namespaces MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Every name borrowed from another module now carries its source namespace at the use site, so where each definition comes from is readable without chasing imports: `ShortWeierstrass.add`, `ShortWeierstrass.SWPoint`, `CurveOrder.HasseBound`, `Endomorphism.phiPt`, `Fields.Pasta.PallasBaseField`. Only `CompElliptic.CurveForms` is opened, never the `ShortWeierstrass` leaf. That keeps the provenance visible while stopping the short-Weierstrass names from expanding to a full `CurveForms.ShortWeierstrass.…` path on every line (which pushed `phiHom`'s signature past 170 characters). `Curves/Pasta.lean` and `Curves/PastaOrder.lean` still open the leaf namespace; they are left alone here to keep this PR to the GLV work. No change to what is proved: `lake build` is green and the axiom footprints are unchanged (`phi_add` on the standard three; `phi_eq_lambda_nsmul` on those plus the pre-existing `PastaOrder` `native_decide` axioms plus `phi_Gpt`). --- CompElliptic/Curves/PastaEndo.lean | 45 +++++++++++++---------- CompElliptic/Endomorphism.lean | 59 ++++++++++++++++-------------- 2 files changed, 57 insertions(+), 47 deletions(-) diff --git a/CompElliptic/Curves/PastaEndo.lean b/CompElliptic/Curves/PastaEndo.lean index 320ccdc..ee30c74 100644 --- a/CompElliptic/Curves/PastaEndo.lean +++ b/CompElliptic/Curves/PastaEndo.lean @@ -38,13 +38,16 @@ Vesta's `ζ` lives in `𝔽_q` and its `λ` in `𝔽ₚ` — so the two curves' namespace CompElliptic.Curves.Pasta -open CompElliptic.CurveForms.ShortWeierstrass CompElliptic.CurveOrder - CompElliptic.Endomorphism CompElliptic.Fields.Pasta +-- No blanket `open`s: each borrowed name is written with its source namespace at the use site +-- (`ShortWeierstrass.…`, `CurveOrder.…`, `Endomorphism.…`, `Fields.Pasta.…`), so where every +-- definition comes from is visible without chasing imports. Only `CurveForms` is opened, so the +-- short-Weierstrass leaf still reads `ShortWeierstrass.X` rather than a full path. +open CompElliptic.CurveForms namespace Pallas /-- A primitive cube root of unity in the Pallas *base* field `𝔽ₚ`; `φ` scales `x` by it. -/ -def ZETA : PallasBaseField := +def ZETA : Fields.Pasta.PallasBaseField := 0x2d33357cb532458ed3552a23a8554e5005270d29d19fc7d27b7fd22f0201b547 /-- The matching primitive cube root of unity in the Pallas *scalar* field `𝔽_q`, as a `ℕ` (so that @@ -66,17 +69,18 @@ theorem ZETA_ne_one : ZETA ≠ 1 := by decide theorem ZETA_quad : ZETA ^ 2 + ZETA + 1 = 0 := by decide /-- `λ` is a canonical (reduced) representative of its scalar-field class. -/ -theorem LAMBDA_lt : LAMBDA < PALLAS_SCALAR_CARD := by decide +theorem LAMBDA_lt : LAMBDA < Fields.Pasta.PALLAS_SCALAR_CARD := by decide /-- `λ` is a cube root of unity in the scalar field — the scalar-side counterpart of `ZETA_cube`, and the reason `φ³ = id` is consistent with `φ = [λ]`. -/ -theorem LAMBDA_cube : (LAMBDA : PallasScalarField) ^ 3 = 1 := by decide +theorem LAMBDA_cube : (LAMBDA : Fields.Pasta.PallasScalarField) ^ 3 = 1 := by decide /-- `λ² + λ + 1 = 0`: the relation `φ² + φ + 1 = 0` that GLV decomposition rests on. -/ -theorem LAMBDA_quad : (LAMBDA : PallasScalarField) ^ 2 + LAMBDA + 1 = 0 := by decide +theorem LAMBDA_quad : (LAMBDA : Fields.Pasta.PallasScalarField) ^ 2 + LAMBDA + 1 = 0 := by decide /-- **The GLV endomorphism on Pallas**: `φ (x, y) = (ζ x, y)`. -/ -def phi (P : SWPoint curve) : SWPoint curve := phiPt A_zero ZETA_cube P +def phi (P : ShortWeierstrass.SWPoint curve) : ShortWeierstrass.SWPoint curve := + Endomorphism.phiPt A_zero ZETA_cube P /-- The spot-check that pins the `(ζ, λ)` pairing: `φ G = [λ] G` on the test point `G = (-1, 2)`. @@ -89,9 +93,9 @@ theorem phi_Gpt : phi Gpt = LAMBDA • Gpt := by native_decide `φ` is an endomorphism (proved outright, `phiHom`); the group has prime order `PALLAS_SCALAR_CARD` (`Pallas.card_eq`, the one place Hasse is assumed); and `φ G = [λ] G` for the non-identity `G` (`phi_Gpt`). By `endo_eq_nsmul_of_prime_card`, `φ` is `[λ]` everywhere. -/ -theorem phi_eq_lambda_nsmul (hHasse : HasseBound curve) (P : SWPoint curve) : - phi P = LAMBDA • P := - phiPt_eq_nsmul A_zero ZETA_cube (card_eq hHasse) Gpt_ne_zero phi_Gpt P +theorem phi_eq_lambda_nsmul (hHasse : CurveOrder.HasseBound curve) + (P : ShortWeierstrass.SWPoint curve) : phi P = LAMBDA • P := + Endomorphism.phiPt_eq_nsmul A_zero ZETA_cube (card_eq hHasse) Gpt_ne_zero phi_Gpt P -- `φ` fixes `𝒪`. example : phi 0 = 0 := by native_decide @@ -108,7 +112,7 @@ example : phi (Gpt + (2 : ℕ) • Gpt) = phi Gpt + phi ((2 : ℕ) • Gpt) := b -- **The `(ζ, λ)` pairing has teeth.** `λ²` is the *other* primitive cube root of unity in `𝔽_q`, -- and `φ` is emphatically not `[λ²]`. Pairing `ζ` with it would give a well-typed, perfectly valid -- endomorphism that is simply the wrong one — which is what `phi_Gpt` exists to rule out. -example : phi Gpt ≠ (LAMBDA ^ 2 % PALLAS_SCALAR_CARD) • Gpt := by native_decide +example : phi Gpt ≠ (LAMBDA ^ 2 % Fields.Pasta.PALLAS_SCALAR_CARD) • Gpt := by native_decide end Pallas @@ -116,7 +120,7 @@ namespace Vesta /-- A primitive cube root of unity in the Vesta *base* field `𝔽_q` (`= PallasScalarField`; the Pasta cycle crosses the two curves' constants). -/ -def ZETA : VestaBaseField := +def ZETA : Fields.Pasta.VestaBaseField := 0x06819a58283e528e511db4d81cf70f5a0fed467d47c033af2aa9d2e050aa0e4f /-- The matching primitive cube root of unity in the Vesta *scalar* field `𝔽ₚ`, as a `ℕ`. -/ @@ -136,24 +140,25 @@ theorem ZETA_ne_one : ZETA ≠ 1 := by decide theorem ZETA_quad : ZETA ^ 2 + ZETA + 1 = 0 := by decide /-- `λ` is a canonical (reduced) representative of its scalar-field class. -/ -theorem LAMBDA_lt : LAMBDA < PALLAS_BASE_CARD := by decide +theorem LAMBDA_lt : LAMBDA < Fields.Pasta.PALLAS_BASE_CARD := by decide /-- `λ` is a cube root of unity in the scalar field. -/ -theorem LAMBDA_cube : (LAMBDA : VestaScalarField) ^ 3 = 1 := by decide +theorem LAMBDA_cube : (LAMBDA : Fields.Pasta.VestaScalarField) ^ 3 = 1 := by decide /-- `λ² + λ + 1 = 0`. -/ -theorem LAMBDA_quad : (LAMBDA : VestaScalarField) ^ 2 + LAMBDA + 1 = 0 := by decide +theorem LAMBDA_quad : (LAMBDA : Fields.Pasta.VestaScalarField) ^ 2 + LAMBDA + 1 = 0 := by decide /-- **The GLV endomorphism on Vesta**: `φ (x, y) = (ζ x, y)`. -/ -def phi (P : SWPoint curve) : SWPoint curve := phiPt A_zero ZETA_cube P +def phi (P : ShortWeierstrass.SWPoint curve) : ShortWeierstrass.SWPoint curve := + Endomorphism.phiPt A_zero ZETA_cube P /-- The spot-check pinning the `(ζ, λ)` pairing on Vesta: `φ G = [λ] G`. -/ theorem phi_Gpt : phi Gpt = LAMBDA • Gpt := by native_decide /-- **`φ = [λ]` on the whole Vesta group** (assuming Hasse's bound). -/ -theorem phi_eq_lambda_nsmul (hHasse : HasseBound curve) (P : SWPoint curve) : - phi P = LAMBDA • P := - phiPt_eq_nsmul A_zero ZETA_cube (card_eq hHasse) Gpt_ne_zero phi_Gpt P +theorem phi_eq_lambda_nsmul (hHasse : CurveOrder.HasseBound curve) + (P : ShortWeierstrass.SWPoint curve) : phi P = LAMBDA • P := + Endomorphism.phiPt_eq_nsmul A_zero ZETA_cube (card_eq hHasse) Gpt_ne_zero phi_Gpt P -- As for Pallas: `φ` fixes `𝒪`, is nontrivial, cubes to the identity, is additive, and is *not* -- `[λ²]` (the other primitive cube root of unity in the scalar field). @@ -161,7 +166,7 @@ example : phi 0 = 0 := by native_decide example : phi Gpt ≠ Gpt := by native_decide example : phi (phi (phi Gpt)) = Gpt := by native_decide example : phi (Gpt + (2 : ℕ) • Gpt) = phi Gpt + phi ((2 : ℕ) • Gpt) := by native_decide -example : phi Gpt ≠ (LAMBDA ^ 2 % PALLAS_BASE_CARD) • Gpt := by native_decide +example : phi Gpt ≠ (LAMBDA ^ 2 % Fields.Pasta.PALLAS_BASE_CARD) • Gpt := by native_decide end Vesta diff --git a/CompElliptic/Endomorphism.lean b/CompElliptic/Endomorphism.lean index ae16fc1..15dca51 100644 --- a/CompElliptic/Endomorphism.lean +++ b/CompElliptic/Endomorphism.lean @@ -39,7 +39,9 @@ closed facts and live in the concrete-curve modules. namespace CompElliptic.Endomorphism -open CompElliptic.CurveForms.ShortWeierstrass +-- 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 @@ -99,14 +101,14 @@ theorem phi_eq_origin_iff (hz : z ^ 3 = 1) (p : F × F) : phi z p = (0, 0) ↔ p 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 : OnCurve 0 b p) : - OnCurve 0 b (phi z p) := by - simp only [OnCurve, phi] at h ⊢ +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 : Valid 0 b p) : - Valid 0 b (phi z p) := by +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]) @@ -143,19 +145,19 @@ slope by exactly `z²`, after which `phi_addX` / `phi_addY` finish. The degenera 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 (add 0 p q) = add 0 (phi z p) (phi z q) := by + 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, CurveForms.ShortWeierstrass.zero_add, phi_origin, CurveForms.ShortWeierstrass.zero_add] + · rw [hp0, ShortWeierstrass.zero_add, phi_origin, ShortWeierstrass.zero_add] by_cases hq0 : q = (0, 0) - · rw [hq0, CurveForms.ShortWeierstrass.add_zero, phi_origin, CurveForms.ShortWeierstrass.add_zero] + · 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 add + 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)] @@ -187,38 +189,41 @@ theorem phi_add (hz : z ^ 3 = 1) (p q : F × F) : /-- `φ` 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 : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) (P : SWPoint E) : SWPoint E := +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 : Valid 0 E.B (P.x, P.y) := hA ▸ P.onCurve - have h' : Valid 0 E.B (phi z (P.x, P.y)) := valid_phi hz h + 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 : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) - (P : SWPoint E) : +@[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 : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) - (P : 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 := - SWPoint.ext_pair (phi_phi_phi hz (P.x, P.y)) + 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 : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) (P Q : SWPoint E) : +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 SWPoint.ext_pair ?_ - show phi z (add E.A (P.x, P.y) (Q.x, Q.y)) - = add E.A (phi z (P.x, P.y)) (phi z (Q.x, Q.y)) + 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 : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) : SWPoint E →+ SWPoint E := +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. @@ -226,10 +231,10 @@ def phiHom {E : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) : SWPoint E →+ SWPo 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 : SWCurve F} (hA : E.A = 0) (hz : z ^ 3 = 1) - {r : ℕ} [Fact r.Prime] (hcard : Nat.card (SWPoint E) = r) - {G : SWPoint E} (hG : G ≠ 0) {lam : ℕ} (hspot : phiPt hA hz G = lam • G) - (P : SWPoint E) : phiPt hA hz P = lam • 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