From 0392940646909e76d26561f75f5e4e3c23f6fd78 Mon Sep 17 00:00:00 2001
From: martyall <martyall@protonmail.com>
Date: Tue, 7 Jul 2026 00:36:24 -0700
Subject: [PATCH 1/4] Pasta: two absolute field names Fp/Fq replace the four
 role aliases
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The role names stated the Pasta cycle as a pun (VestaBaseField =
PallasScalarField and vice versa) — four names for two fields. The fields
now carry their standard absolute names: Fp (the Pallas base field, also
the Vesta scalar field) and Fq (the Pallas scalar field, also the Vesta
base field), matching proof-systems' own convention. Role information
belongs to consumers' relative projections, not to which alias was picked.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 CompElliptic/Curves/Pasta.lean      | 30 ++++++++++++++---------------
 CompElliptic/Curves/PastaOrder.lean |  8 ++++----
 CompElliptic/Encodings/Pasta.lean   |  2 +-
 CompElliptic/Fields/Pasta.lean      | 25 +++++++++++-------------
 4 files changed, 31 insertions(+), 34 deletions(-)

diff --git a/CompElliptic/Curves/Pasta.lean b/CompElliptic/Curves/Pasta.lean
index 871f5da..92b9d1e 100644
--- a/CompElliptic/Curves/Pasta.lean
+++ b/CompElliptic/Curves/Pasta.lean
@@ -27,18 +27,18 @@ open CompElliptic.CurveForms.ShortWeierstrass CompElliptic.Fields.Pasta
 namespace Pallas
 
 /-- Pallas: `y² = x³ + 5` over the Pallas base field (`A = 0`, `B = 5`). -/
-def a : PallasBaseField := 0
-def b : PallasBaseField := 5
+def a : Fp := 0
+def b : Fp := 5
 
 /-- A convenient prime-order point `(-1, 2)` for testing (just a test point, not a
 protocol-specified base). -/
-def G : PallasBaseField × PallasBaseField := (-1, 2)
+def G : Fp × Fp := (-1, 2)
 
 theorem b_ne_zero : b ≠ 0 := by decide
 
 /-- The Pallas curve as a rich `SWCurve`: ellipticity (`sw_Δ 0 5 = -10800 ≠ 0`, so `IsUnit`) and
 `B ≠ 0` discharged by computation. -/
-def curve : SWCurve PallasBaseField where
+def curve : SWCurve Fp where
   A := a
   B := b
   IsElliptic := by rw [isUnit_iff_ne_zero]; decide
@@ -54,14 +54,14 @@ theorem not_onCurve_zero : ¬ OnCurve a b (0, 0) :=
 Euler's criterion (`ZMod.euler_criterion`) reduces this to `5 ^ (p / 2) ≠ 1`. The LHS (`-1`) is
 evaluated by `reduce_mod_char` (fast modular exponentiation via `NormNum.PowMod`), the same
 machinery the `PrattPartList.prime` legs use for their `a ^ k ≠ 1` conditions. -/
-theorem five_not_isSquare : ¬ IsSquare (5 : PallasBaseField) := by
-  rw [ZMod.euler_criterion PALLAS_BASE_CARD (by decide : (5 : PallasBaseField) ≠ 0)]
+theorem five_not_isSquare : ¬ IsSquare (5 : Fp) := by
+  rw [ZMod.euler_criterion PALLAS_BASE_CARD (by decide : (5 : Fp) ≠ 0)]
   reduce_mod_char
   decide
 
 /-- Consequently no point on the Pallas curve has `x`-coordinate `0`, so `x = 0` denotes `𝒪`
 unambiguously. -/
-theorem no_onCurve_x_zero (y : PallasBaseField) : ¬ OnCurve a b (0, y) := by
+theorem no_onCurve_x_zero (y : Fp) : ¬ OnCurve a b (0, y) := by
   intro h
   have h' : y ^ 2 = 5 := by simpa [OnCurve, a, b] using h
   exact five_not_isSquare ⟨y, by rw [← h', pow_two]⟩
@@ -90,19 +90,19 @@ end Pallas
 
 namespace Vesta
 
-/-- Vesta: `y² = x³ + 5` over the Vesta base field (`= PallasScalarField`; `A = 0`, `B = 5`). -/
-def a : VestaBaseField := 0
-def b : VestaBaseField := 5
+/-- Vesta: `y² = x³ + 5` over the Vesta base field (`= Fq`; `A = 0`, `B = 5`). -/
+def a : Fq := 0
+def b : Fq := 5
 
 /-- A convenient prime-order point `(-1, 2)` for testing (just a test point, not a
 protocol-specified base). -/
-def G : VestaBaseField × VestaBaseField := (-1, 2)
+def G : Fq × Fq := (-1, 2)
 
 theorem b_ne_zero : b ≠ 0 := by decide
 
 /-- The Vesta curve as a rich `SWCurve`: ellipticity (`sw_Δ 0 5 = -10800 ≠ 0`, so `IsUnit`) and
 `B ≠ 0` discharged by computation. -/
-def curve : SWCurve VestaBaseField where
+def curve : SWCurve Fq where
   A := a
   B := b
   IsElliptic := by rw [isUnit_iff_ne_zero]; decide
@@ -117,14 +117,14 @@ theorem not_onCurve_zero : ¬ OnCurve a b (0, 0) :=
 
 As for Pallas: Euler's criterion (`ZMod.euler_criterion`) reduces this to `5 ^ (q / 2) ≠ 1`, and
 `reduce_mod_char` (fast modular exponentiation) evaluates the power to `-1`. -/
-theorem five_not_isSquare : ¬ IsSquare (5 : VestaBaseField) := by
-  rw [ZMod.euler_criterion PALLAS_SCALAR_CARD (by decide : (5 : VestaBaseField) ≠ 0)]
+theorem five_not_isSquare : ¬ IsSquare (5 : Fq) := by
+  rw [ZMod.euler_criterion PALLAS_SCALAR_CARD (by decide : (5 : Fq) ≠ 0)]
   reduce_mod_char
   decide
 
 /-- Consequently no point on the Vesta curve has `x`-coordinate `0`, so `x = 0` denotes `𝒪`
 unambiguously. -/
-theorem no_onCurve_x_zero (y : VestaBaseField) : ¬ OnCurve a b (0, y) := by
+theorem no_onCurve_x_zero (y : Fq) : ¬ OnCurve a b (0, y) := by
   intro h
   have h' : y ^ 2 = 5 := by simpa [OnCurve, a, b] using h
   exact five_not_isSquare ⟨y, by rw [← h', pow_two]⟩
diff --git a/CompElliptic/Curves/PastaOrder.lean b/CompElliptic/Curves/PastaOrder.lean
index ed0d2af..3838b2e 100644
--- a/CompElliptic/Curves/PastaOrder.lean
+++ b/CompElliptic/Curves/PastaOrder.lean
@@ -40,9 +40,9 @@ theorem card_eq (hHasse : HasseBound curve) :
     Nat.card (SWPoint curve) = PALLAS_SCALAR_CARD := by
   refine card_eq_of_hasse_of_field_ge_37 curve PALLAS_SCALAR_is_prime Gpt_ne_zero
     scalarCard_nsmul_Gpt hHasse ?_ ?_
-  · rw [show Fintype.card PallasBaseField = PALLAS_BASE_CARD from ZMod.card _]
+  · rw [show Fintype.card Fp = PALLAS_BASE_CARD from ZMod.card _]
     simp only [hasseInterval, Set.mem_setOf_eq]; native_decide
-  · rw [show Fintype.card PallasBaseField = PALLAS_BASE_CARD from ZMod.card _]; decide
+  · rw [show Fintype.card Fp = PALLAS_BASE_CARD from ZMod.card _]; decide
 
 end Pallas
 
@@ -61,9 +61,9 @@ theorem card_eq (hHasse : HasseBound curve) :
     Nat.card (SWPoint curve) = PALLAS_BASE_CARD := by
   refine card_eq_of_hasse_of_field_ge_37 curve PALLAS_BASE_is_prime Gpt_ne_zero
     baseCard_nsmul_Gpt hHasse ?_ ?_
-  · rw [show Fintype.card VestaBaseField = PALLAS_SCALAR_CARD from ZMod.card _]
+  · rw [show Fintype.card Fq = PALLAS_SCALAR_CARD from ZMod.card _]
     simp only [hasseInterval, Set.mem_setOf_eq]; native_decide
-  · rw [show Fintype.card VestaBaseField = PALLAS_SCALAR_CARD from ZMod.card _]; decide
+  · rw [show Fintype.card Fq = PALLAS_SCALAR_CARD from ZMod.card _]; decide
 
 end Vesta
 
diff --git a/CompElliptic/Encodings/Pasta.lean b/CompElliptic/Encodings/Pasta.lean
index 91bc575..59574fc 100644
--- a/CompElliptic/Encodings/Pasta.lean
+++ b/CompElliptic/Encodings/Pasta.lean
@@ -59,7 +59,7 @@ end Curves.Pasta.Pallas
 namespace Curves.Pasta.Vesta
 
 /-- The test point `G = (-1, 2)` on the Vesta curve as an on-curve `SWPoint`, for exercising
-`toBytes` over the Vesta base field (`= PallasScalarField`). -/
+`toBytes` over the Vesta base field (`= Fq`). -/
 def G_point : SWPoint curve := ⟨-1, 2, Or.inl (by decide)⟩
 
 #eval (toBytes G_point).toList
diff --git a/CompElliptic/Fields/Pasta.lean b/CompElliptic/Fields/Pasta.lean
index dd7db07..632b679 100644
--- a/CompElliptic/Fields/Pasta.lean
+++ b/CompElliptic/Fields/Pasta.lean
@@ -22,7 +22,8 @@ namespace CompElliptic.Fields.Pasta
 -- Pallas base field p (= Vesta scalar field).
 @[reducible] def PALLAS_BASE_CARD : Nat := 0x40000000000000000000000000000000224698fc094cf91b992d30ed00000001
 
-abbrev PallasBaseField := ZMod PALLAS_BASE_CARD
+/-- The Pallas base field `𝔽ₚ` — also the Vesta scalar field (the Pasta cycle). -/
+abbrev Fp := ZMod PALLAS_BASE_CARD
 
 theorem PALLAS_BASE_is_prime : Nat.Prime PALLAS_BASE_CARD := by
   unfold PALLAS_BASE_CARD
@@ -88,12 +89,13 @@ theorem PALLAS_BASE_is_prime : Nat.Prime PALLAS_BASE_CARD := by
       · exact .prime 772231 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
 
 instance : Fact (Nat.Prime PALLAS_BASE_CARD) := ⟨PALLAS_BASE_is_prime⟩
-instance : Field PallasBaseField := ZMod.instField PALLAS_BASE_CARD
+instance : Field Fp := ZMod.instField PALLAS_BASE_CARD
 
 -- Pallas scalar field q (= Vesta base field).
 @[reducible] def PALLAS_SCALAR_CARD : Nat := 0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001
 
-abbrev PallasScalarField := ZMod PALLAS_SCALAR_CARD
+/-- The Pallas scalar field `𝔽_q` — also the Vesta base field (the Pasta cycle). -/
+abbrev Fq := ZMod PALLAS_SCALAR_CARD
 
 theorem PALLAS_SCALAR_is_prime : Nat.Prime PALLAS_SCALAR_CARD := by
   unfold PALLAS_SCALAR_CARD
@@ -159,16 +161,11 @@ theorem PALLAS_SCALAR_is_prime : Nat.Prime PALLAS_SCALAR_CARD := by
       · exact .prime 31649 1 _ (by pratt) (by reduce_mod_char; decide) (by norm_num)
 
 instance : Fact (Nat.Prime PALLAS_SCALAR_CARD) := ⟨PALLAS_SCALAR_is_prime⟩
-instance : Field PallasScalarField := ZMod.instField PALLAS_SCALAR_CARD
-
-/-- Vesta base field = Pallas scalar field. -/
-abbrev VestaBaseField := PallasScalarField
-/-- Vesta scalar field = Pallas base field. -/
-abbrev VestaScalarField := PallasBaseField
+instance : Field Fq := ZMod.instField PALLAS_SCALAR_CARD
 
 /-- Tonelli–Shanks data for the Pallas base field `𝔽ₚ`: `p-1 = 2^32 · T`, with `rootOfUnity = 5ᵀ`
 (`pallas.py`). -/
-def pallasBase : TonelliShanks PallasBaseField where
+def pallasBase : TonelliShanks Fp where
   twoAdicity := 32
   oddPart := 0x40000000000000000000000000000000224698fc094cf91b992d30ed
   rootOfUnity := 0x2bce74deac30ebda362120830561f81aea322bf2b7bb7584bdad6fabd87ea32f
@@ -177,11 +174,11 @@ def pallasBase : TonelliShanks PallasBaseField where
 example : (pallasBase.sqrt? 4).map (· ^ 2) = some 4 := by native_decide
 example : pallasBase.sqrt? 5 = none := by native_decide
 -- `√((-1)³ + 5) = √4`: the `y` of the test point `G = (-1, 2)`.
-example : (pallasBase.sqrt? ((-1 : PallasBaseField)^3 + 5)).map (· ^ 2) = some 4 := by native_decide
+example : (pallasBase.sqrt? ((-1 : Fp)^3 + 5)).map (· ^ 2) = some 4 := by native_decide
 
-/-- Tonelli–Shanks data for the Vesta base field `𝔽_q` (`= PallasScalarField`): `q-1 = 2^32 · T`,
+/-- Tonelli–Shanks data for the Vesta base field `𝔽_q` (`= Fq`): `q-1 = 2^32 · T`,
 with `rootOfUnity = 5ᵀ` (`vesta.py`). -/
-def vestaBase : TonelliShanks VestaBaseField where
+def vestaBase : TonelliShanks Fq where
   twoAdicity := 32
   oddPart := 0x40000000000000000000000000000000224698fc0994a8dd8c46eb21
   rootOfUnity := 0x2de6a9b8746d3f589e5c4dfd492ae26e9bb97ea3c106f049a70e2c1102b6d05f
@@ -190,6 +187,6 @@ def vestaBase : TonelliShanks VestaBaseField where
 example : (vestaBase.sqrt? 4).map (· ^ 2) = some 4 := by native_decide
 example : vestaBase.sqrt? 5 = none := by native_decide
 -- `√((-1)³ + 5) = √4`: the `y` of the test point `G = (-1, 2)`.
-example : (vestaBase.sqrt? ((-1 : VestaBaseField)^3 + 5)).map (· ^ 2) = some 4 := by native_decide
+example : (vestaBase.sqrt? ((-1 : Fq)^3 + 5)).map (· ^ 2) = some 4 := by native_decide
 
 end CompElliptic.Fields.Pasta

From 77edae7b7d993a4685eb29227e5e6f5c8b802999 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Wed, 15 Jul 2026 13:05:50 +0200
Subject: [PATCH 2/4] refactor: factor out shared curve lemmas
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Several facts were being re-derived ad hoc at each use site. Pull them
out to a single home so that callers, existing and future, can consume
them instead of restating them.

* `SWPoint.equivSubtype` — the `SWPoint E ≃ { pr : F × F // Valid .. }`
  injection was hand-rolled separately for decidable equality and for
  finiteness. Both now derive from the equiv, as does anything that
  wants to count points as a subtype of `F × F`.
* `Decidable (Valid a b p)` — sits beside the `OnCurve` instance it
  builds on. This removes the need to write `Or.inl (by decide)` to
  exhibit a representable point, and with it the comment in
  `Encodings/Pasta` explaining why `Valid` could not be decided
  directly.
* `SWPoint.neg_x` / `SWPoint.neg_y` — `(-P).y = -P.y` is `rfl`, but was
  inlined with a "there is no named lemma for it" apology at each use.
  Now there is one.
* `dvd_natCard_of_prime_witness` — the prime-witness half of
  `card_eq_of_prime_witness`, split off so other order-pinning routes
  can share it. Its body also stops hand-rolling Mathlib's
  `addOrderOf_eq_prime`, which is exactly the three lines it spelled out.

No new mathematical results and no statement changes: every existing
theorem keeps its signature, and only proofs and locations move.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 CompElliptic/CurveForms/ShortWeierstrass.lean | 29 +++++++++++++++++--
 CompElliptic/CurveOrder.lean                  | 25 ++++++++++------
 CompElliptic/Encodings/Pasta.lean             |  8 ++---
 3 files changed, 45 insertions(+), 17 deletions(-)

diff --git a/CompElliptic/CurveForms/ShortWeierstrass.lean b/CompElliptic/CurveForms/ShortWeierstrass.lean
index d7eb6f5..f0c938c 100644
--- a/CompElliptic/CurveForms/ShortWeierstrass.lean
+++ b/CompElliptic/CurveForms/ShortWeierstrass.lean
@@ -46,6 +46,11 @@ instance (a b : F) (p : F × F) : Decidable (OnCurve a b p) := by unfold OnCurve
 /-- A representable point: on the curve, or the `(0, 0)` identity sentinel `𝒪`. -/
 def Valid (a b : F) (p : F × F) : Prop := OnCurve a b p ∨ p = (0, 0)
 
+/-- Representability is decidable too: being on the curve is, and so is the `(0, 0)` sentinel test.
+This is what lets a representable point be exhibited by `decide`, and `SWPoint E` be counted as a
+subtype of `F × F`. -/
+instance (a b : F) (p : F × F) : Decidable (Valid a b p) := by unfold Valid; infer_instance
+
 omit [DecidableEq F] in
 /-- The `(0, 0)` sentinel is off the curve exactly when `b ≠ 0` (which holds for any elliptic
 curve: `a = b = 0` is the singular cusp `y² = x³`). This is what makes `(0, 0) ≡ 𝒪` unambiguous. -/
@@ -389,6 +394,15 @@ theorem SWPoint.ext_pair {E : SWCurve F} {P Q : SWPoint E}
   injection h with hx hy
   subst hx; subst hy; rfl
 
+/-- Points on `E` are exactly the valid coordinate pairs: the carried `onCurve` proof is a `Prop`,
+so nothing is lost by passing to the subtype. This is the bridge to anything `F × F` already knows —
+decidable equality, finiteness, and counting `SWPoint E` as a `Finset` of pairs. -/
+def SWPoint.equivSubtype (E : SWCurve F) : SWPoint E ≃ { pr : F × F // Valid E.A E.B pr } where
+  toFun P := ⟨(P.x, P.y), P.onCurve⟩
+  invFun pr := ⟨pr.1.1, pr.1.2, pr.2⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
 /-- Addition lifted to `SWPoint E`; closure from `valid_add`. -/
 def sw_add {E : SWCurve F} (P Q : SWPoint E) : SWPoint E :=
   haveI := instIsElliptic E
@@ -403,6 +417,15 @@ instance (E : SWCurve F) : Zero (SWPoint E) := ⟨SWPoint.zero E⟩
 instance (E : SWCurve F) : Add (SWPoint E) := ⟨sw_add⟩
 instance (E : SWCurve F) : Neg (SWPoint E) := ⟨sw_neg⟩
 
+omit [DecidableEq F] in
+/-- Negation fixes the `x`-coordinate. True by `rfl` (`sw_neg` is `neg` on the coordinates), but
+worth naming: without it every caller re-derives it inline. -/
+@[simp] theorem SWPoint.neg_x {E : SWCurve F} (P : SWPoint E) : (-P).x = P.x := rfl
+
+omit [DecidableEq F] in
+/-- Negation negates the `y`-coordinate — the one fact that makes `2 • P = 0` say `P.y = -P.y`. -/
+@[simp] theorem SWPoint.neg_y {E : SWCurve F} (P : SWPoint E) : (-P).y = -P.y := rfl
+
 /-! ### Fast (logarithmic) scalar multiplication
 
 The spec-level `smul` is linear (`n` additions), so it cannot be evaluated by `decide` or
@@ -413,9 +436,9 @@ double-and-add `CompElliptic.binNsmul` over the raw `sw_add` / `SWPoint.zero`. S
 `n • _` lemma still applies, since they follow from `nsmul_zero` and `nsmul_succ`. -/
 
 /-- `SWPoint E` has decidable equality (the `onCurve` field is a `Prop`, so equality reduces to the
-coordinate pair); needed for `native_decide` on `n • P = Q`. -/
-instance instDecidableEqSWPoint {E : SWCurve F} : DecidableEq (SWPoint E) := fun P Q =>
-  decidable_of_iff ((P.x, P.y) = (Q.x, Q.y)) ⟨SWPoint.ext_pair, fun h => by rw [h]⟩
+coordinate pair, via `SWPoint.equivSubtype`); needed for `native_decide` on `n • P = Q`. -/
+instance instDecidableEqSWPoint {E : SWCurve F} : DecidableEq (SWPoint E) :=
+  (SWPoint.equivSubtype E).decidableEq
 
 /-- The abelian group of representable points on `E`: identity laws and inverses are immediate;
 commutativity and associativity transport from the raw `add` lemmas, whose hypotheses are discharged
diff --git a/CompElliptic/CurveOrder.lean b/CompElliptic/CurveOrder.lean
index 1b3ed03..2482212 100644
--- a/CompElliptic/CurveOrder.lean
+++ b/CompElliptic/CurveOrder.lean
@@ -42,20 +42,26 @@ open CompElliptic.CurveForms.ShortWeierstrass
 
 /-! ## Layer 1: pin the order from a prime-order witness (any finite additive group) -/
 
+/-- **The prime-order witness step.** A non-identity `P` killed by a prime `r` has `addOrderOf P`
+exactly `r` (`addOrderOf_eq_prime`), so `r ∣ #G` by Lagrange.
+
+This is the half of the argument that uses the witness, and the only half; everything downstream
+just rules out the remaining multiples of `r` using an upper bound on `#G`. -/
+theorem dvd_natCard_of_prime_witness {G : Type*} [AddGroup G] [Finite G] {r : ℕ}
+    (hr : r.Prime) {P : G} (hP : P ≠ 0) (hPr : r • P = 0) : r ∣ Nat.card G := by
+  haveI := Fact.mk hr
+  exact addOrderOf_eq_prime hPr hP ▸ addOrderOf_dvd_natCard P
+
 /-- If `r` is prime, the finite additive group `G` has a non-identity element `P` killed by `r`
 (`r • P = 0`), and `#G < 2r`, then `#G = r`.
 
-`r • P = 0` gives `addOrderOf P ∣ r`; primality and `P ≠ 0` upgrade this to `addOrderOf P = r`,
-so `r ∣ #G` by Lagrange. With `0 < #G < 2r` the only multiple of `r` available is `r` itself. -/
+The witness gives `r ∣ #G` (`dvd_natCard_of_prime_witness`); with `0 < #G < 2r` the only multiple
+of `r` available is `r` itself. -/
 theorem card_eq_of_prime_witness {G : Type*} [AddGroup G] [Finite G] {r : ℕ}
     (hr : r.Prime) {P : G} (hP : P ≠ 0) (hPr : r • P = 0)
     (hlt : Nat.card G < 2 * r) : Nat.card G = r := by
-  have hdvd : addOrderOf P ∣ r := addOrderOf_dvd_iff_nsmul_eq_zero.mpr hPr
-  have hne1 : addOrderOf P ≠ 1 := by simp [hP]
-  have hord : addOrderOf P = r := (hr.eq_one_or_self_of_dvd _ hdvd).resolve_left hne1
-  have hrdvd : r ∣ Nat.card G := hord ▸ addOrderOf_dvd_natCard P
   have hne0 : Nat.card G ≠ 0 := Nat.card_ne_zero.mpr ⟨⟨P⟩, inferInstance⟩
-  exact Nat.eq_of_dvd_of_lt_two_mul hne0 hrdvd hlt
+  exact Nat.eq_of_dvd_of_lt_two_mul hne0 (dvd_natCard_of_prime_witness hr hP hPr) hlt
 
 /-! ## Layer 2: the Hasse bound (assumed; not yet in Mathlib) discharges `#G < 2r` -/
 
@@ -105,10 +111,11 @@ as a hypothesis where needed. -/
 def HasseBound {F : Type*} [Field F] [Fintype F] (E : SWCurve F) : Prop :=
   Nat.card (SWPoint E) ∈ hasseInterval (Fintype.card F)
 
-/-- `SWPoint E` is finite whenever the base field is, by the injection into `F × F`. -/
+/-- `SWPoint E` is finite whenever the base field is: it is a subtype of `F × F`
+(`SWPoint.equivSubtype`). -/
 instance instFiniteSWPoint {F : Type*} [Field F] [DecidableEq F] [Fintype F] (E : SWCurve F) :
     Finite (SWPoint E) :=
-  Finite.of_injective (fun P => (P.x, P.y)) (fun _ _ h => SWPoint.ext_pair h)
+  Finite.of_equiv _ (SWPoint.equivSubtype E).symm
 
 /-- **Order of a prime-order short-Weierstrass curve group, via Hasse.** Given Hasse's bound
 (assumed), a prime `r`, a non-identity point `P` with `r • P = 0`, and the concrete gap
diff --git a/CompElliptic/Encodings/Pasta.lean b/CompElliptic/Encodings/Pasta.lean
index 91bc575..3ccfb56 100644
--- a/CompElliptic/Encodings/Pasta.lean
+++ b/CompElliptic/Encodings/Pasta.lean
@@ -47,10 +47,8 @@ instance : Fact (PALLAS_SCALAR_CARD ≤ 2^255) := ⟨by decide⟩
 
 namespace Curves.Pasta.Pallas
 
-/-- The test point `G = (-1, 2)` as an on-curve `SWPoint`, for exercising `toBytes`.
-(`Valid` is `OnCurve ∨ · = (0, 0)`; only the `OnCurve` disjunct is `Decidable`, so we supply
-`Or.inl (by decide)` rather than deciding `Valid` directly.) -/
-def G_point : SWPoint curve := ⟨-1, 2, Or.inl (by decide)⟩
+/-- The test point `G = (-1, 2)` as an on-curve `SWPoint`, for exercising `toBytes`. -/
+def G_point : SWPoint curve := ⟨-1, 2, by decide⟩
 
 #eval (toBytes G_point).toList
 
@@ -60,7 +58,7 @@ namespace Curves.Pasta.Vesta
 
 /-- The test point `G = (-1, 2)` on the Vesta curve as an on-curve `SWPoint`, for exercising
 `toBytes` over the Vesta base field (`= PallasScalarField`). -/
-def G_point : SWPoint curve := ⟨-1, 2, Or.inl (by decide)⟩
+def G_point : SWPoint curve := ⟨-1, 2, by decide⟩
 
 #eval (toBytes G_point).toList
 

From 082b57a58daddca4f6e85fa271ec50fc8d226d51 Mon Sep 17 00:00:00 2001
From: Daira-Emma Hopwood <daira@jacaranda.org>
Date: Thu, 16 Jul 2026 01:39:45 +0100
Subject: [PATCH 3/4] feat: pin the Pasta group orders without assuming Hasse
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Fix the Pallas and Vesta group orders to their known primes with no assumption.
A prime-order witness ([order]·G = 𝒪) gives r ∣ #E; it then remains to bound #E.
Mathlib has no Hasse bound for WeierstrassCurve, so use the elementary fibre bound

looser than Hasse (a factor of ~2 rather than 2√q) but unconditional, and enough when
r ≈ #F: Pallas closes directly (#F < r ⇒ #E < 2r), and Vesta additionally rules out

CurveOrder holds the reusable core: Layer 1 pins the order from the witness plus an
upper bound (< 2r, or < 3r without 2-torsion); Layer 2 is the fibre bound. Curves.PastaOrder
instantiates it at the two curves. Every remaining obligation is a closed comparison of

Co-authored-by: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Signed-off-by: Daira-Emma Hopwood <daira@jacaranda.org>
---
 CompElliptic.lean                   |   1 +
 CompElliptic/CurveOrder.lean        | 272 ++++++++++++++++------------
 CompElliptic/Curves/Pasta.lean      |  25 +++
 CompElliptic/Curves/PastaOrder.lean |  77 ++++----
 CompElliptic/Fields/Residue.lean    |  42 +++++
 5 files changed, 270 insertions(+), 147 deletions(-)
 create mode 100644 CompElliptic/Fields/Residue.lean

diff --git a/CompElliptic.lean b/CompElliptic.lean
index 513c96c..24cd793 100644
--- a/CompElliptic.lean
+++ b/CompElliptic.lean
@@ -11,6 +11,7 @@ import CompElliptic.Encoding
 import CompElliptic.Encodings.Common
 import CompElliptic.Encodings.Pasta
 import CompElliptic.Fields.Pasta
+import CompElliptic.Fields.Residue
 import CompElliptic.Fields.Sqrt
 import CompElliptic.CurveForms.ShortWeierstrass
 import CompElliptic.CurveOrder
diff --git a/CompElliptic/CurveOrder.lean b/CompElliptic/CurveOrder.lean
index 2482212..2afc445 100644
--- a/CompElliptic/CurveOrder.lean
+++ b/CompElliptic/CurveOrder.lean
@@ -2,7 +2,7 @@
 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
+Authors: Daira-Emma Hopwood, Gregor Mitscha-Baude
 -/
 import CompElliptic.CurveForms.ShortWeierstrass
 import Mathlib.GroupTheory.OrderOfElement
@@ -15,25 +15,28 @@ no point-counting algorithm (no Schoof, no proof of a counting algorithm's corre
 It needs only:
 
 1. a non-identity point P killed by r (so r ∣ #G, since r is prime); and
-2. an *upper* bound #G < 2r, which can be provided by the Hasse bound for elliptic curves.
+2. an upper bound on #G that leaves r (rather than some multiple ≥ 2r) as the only possible #G.
 
-This module is the curve-agnostic core of that argument, in two layers.
+This module supplies both layers, and neither assumes any general theorem — in particular not
+Hasse's theorem, which Mathlib lacks for `WeierstrassCurve`.
 
 * **Layer 1 — pure finite-group theory.** `card_eq_of_prime_witness` holds for *any* finite
   additive group, with no reference to elliptic curves. A witness of r • P = 0 forces r ∣ #G,
-  and #G < 2r then forces #G = r.
-
-* **Layer 2 — the Hasse bound.** If G is any elliptic curve E(F) over any finite field F of
-  order q ≥ 37, Hasse's theorem |#E(F) - (q+1)| ≤ 2·√q supplies the #G < 2r premiss provided
-  that r also satisfies the Hasse bound. For a prime-order cryptographic curve r ≈ q, so 2r
-  sits far above the Hasse upper bound. Mathlib does not yet have Hasse's theorem for
-  `WeierstrassCurve`, so we state it as a predicate (`HasseBound`) and take it as a hypothesis.
-
-This is an application of the *Independently re-checkable trust* principle: the one piece
-of trust beyond the kernel + standard axioms is a single *named general theorem* (Hasse),
-flagged as an explicit hypothesis. It is separated from the concrete *closed numeric* fact
-4q < (2r - (q+1))² (`hgap`), or alternatively the Hasse bound on r (`hr`), either of which
-can be verified by any independent tool.
+  and #G < 2r then forces #G = r. `card_eq_of_prime_witness_of_lt_three_mul` reaches the same
+  conclusion from the weaker #G < 3r, at the price of ruling out 2-torsion (which kills the extra
+  candidate 2r by Cauchy's theorem).
+
+* **Layer 2 — the fibre bound.** For a short-Weierstrass curve E over any finite field F, the
+  equation y² = x³ + A x + B has at most two roots y for each fixed x; summing over #F choices of
+  x and adding 𝒪 gives `#E(F) ≤ 2·#F + 1` (`card_le_two_mul_card_add_one`), with no arithmetic
+  geometry. This overshoots the true count by a factor of about two where Hasse overshoots by only
+  2√q, but it is unconditional, and it is enough whenever the prime r is close to the field size —
+  exactly the situation for a prime-order cryptographic curve. Which of Layer 1's thresholds it
+  clears is then decided by the two concrete numbers #F and r.
+
+This is an application of the *Independently re-checkable trust* principle: no general theorem is
+assumed, and all that a caller must discharge are closed numeric facts about #F and r, verifiable
+by any independent tool.
 -/
 
 namespace CompElliptic.CurveOrder
@@ -59,57 +62,40 @@ The witness gives `r ∣ #G` (`dvd_natCard_of_prime_witness`); with `0 < #G < 2r
 of `r` available is `r` itself. -/
 theorem card_eq_of_prime_witness {G : Type*} [AddGroup G] [Finite G] {r : ℕ}
     (hr : r.Prime) {P : G} (hP : P ≠ 0) (hPr : r • P = 0)
-    (hlt : Nat.card G < 2 * r) : Nat.card G = r := by
+    (hlt2r : Nat.card G < 2 * r) : Nat.card G = r := by
   have hne0 : Nat.card G ≠ 0 := Nat.card_ne_zero.mpr ⟨⟨P⟩, inferInstance⟩
-  exact Nat.eq_of_dvd_of_lt_two_mul hne0 (dvd_natCard_of_prime_witness hr hP hPr) hlt
-
-/-! ## Layer 2: the Hasse bound (assumed; not yet in Mathlib) discharges `#G < 2r` -/
-
-/-- The Hasse interval for a field of size `q`: the cardinalities `n` within `2√q` of `q + 1`,
-written sqrt-free over `ℤ` as `(n - (q+1))² ≤ 4·q` (equivalently `|n - (q+1)| ≤ 2√q`). By Hasse's
-theorem every point count `#E(F)` lies in it (with `q = #F`); we use the same interval to constrain
-a candidate prime order. -/
-def hasseInterval (q : ℕ) : Set ℕ := { n | ((n : ℤ) - (q+1))^2 ≤ 4*q }
-
-/-- The arithmetic step from Hasse to the layer-1 premiss, purely over `ℕ`/`ℤ` and independent of
-any particular curve. From the sqrt-free Hasse inequality on `N` relative to the field size `q`
-(`(N - (q+1))² ≤ 4·q`), the concrete gap `4·q < (2r - (q+1))²`, and `q + 1 ≤ 2r`, conclude `N < 2r`.
-(Only the *upper* Hasse bound is used; the gap and `q + 1 ≤ 2r` are closed facts about the two
-relevant numbers, true here because `r ≈ q` so `2r` clears the upper bound with room.) -/
-theorem lt_two_mul_of_hasse {N q r : ℕ}
-    (hHasse : N ∈ hasseInterval q)
-    (hgap : 4*(q : ℤ) < (2*r - (q+1))^2)
-    (hle : (q : ℤ) + 1 ≤ 2*r) :
-    N < 2*r := by
-  simp only [hasseInterval, Set.mem_setOf_eq] at hHasse
-  by_contra hcon
-  rw [not_lt] at hcon
-  have hN : (2*r : ℤ) ≤ (N : ℤ) := by exact_mod_cast hcon
-  have h0 : (0 : ℤ) ≤ 2*r - (q+1) := by linarith
-  have h1 : 2*(r : ℤ) - (q+1) ≤ (N : ℤ) - (q+1) := by linarith
-  have hmono : (2*(r : ℤ) - (q+1))^2 ≤ ((N : ℤ) - (q+1))^2 := pow_le_pow_left₀ h0 h1 2
-  linarith
-
-/-- The Hasse bound for a short-Weierstrass elliptic curve `E` over a finite field `F` with
-`q = #F`: `|#E(F) - (q+1)| ≤ 2·√q`, written sqrt-free over `ℤ` as `(#E(F) - (q+1))² ≤ 4·q`,
-where `#E(F) = Nat.card (SWPoint E)`.
-
-This is Hasse's theorem, the "Riemann hypothesis for elliptic function fields":
-
-> H. Hasse, *Zur Theorie der abstrakten elliptischen Funktionenkörper III: Die Struktur des
-> Meromorphismenrings; Die Riemannsche Vermutung*, Journal für die reine und angewandte
-> Mathematik (Crelle's Journal) *175* (1936), 193–208. doi:10.1515/crll.1936.175.193.
-
-The point-count form used here is §4.2 (p. 206): for `N₁` the number of degree-one prime divisors
-(`= #E(F)`, the `F`-rational places including `𝒪`) and `q = #F`, `(q + 1 - N₁)² ≤ 4q`. It rests on
-§3.1 (p. 203), where the Frobenius meromorphism `π : (x, y) ↦ (x^q, y^q)` satisfies
-`Q(π) = π² - lπ + q = 0` with `l² ≤ 4q`. A scan of part III is available at
-https://download.uni-mainz.de/mathematik/Algebraische%20Geometrie/Lehre/WS23.Padische.Hasse.III.pdf
-
-Mathlib does not yet carry this for `WeierstrassCurve`, so we define the statement and take it
-as a hypothesis where needed. -/
-def HasseBound {F : Type*} [Field F] [Fintype F] (E : SWCurve F) : Prop :=
-  Nat.card (SWPoint E) ∈ hasseInterval (Fintype.card F)
+  exact Nat.eq_of_dvd_of_lt_two_mul hne0 (dvd_natCard_of_prime_witness hr hP hPr) hlt2r
+
+/-- The same conclusion as `card_eq_of_prime_witness` from a weaker bound `#G < 3r`, at the price
+of ruling out 2-torsion (`hOdd`).
+
+`#G < 2r` leaves `r` as the only multiple of `r` in range; `#G < 3r` also admits `2r`. That case is
+excluded by parity rather than by counting: `#G = 2r` is even, so Cauchy's theorem would supply an
+element of order exactly 2, which `hOdd` forbids.
+
+The weaker bound is what an elementary point count affords when the prime sits just below the field
+size, so this is the entry point for callers who cannot reach `2r` — but the argument is pure
+finite-group theory and mentions no curve. -/
+theorem card_eq_of_prime_witness_of_lt_three_mul {G : Type*} [AddGroup G] [Finite G] {r : ℕ}
+    (hrPrime : r.Prime) {P : G} (hP : P ≠ 0) (hrP : r • P = 0)
+    (hlt3r : Nat.card G < 3 * r) (hOdd : ∀ Q : G, 2 • Q = 0 → Q = 0) : Nat.card G = r := by
+  obtain ⟨k, hk⟩ := dvd_natCard_of_prime_witness hrPrime hP hrP
+  -- `#G = r * k` with `r * k < 3 * r`, so `k < 3`; `k = 0` contradicts `0 < #G`.
+  have hklt3 : k < 3 := by
+    refine Nat.lt_of_mul_lt_mul_left (a := r) ?_
+    simp_all only [nsmul_zero, ne_eq, mul_comm]
+  have hkne0 : k ≠ 0 := by
+    rintro rfl
+    exact absurd (hk.trans (Nat.mul_zero r)) Nat.card_pos.ne'
+  -- `k = 2` would make `#G` even, so Cauchy would give an element of order 2 — excluded by `hOdd`.
+  have hkne2 : k ≠ 2 := by
+    rintro rfl
+    haveI : Fintype G := Fintype.ofFinite _
+    have hEven : 2 ∣ Fintype.card G := ⟨r, by rw [← Nat.card_eq_fintype_card, hk]; ring⟩
+    obtain ⟨Q, hQ⟩ := exists_prime_addOrderOf_dvd_card 2 hEven
+    have hQ0 : Q ≠ 0 := fun h => by simp [h, addOrderOf_zero] at hQ
+    exact hQ0 (hOdd Q (hQ ▸ addOrderOf_nsmul_eq_zero Q))
+  rw [hk, show k = 1 by omega, Nat.mul_one]
 
 /-- `SWPoint E` is finite whenever the base field is: it is a subtype of `F × F`
 (`SWPoint.equivSubtype`). -/
@@ -117,57 +103,111 @@ instance instFiniteSWPoint {F : Type*} [Field F] [DecidableEq F] [Fintype F] (E
     Finite (SWPoint E) :=
   Finite.of_equiv _ (SWPoint.equivSubtype E).symm
 
-/-- **Order of a prime-order short-Weierstrass curve group, via Hasse.** Given Hasse's bound
-(assumed), a prime `r`, a non-identity point `P` with `r • P = 0`, and the concrete gap
-`4q < (2r - (q+1))²` together with `q + 1 ≤ 2r`, the curve group has exactly `r` points. -/
-theorem card_eq_of_hasse {F : Type*} [Field F] [DecidableEq F] [Fintype F] (E : SWCurve F)
-    {r : ℕ} (hrPrime : r.Prime) {P : SWPoint E} (hP : P ≠ 0) (hPr : r • P = 0)
-    (hHasse : HasseBound E)
-    (hgap : 4*(Fintype.card F : ℤ) < (2*r - (Fintype.card F + 1))^2)
-    (hle : (Fintype.card F : ℤ) + 1 ≤ 2*r) :
+/-! ## Layer 2: the fibre bound `#E(F) ≤ 2 · #F + 1` -/
+
+variable {F : Type*} [Field F] [DecidableEq F]
+
+/-- **At most two points share an x-coordinate.** Two on-curve points sharing an `x` have
+`y² = x³ + A x + B` for the *same* right-hand side, so `(y₁ − y₂)(y₁ + y₂) = 0` and hence
+`y₁ = y₂ ∨ y₁ = −y₂` — the short-Weierstrass form of `WeierstrassCurve.Affine.Y_eq_of_X_eq`.
+The fibre for any point is therefore contained in the two-element set `{(x, y), (x, −y)}`. -/
+theorem card_fibre_le_two [Fintype F] (E : SWCurve F) (x : F) :
+    ((Finset.univ.filter fun R : F × F => OnCurve E.A E.B R).filter
+      fun R => R.1 = x).card ≤ 2 := by
+  rcases ((Finset.univ.filter fun R : F × F => OnCurve E.A E.B R).filter
+      fun R => R.1 = x).eq_empty_or_nonempty with hR | ⟨P, hP⟩
+  · simp [hR]
+  · simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hP
+    obtain ⟨hPOnCurve, hxP⟩ := hP
+    refine le_trans (Finset.card_le_card ?_) ((Finset.card_insert_le P {(x, -P.2)}).trans (by simp))
+    intro Q hQ
+    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hQ
+    obtain ⟨hQOnCurve, hxQ⟩ := hQ
+    have hsq : Q.2 ^ 2 = P.2 ^ 2 := by
+      simp only [OnCurve] at hPOnCurve hQOnCurve
+      rw [hPOnCurve, hQOnCurve, hxP, hxQ]
+    have hfac : (Q.2 - P.2) * (Q.2 + P.2) = 0 := by linear_combination hsq
+    rcases mul_eq_zero.mp hfac with h | h
+    · exact Finset.mem_insert.mpr (Or.inl (Prod.ext (hxQ.trans hxP.symm) (sub_eq_zero.mp h)))
+    · exact Finset.mem_insert.mpr
+        (Or.inr (Finset.mem_singleton.mpr (Prod.ext hxQ (eq_neg_of_add_eq_zero_left h))))
+
+/-- **The unconditional cardinality bound**: at most two points per `x`-coordinate
+(`card_fibre_le_two`) over `#F` choices of `x`, plus the identity `𝒪`.
+
+This is elementary and holds for every short-Weierstrass curve over every finite field; it is
+looser than Hasse (which Mathlib lacks) but needs no algebraic geometry. -/
+theorem card_le_two_mul_card_add_one [Fintype F] (E : SWCurve F) :
+    Nat.card (SWPoint E) ≤ 2 * Fintype.card F + 1 := by
+  rw [Nat.card_congr (SWPoint.equivSubtype E), Nat.card_eq_fintype_card, Fintype.card_subtype]
+  have hsub : (Finset.univ.filter fun R : F × F => Valid E.A E.B R) ⊆
+      (Finset.univ.filter fun R : F × F => OnCurve E.A E.B R) ∪ {((0 : F), (0 : F))} := by
+    intro R hR
+    simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_union,
+      Finset.mem_singleton] at hR ⊢
+    exact hR
+  calc (Finset.univ.filter fun R : F × F => Valid E.A E.B R).card
+      ≤ ((Finset.univ.filter fun R : F × F => OnCurve E.A E.B R) ∪ {0}).card :=
+        Finset.card_le_card hsub
+    _ ≤ (Finset.univ.filter fun R : F × F => OnCurve E.A E.B R).card + 1 :=
+        le_trans (Finset.card_union_le _ _) (by simp)
+    _ ≤ 2 * Fintype.card F + 1 := by
+        have h := Finset.card_le_mul_card_image_of_maps_to
+          (f := Prod.fst) (t := (Finset.univ : Finset F))
+          (fun _ _ => Finset.mem_univ _) 2 (fun x _ => card_fibre_le_two E x)
+        rw [Finset.card_univ] at h
+        omega
+
+/-! ## Order pinning from the fibre bound
+
+Both results below feed `card_le_two_mul_card_add_one` into Layer 1, replacing its `#G < 2r` (resp.
+`#G < 3r`) premiss by a closed numeric comparison between `#F` and `r`. -/
+
+/-- **Order of a prime-order curve group whose prime exceeds the field size.** If the prime `r`
+kills the non-identity point `P` and `2 · #F + 1 < 2r`, the curve group has exactly `r` points.
+
+The Layer 1 core `card_eq_of_prime_witness`, with the upper bound supplied by
+`card_le_two_mul_card_add_one`. -/
+theorem card_eq_of_prime_witness_of_card_lt_two_mul [Fintype F] (E : SWCurve F) {r : ℕ}
+    (hrPrime : r.Prime) {P : SWPoint E} (hP : P ≠ 0) (hPr : r • P = 0)
+    (hBound : 2 * Fintype.card F + 1 < 2 * r) :
     Nat.card (SWPoint E) = r :=
-  card_eq_of_prime_witness hrPrime hP hPr (lt_two_mul_of_hasse hHasse hgap hle)
-
-/-! ## Alternative approach that reaches the same conclusion -/
-
-/-- Convenience form of `lt_two_mul_of_hasse` for callers who already hold the two-sided Hasse
-bound. For `37 ≤ q` (the least prime power for which `2·(q + 1 - 2√q) > q + 1 + 2√q`), the
-explicit gap inequalities are implied by the Hasse bound on `r` itself: a `r` in the Hasse interval
-`[q + 1 - 2√q, q + 1 + 2√q]` has `2r ≥ 2·(q + 1 - 2√q) > q + 1 + 2√q ≥ N`, so `N < 2r`.
-
-The Hasse bound on `r` (`hr`) is essential — `37 ≤ q` alone is unsound. A witness of small prime
-order (e.g. an order-2 point on a group of composite order in the interval) would otherwise force a
-wrong conclusion; `hr` pins `r` to the interval from below, ruling that out. -/
-theorem lt_two_mul_of_hasse_of_field_ge_37 {N q r : ℕ}
-    (hN : N ∈ hasseInterval q)
-    (hr : r ∈ hasseInterval q)
-    (hq : 37 ≤ q) :
-    N < 2*r := by
-  simp only [hasseInterval, Set.mem_setOf_eq] at hN hr
-  have hq' : (36 : ℤ) < q := by exact_mod_cast hq
-  by_contra hcon
-  rw [not_lt] at hcon
-  have hcon' : 2 * (r : ℤ) ≤ (N : ℤ) := by exact_mod_cast hcon
-  -- Writing `n = N - (q+1)`, `m = r - (q+1)`: from `hN`/`hr`, `(n - 2m)² ≤ 3n² + 6m² ≤ 36·q`
-  -- (the `sq_nonneg (n+m)` hint supplies `-4nm ≤ 2(n² + m²)`); but `N ≥ 2r` gives `n - 2m ≥ q+1`,
-  -- so `(q+1)² ≤ (n-2m)² ≤ 36·q`, contradicting `37 ≤ q` (where `(q+1)² > 36·q`).
-  nlinarith [hN, hr, hq', hcon',
-    sq_nonneg ((N : ℤ) - (q+1) + ((r : ℤ) - (q+1))),
-    mul_nonneg (show (0 : ℤ) ≤ (N : ℤ) - 2*r by linarith)
-               (show (0 : ℤ) ≤ (N : ℤ) - 2*r + 2*((q : ℤ)+1) by linarith)]
-
-/-- Curve-level capstone of the `37 ≤ #F` route: combine `HasseBound` (assumed) with `37 ≤ #F` and
-the Hasse bound on the prime `r` to conclude the curve group has exactly `r` points, without the
-caller having to supply the explicit gap inequalities `hgap` and `hle`.
-
-`hHasse` is definitionally the two-sided bound on `#E(F)` that `lt_two_mul_of_hasse_of_field_ge_37`
-needs; see there for why `hr` is needed. -/
-theorem card_eq_of_hasse_of_field_ge_37 {F : Type*} [Field F] [DecidableEq F] [Fintype F]
-    (E : SWCurve F) {r : ℕ} (hrPrime : r.Prime) {P : SWPoint E} (hP : P ≠ 0) (hPr : r • P = 0)
-    (hHasse : HasseBound E)
-    (hr : r ∈ hasseInterval (Fintype.card F))
-    (hq : 37 ≤ Fintype.card F) :
+  card_eq_of_prime_witness hrPrime hP hPr
+    (lt_of_le_of_lt (card_le_two_mul_card_add_one E) hBound)
+
+/-- No 2-torsion on a curve, in odd characteristic, no point of which has `y = 0`.
+
+A point with `2 • Q = 0` satisfies `Q = -Q`, hence `Q.y = -Q.y` and so `2 · Q.y = 0`; with
+`2 ≠ 0` that forces `Q.y = 0`. An on-curve point cannot then exist by hypothesis, leaving
+only the sentinel `𝒪`. This discharges the `hOdd` side condition of
+`card_eq_of_prime_witness_of_card_lt_three_mul`. -/
+theorem eq_zero_of_two_nsmul_eq_zero {E : SWCurve F} (h2ne0 : (2 : F) ≠ 0)
+    (hy : ∀ x : F, ¬ OnCurve E.A E.B (x, 0)) {Q : SWPoint E} (hQ : 2 • Q = 0) : Q = 0 := by
+  rw [two_nsmul] at hQ
+  have hNeg : Q = -Q := eq_neg_of_add_eq_zero_left hQ
+  have hyy : Q.y = -Q.y := by rw [← SWPoint.neg_y Q, ← hNeg]
+  have hQy : Q.y = 0 := by
+    have h2y : 2 * Q.y = 0 := by linear_combination hyy
+    exact (mul_eq_zero.mp h2y).resolve_left h2ne0
+  rcases Q.onCurve with hc | h0
+  · rw [hQy] at hc
+    exact absurd hc (hy Q.x)
+  · exact SWPoint.ext_pair h0
+
+/-- **Order of a prime-order curve group whose prime is below the field size.** There the fibre
+bound only yields `#E(F) < 3r`, admitting `#E(F) = 2r` alongside `#E(F) = r`. Given additionally
+that the group has no 2-torsion, `2r` is impossible, and `#E(F) = r`.
+
+The curve-free half is Layer 1's `card_eq_of_prime_witness_of_lt_three_mul`; all this adds is the
+fibre bound, so that the caller supplies a comparison between `#F` and `r` rather than one against
+`#E(F)`. Use `eq_zero_of_two_nsmul_eq_zero` to supply `hOdd` from the absence of curve points with
+`y = 0`. -/
+theorem card_eq_of_prime_witness_of_card_lt_three_mul [Fintype F] (E : SWCurve F) {r : ℕ}
+    (hrPrime : r.Prime) {P : SWPoint E} (hP : P ≠ 0) (hPr : r • P = 0)
+    (hBound : 2 * Fintype.card F + 1 < 3 * r)
+    (hOdd : ∀ Q : SWPoint E, 2 • Q = 0 → Q = 0) :
     Nat.card (SWPoint E) = r :=
-  card_eq_of_prime_witness hrPrime hP hPr (lt_two_mul_of_hasse_of_field_ge_37 hHasse hr hq)
+  card_eq_of_prime_witness_of_lt_three_mul hrPrime hP hPr
+    (lt_of_le_of_lt (card_le_two_mul_card_add_one E) hBound) hOdd
 
 end CompElliptic.CurveOrder
diff --git a/CompElliptic/Curves/Pasta.lean b/CompElliptic/Curves/Pasta.lean
index 871f5da..c4ee51a 100644
--- a/CompElliptic/Curves/Pasta.lean
+++ b/CompElliptic/Curves/Pasta.lean
@@ -6,6 +6,7 @@ Authors: Daira-Emma Hopwood
 -/
 import CompElliptic.CurveForms.ShortWeierstrass
 import CompElliptic.Fields.Pasta
+import CompElliptic.Fields.Residue
 import Mathlib.NumberTheory.LegendreSymbol.Basic
 
 /-!
@@ -129,6 +130,30 @@ theorem no_onCurve_x_zero (y : VestaBaseField) : ¬ OnCurve a b (0, y) := by
   have h' : y ^ 2 = 5 := by simpa [OnCurve, a, b] using h
   exact five_not_isSquare ⟨y, by rw [← h', pow_two]⟩
 
+/-- `-5` is not a cube in the Vesta base field — the cubic analogue of `five_not_isSquare`, and
+what rules out 2-torsion on the Vesta curve.
+
+`3 ∣ q - 1`, so `not_exists_pow_eq_of_pow_ne_one` reduces this to the single power
+`(-5)^((q-1)/3)`, which is not `1`. As for `five_not_isSquare`, `reduce_mod_char` (fast modular
+exponentiation) evaluates it and the kernel re-checks the result. -/
+theorem neg_five_not_isCube : ¬ ∃ x : VestaBaseField, x ^ 3 = -(5 : VestaBaseField) := by
+  have hcard : Fintype.card VestaBaseField = PALLAS_SCALAR_CARD := ZMod.card _
+  refine Fields.not_exists_pow_eq_of_pow_ne_one (n := 3) (by rw [hcard]; decide) (by decide) ?_
+  rw [hcard]
+  -- `reduce_mod_char` keys on the `ZMod` spelling of the type, which the `VestaBaseField` abbrev
+  -- hides; `show` re-exposes it. (The `Field` instances agree — `(inferInstance : Field
+  -- VestaBaseField) = ZMod.instField _` is `rfl` — so this is only about how the goal is written.)
+  show (-(5 : ZMod PALLAS_SCALAR_CARD)) ^ ((PALLAS_SCALAR_CARD - 1) / 3) ≠ 1
+  reduce_mod_char
+  decide
+
+/-- No point on the Vesta curve has `y`-coordinate `0`: that would need `x³ = -5`, and `-5` is not
+a cube (`neg_five_not_isCube`). Equivalently, the Vesta group has no 2-torsion. -/
+theorem no_onCurve_y_zero (x : VestaBaseField) : ¬ OnCurve a b (x, 0) := by
+  intro h
+  have hsum : x ^ 3 + 5 = 0 := by simpa [OnCurve, a, b] using h.symm
+  exact neg_five_not_isCube ⟨x, by linear_combination hsum⟩
+
 -- `(-1, 2)` is on the curve: `2² = 4 = (-1)³ + 5`.
 example : OnCurve a b G := by native_decide
 
diff --git a/CompElliptic/Curves/PastaOrder.lean b/CompElliptic/Curves/PastaOrder.lean
index ed0d2af..85834de 100644
--- a/CompElliptic/Curves/PastaOrder.lean
+++ b/CompElliptic/Curves/PastaOrder.lean
@@ -2,7 +2,7 @@
 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
+Authors: Daira-Emma Hopwood, Gregor Mitscha-Baude
 -/
 import CompElliptic.Curves.Pasta
 import CompElliptic.CurveOrder
@@ -10,15 +10,26 @@ import CompElliptic.CurveOrder
 /-!
 # Orders of the Pasta curve groups (Pallas and Vesta)
 
-Instantiates `CompElliptic.CurveOrder.card_eq_of_hasse_of_field_ge_37` at the two Pasta curves:
-assuming Hasse's bound (`HasseBound`, the one irreducible hypothesis — Mathlib lacks Hasse's
-theorem), the Pallas group has order `PALLAS_SCALAR_CARD` and the Vesta group has order
-`PALLAS_BASE_CARD` (the Pasta cycle: each curve's order is the other's base-field size).
-
-Everything else is discharged outright. The test point `G = (-1, 2)` is the prime-order witness,
-and the witness fact `[order] G = 𝒪` (a `≈ 2^254` scalar multiplication) is a one-line
-`native_decide` now that the `SWPoint` scalar action `•` itself computes in `O(log n)`. The
-field-size facts (`order ∈ hasseInterval (#F)`, `37 ≤ #F`) are concrete closed facts.
+Instantiates the `CompElliptic.CurveOrder` fibre bound at the two Pasta curves, with no assumption:
+the Pallas group has order `PALLAS_SCALAR_CARD` and the Vesta group has order `PALLAS_BASE_CARD`
+(the Pasta cycle: each curve's order is the other's base-field size).
+
+The test point `G = (-1, 2)` is the prime-order witness, and the witness fact `[order] G = 𝒪`
+(a `≈ 2^254` scalar multiplication) is a one-line `native_decide` now that the `SWPoint` scalar
+action `•` itself computes in `O(log n)`. The only *upper* bound needed is the elementary fibre
+bound `#E(F) ≤ 2·#F + 1`; whether it clears the order threshold is decided by a closed comparison
+of the two field sizes, and the Pasta cycle puts the two curves on opposite sides of it:
+
+* **Pallas** — order `q = PALLAS_SCALAR_CARD` over the base field of size `p`, and `p < q`, so
+  `2p + 1 < 2q` outright: `card_eq_of_prime_witness_of_card_lt_two_mul` closes it.
+* **Vesta** — order `p = PALLAS_BASE_CARD` over the base field of size `q`, and `p < q`, so only
+  `2q + 1 < 3p` is available. `#E = 2p` is ruled out separately: a 2-torsion point needs `y = 0`,
+  i.e. `x³ = -5`, which `Pasta.Vesta.no_onCurve_y_zero` forbids.
+
+Per the *Independently re-checkable trust* principle every obligation here is a closed numeric fact
+(`2p + 1 < 2q`, `2q + 1 < 3p`), discharged by kernel `decide`; the only trust is the prime-order
+witnesses (`q_nsmul_Gpt`, `p_nsmul_Gpt`), proved by `native_decide` and appearing in `#print axioms`
+for the two theorems below.
 -/
 
 namespace CompElliptic.Curves.Pasta
@@ -28,42 +39,46 @@ open CompElliptic.CurveForms.ShortWeierstrass CompElliptic.CurveOrder CompEllipt
 namespace Pallas
 
 /-- The test point `(-1, 2)` as a point of the Pallas curve — the prime-order witness. -/
-def Gpt : SWPoint curve := ⟨-1, 2, Or.inl (by native_decide)⟩
+def Gpt : SWPoint curve := ⟨-1, 2, Or.inl (by decide)⟩
 
-theorem Gpt_ne_zero : Gpt ≠ 0 := by native_decide
+theorem Gpt_ne_zero : Gpt ≠ 0 := by decide
 
 /-- `[q] G = 𝒪`, where `q = PALLAS_SCALAR_CARD` is the Pallas group order. -/
-theorem scalarCard_nsmul_Gpt : PALLAS_SCALAR_CARD • Gpt = 0 := by native_decide
+theorem q_nsmul_Gpt : PALLAS_SCALAR_CARD • Gpt = 0 := by native_decide
+
+/-- **The Pallas curve group has order `PALLAS_SCALAR_CARD`**, unconditionally.
 
-/-- **The Pallas curve group has order `PALLAS_SCALAR_CARD`**, assuming Hasse's bound. -/
-theorem card_eq (hHasse : HasseBound curve) :
-    Nat.card (SWPoint curve) = PALLAS_SCALAR_CARD := by
-  refine card_eq_of_hasse_of_field_ge_37 curve PALLAS_SCALAR_is_prime Gpt_ne_zero
-    scalarCard_nsmul_Gpt hHasse ?_ ?_
-  · rw [show Fintype.card PallasBaseField = PALLAS_BASE_CARD from ZMod.card _]
-    simp only [hasseInterval, Set.mem_setOf_eq]; native_decide
-  · rw [show Fintype.card PallasBaseField = PALLAS_BASE_CARD from ZMod.card _]; decide
+The Pallas group order `q` exceeds its base-field size `p`, so the fibre bound `#E ≤ 2p + 1`
+already sits below `2q`, and the prime-order witness `G = (-1, 2)` pins the order outright. -/
+theorem card_eq : Nat.card (SWPoint curve) = PALLAS_SCALAR_CARD := by
+  refine card_eq_of_prime_witness_of_card_lt_two_mul curve PALLAS_SCALAR_is_prime Gpt_ne_zero
+    q_nsmul_Gpt ?_
+  rw [show Fintype.card PallasBaseField = PALLAS_BASE_CARD from ZMod.card _]
+  decide
 
 end Pallas
 
 namespace Vesta
 
 /-- The test point `(-1, 2)` as a point of the Vesta curve — the prime-order witness. -/
-def Gpt : SWPoint curve := ⟨-1, 2, Or.inl (by native_decide)⟩
+def Gpt : SWPoint curve := ⟨-1, 2, Or.inl (by decide)⟩
 
-theorem Gpt_ne_zero : Gpt ≠ 0 := by native_decide
+theorem Gpt_ne_zero : Gpt ≠ 0 := by decide
 
 /-- `[p] G = 𝒪`, where `p = PALLAS_BASE_CARD` is the Vesta group order. -/
-theorem baseCard_nsmul_Gpt : PALLAS_BASE_CARD • Gpt = 0 := by native_decide
+theorem p_nsmul_Gpt : PALLAS_BASE_CARD • Gpt = 0 := by native_decide
+
+/-- **The Vesta curve group has order `PALLAS_BASE_CARD`**, unconditionally.
 
-/-- **The Vesta curve group has order `PALLAS_BASE_CARD`**, assuming Hasse's bound. -/
-theorem card_eq (hHasse : HasseBound curve) :
-    Nat.card (SWPoint curve) = PALLAS_BASE_CARD := by
-  refine card_eq_of_hasse_of_field_ge_37 curve PALLAS_BASE_is_prime Gpt_ne_zero
-    baseCard_nsmul_Gpt hHasse ?_ ?_
+Here the group order `p` is *below* the base-field size `q`, so the fibre bound only gives
+`#E ≤ 2q + 1 < 3p`, leaving `#E = 2p` open. That case needs a point of order 2, which would have
+`y = 0` — impossible by `no_onCurve_y_zero`. -/
+theorem card_eq : Nat.card (SWPoint curve) = PALLAS_BASE_CARD := by
+  refine card_eq_of_prime_witness_of_card_lt_three_mul curve PALLAS_BASE_is_prime Gpt_ne_zero
+    p_nsmul_Gpt ?_ ?_
   · rw [show Fintype.card VestaBaseField = PALLAS_SCALAR_CARD from ZMod.card _]
-    simp only [hasseInterval, Set.mem_setOf_eq]; native_decide
-  · rw [show Fintype.card VestaBaseField = PALLAS_SCALAR_CARD from ZMod.card _]; decide
+    decide
+  · exact fun _ => eq_zero_of_two_nsmul_eq_zero (by decide) no_onCurve_y_zero
 
 end Vesta
 
diff --git a/CompElliptic/Fields/Residue.lean b/CompElliptic/Fields/Residue.lean
new file mode 100644
index 0000000..3cde54e
--- /dev/null
+++ b/CompElliptic/Fields/Residue.lean
@@ -0,0 +1,42 @@
+/-
+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: Gregor Mitscha-Baude
+-/
+import Mathlib.FieldTheory.Finite.Basic
+
+/-!
+# Higher-power residues in a finite field
+
+Mathlib covers *quadratic* residues thoroughly (`ZMod.euler_criterion`, `FiniteField.isSquare_iff`,
+the `LegendreSymbol` hierarchy), but all of that hard-codes the exponent 2; there is no n'th power
+analogue.
+
+We only need the *easy* direction of the residue criterion: a single power that misses 1 certifies
+a non-residue. That direction is a two-line consequence of Fermat's little theorem and needs
+nothing about the structure of `Fˣ`, whereas the converse would need its cyclicity.
+
+This is used to derive the concrete non-residue facts about the Pasta base fields in `Curves.Pasta`
+(`5` is not a square, and `-5` is not a cube in either field).
+-/
+
+namespace CompElliptic.Fields
+
+/-- If `n ∣ #F - 1` and `a ^ ((#F - 1) / n) ≠ 1`, then `a` is not an `n`-th power in `F`.
+
+An `n`-th root `x` of `a` is nonzero along with `a`, so Fermat's little theorem forces
+`a ^ ((#F - 1) / n) = x ^ (n * ((#F - 1) / n)) = x ^ (#F - 1) = 1`. Contrapositively, evaluating
+that one power and finding it is not `1` rules out every root at once. -/
+theorem not_exists_pow_eq_of_pow_ne_one {F : Type*} [Field F] [Fintype F] {n : ℕ} {a : F}
+    (hn : n ∣ Fintype.card F - 1) (ha : a ≠ 0)
+    (h : a ^ ((Fintype.card F - 1) / n) ≠ 1) : ¬ ∃ x : F, x^n = a := by
+  -- `n = 0` is already impossible: the exponent `(#F - 1) / 0` is `0`, so `h` reads `1 ≠ 1`.
+  have hn0 : n ≠ 0 := by rintro rfl; simp at h
+  rintro ⟨x, rfl⟩
+  refine h ?_
+  have hx : x ≠ 0 := by intro hzero; exact ha (by rw [hzero, zero_pow hn0])
+  rw [← pow_mul, Nat.mul_div_cancel' hn]
+  exact FiniteField.pow_card_sub_one_eq_one x hx
+
+end CompElliptic.Fields

From 0950241765f1940470638db3ff964da0b7c6d7f3 Mon Sep 17 00:00:00 2001
From: martyall <martyall@protonmail.com>
Date: Thu, 16 Jul 2026 16:01:17 -0700
Subject: [PATCH 4/4] scripts: teach the field-file generators the absolute
 field names

The absolute-field-names commit renamed the four role aliases to Fp/Fq in
the generated CompElliptic/Fields/Pasta.lean but never updated
scripts/gen_pasta.py, so the generator-reproducibility CI gate failed once
it ran on a PR. field_block gains an optional fielddoc parameter (the
committed file carries docstrings on the field abbrevs; gen_jubjub.py is
unaffected by the default), and gen_pasta.py emits Fp/Fq throughout.

Verified: both gen_pasta.py and gen_jubjub.py reproduce the committed files
byte-identically under PARI/GP.
---
 scripts/gen_pasta.py | 27 +++++++++++++--------------
 scripts/pratt.py     |  6 ++++--
 2 files changed, 17 insertions(+), 16 deletions(-)

diff --git a/scripts/gen_pasta.py b/scripts/gen_pasta.py
index 263bbdf..e2ab959 100644
--- a/scripts/gen_pasta.py
+++ b/scripts/gen_pasta.py
@@ -45,14 +45,9 @@
 
 FOOTER = """\
 
-/-- Vesta base field = Pallas scalar field. -/
-abbrev VestaBaseField := PallasScalarField
-/-- Vesta scalar field = Pallas base field. -/
-abbrev VestaScalarField := PallasBaseField
-
 /-- Tonelli–Shanks data for the Pallas base field `𝔽ₚ`: `p-1 = 2^32 · T`, with `rootOfUnity = 5ᵀ`
 (`pallas.py`). -/
-def pallasBase : TonelliShanks PallasBaseField where
+def pallasBase : TonelliShanks Fp where
   twoAdicity := 32
   oddPart := 0x40000000000000000000000000000000224698fc094cf91b992d30ed
   rootOfUnity := 0x2bce74deac30ebda362120830561f81aea322bf2b7bb7584bdad6fabd87ea32f
@@ -61,11 +56,11 @@ def pallasBase : TonelliShanks PallasBaseField where
 example : (pallasBase.sqrt? 4).map (· ^ 2) = some 4 := by native_decide
 example : pallasBase.sqrt? 5 = none := by native_decide
 -- `√((-1)³ + 5) = √4`: the `y` of the test point `G = (-1, 2)`.
-example : (pallasBase.sqrt? ((-1 : PallasBaseField)^3 + 5)).map (· ^ 2) = some 4 := by native_decide
+example : (pallasBase.sqrt? ((-1 : Fp)^3 + 5)).map (· ^ 2) = some 4 := by native_decide
 
-/-- Tonelli–Shanks data for the Vesta base field `𝔽_q` (`= PallasScalarField`): `q-1 = 2^32 · T`,
+/-- Tonelli–Shanks data for the Vesta base field `𝔽_q` (`= Fq`): `q-1 = 2^32 · T`,
 with `rootOfUnity = 5ᵀ` (`vesta.py`). -/
-def vestaBase : TonelliShanks VestaBaseField where
+def vestaBase : TonelliShanks Fq where
   twoAdicity := 32
   oddPart := 0x40000000000000000000000000000000224698fc0994a8dd8c46eb21
   rootOfUnity := 0x2de6a9b8746d3f589e5c4dfd492ae26e9bb97ea3c106f049a70e2c1102b6d05f
@@ -74,7 +69,7 @@ def vestaBase : TonelliShanks VestaBaseField where
 example : (vestaBase.sqrt? 4).map (· ^ 2) = some 4 := by native_decide
 example : vestaBase.sqrt? 5 = none := by native_decide
 -- `√((-1)³ + 5) = √4`: the `y` of the test point `G = (-1, 2)`.
-example : (vestaBase.sqrt? ((-1 : VestaBaseField)^3 + 5)).map (· ^ 2) = some 4 := by native_decide
+example : (vestaBase.sqrt? ((-1 : Fq)^3 + 5)).map (· ^ 2) = some 4 := by native_decide
 
 end CompElliptic.Fields.Pasta
 """
@@ -82,9 +77,13 @@ def vestaBase : TonelliShanks VestaBaseField where
 
 if __name__ == "__main__":
     out = HEADER
-    out += field_block("PALLAS_BASE", P, "PallasBaseField",
-                       "Pallas base field p (= Vesta scalar field).")
-    out += field_block("PALLAS_SCALAR", Q, "PallasScalarField",
-                       "Pallas scalar field q (= Vesta base field).")
+    out += field_block("PALLAS_BASE", P, "Fp",
+                       "Pallas base field p (= Vesta scalar field).",
+                       fielddoc="The Pallas base field `𝔽ₚ` — also the Vesta scalar field "
+                                "(the Pasta cycle).")
+    out += field_block("PALLAS_SCALAR", Q, "Fq",
+                       "Pallas scalar field q (= Vesta base field).",
+                       fielddoc="The Pallas scalar field `𝔽_q` — also the Vesta base field "
+                                "(the Pasta cycle).")
     out += FOOTER
     print(out, end="")
diff --git a/scripts/pratt.py b/scripts/pratt.py
index 9c61f02..588c6c6 100644
--- a/scripts/pratt.py
+++ b/scripts/pratt.py
@@ -69,11 +69,13 @@ def theorem(name: str, card: int) -> str:
     return f"theorem {name}_is_prime : Nat.Prime {name}_CARD := by\n  unfold {name}_CARD\n{body}"
 
 
-def field_block(name: str, card: int, fieldabbrev: str, doc: str) -> str:
+def field_block(name: str, card: int, fieldabbrev: str, doc: str,
+                fielddoc: str | None = None) -> str:
+    fielddoc_line = f"/-- {fielddoc} -/\n" if fielddoc else ""
     return (
         f"\n-- {doc}\n"
         f"@[reducible] def {name}_CARD : Nat := 0x{card:x}\n\n"
-        f"abbrev {fieldabbrev} := ZMod {name}_CARD\n\n"
+        f"{fielddoc_line}abbrev {fieldabbrev} := ZMod {name}_CARD\n\n"
         f"{theorem(name, card)}\n\n"
         f"instance : Fact (Nat.Prime {name}_CARD) := ⟨{name}_is_prime⟩\n"
         f"instance : Field {fieldabbrev} := ZMod.instField {name}_CARD\n"