From ae6c227a46034059e382326855041712c277e0f2 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Mon, 17 Aug 2026 20:23:45 +0100 Subject: [PATCH 01/11] PastaSSWU.lean: Make the spatial metaphor for applying the isogeny consistent: we map from the iso-curve *across* to the main curve, not *down* to it. (FWIW, for me the iso-curve has always been on the left and the main curve on the right.) The "across" wording is used in `ThreeIsogeny.lean` and in `zcash/ironwood`. Signed-off-by: Daira-Emma Hopwood --- CompElliptic/Hashing/PastaSSWU.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/CompElliptic/Hashing/PastaSSWU.lean b/CompElliptic/Hashing/PastaSSWU.lean index fa2b28b..03d9abe 100644 --- a/CompElliptic/Hashing/PastaSSWU.lean +++ b/CompElliptic/Hashing/PastaSSWU.lean @@ -142,7 +142,7 @@ theorem isSignFunction_sgn0 : IsSignFunction (sgn0 (p := PALLAS_BASE_CARD)) := CompElliptic.Hashing.isSignFunction_sgn0 (Nat.odd_iff.mpr (by decide)) /-- The deployed `map_to_curve` for Pallas: simplified SWU onto iso-Pallas, -then the 3-isogeny down to Pallas. -/ +then the 3-isogeny across to Pallas. -/ def mapToCurve (u : PallasBaseField) : SWPoint curve := iso.map (sswu.map u) @@ -189,7 +189,7 @@ add on the iso-curve, apply the isogeny once. -/ def mapHashOutputsToCurve (u₀ u₁ : PallasBaseField) : SWPoint curve := iso.mapHashOutputsToCurve sswu.map u₀ u₁ -/-- The construction agrees with mapping each point down and adding on +/-- The construction agrees with mapping each point across and adding on Pallas — the order `zcash-test-vectors` and `pasta_curves` use — by the homomorphism. -/ theorem mapHashOutputsToCurve_eq (u₀ u₁ : PallasBaseField) : @@ -329,7 +329,7 @@ theorem isSignFunction_sgn0 : IsSignFunction (sgn0 (p := PALLAS_SCALAR_CARD)) := CompElliptic.Hashing.isSignFunction_sgn0 (Nat.odd_iff.mpr (by decide)) /-- The deployed `map_to_curve` for Vesta: simplified SWU onto iso-Vesta, -then the 3-isogeny down to Vesta. -/ +then the 3-isogeny across to Vesta. -/ def mapToCurve (u : VestaBaseField) : SWPoint curve := iso.map (sswu.map u) @@ -376,7 +376,7 @@ add on the iso-curve, apply the isogeny once. -/ def mapHashOutputsToCurve (u₀ u₁ : VestaBaseField) : SWPoint curve := iso.mapHashOutputsToCurve sswu.map u₀ u₁ -/-- The construction agrees with mapping each point down and adding on +/-- The construction agrees with mapping each point across and adding on Vesta — the order `zcash-test-vectors` and `pasta_curves` use — by the homomorphism. -/ theorem mapHashOutputsToCurve_eq (u₀ u₁ : VestaBaseField) : From 62d6ece9182b7b7da3950aeb3c75e530c5da6c48 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Tue, 18 Aug 2026 15:49:24 -0300 Subject: [PATCH 02/11] CurveCycle.lean: a 2-cycle of curves shares its CM discriminant The two curves of a 2-cycle cannot be chosen independently. Adding the two point-counting equations forces t1 + t2 = 2, and substituting t2 = 2 - t1 gives t2^2 - 4*#F2 = t1^2 - 4*#F1: the two Frobenius discriminants are equal as integers, not merely up to squares, so both curves have CM by an order in the same imaginary quadratic field. This is Proposition 6.1 of Chiesa, Chua and Weidner (SIAM J. Appl. Algebra Geom. 3(2), 2019), restated as Proposition 3.3(iv) of Belles-Munoz, Jimenez Urroz and Silva (ia.cr/2022/1662). The proof is integer algebra over the two point counts and says nothing about endomorphism rings, so it needs neither Hasse nor any arithmetic geometry; the trace is defined by counting for the same reason. The order the discriminant is a shadow of is defined rather than described: frobCharPoly is X^2 - t*X + #F, frobeniusOrder is the quotient by it (which is Z[pi]), frobeniusElt is the class of X (which is pi), and frobeniusElt_charEq is the characteristic equation. That lets the conclusion be stated where it belongs, as an isomorphism of rings rather than an equality of integers: frobeniusOrderEquiv sends pi_1 to pi_2 + (t_1 - 1), which is a ring map exactly because the traces sum to 2, and its mirror image inverts it. The geometric pi is not defined, since as an endomorphism it acts on points over extensions of the base field and is the identity on the rational points alone. Instantiated at the Pasta cycle from the orders already pinned in Curves/PastaOrder.lean: the shared discriminant is -3 * V^2 with V = 0x93cd3a2c8198e2690c7c095a00000001, so the CM field is Q(sqrt(-3)). That is the field behind the j = 0 case, though sharing it does not by itself force j = 0 (an order of conductor f > 1 has other j-invariants); what the Pasta search additionally fixed, by taking |D| = 3 and reading off six twists per prime, is the maximal order. The general theorems rest on the standard axioms only, and the Pasta corollaries inherit the two prime-order witnesses; both tiers are registered in TrustBoundary.lean. Co-Authored-By: Claude Opus 5 (1M context) --- CompElliptic.lean | 1 + CompElliptic/CurveCycle.lean | 379 ++++++++++++++++++++++++++++++++ CompElliptic/TrustBoundary.lean | 19 ++ 3 files changed, 399 insertions(+) create mode 100644 CompElliptic/CurveCycle.lean diff --git a/CompElliptic.lean b/CompElliptic.lean index 47774e4..428852c 100644 --- a/CompElliptic.lean +++ b/CompElliptic.lean @@ -15,6 +15,7 @@ import CompElliptic.Fields.Residue import CompElliptic.Fields.Sqrt import CompElliptic.CurveForms.ShortWeierstrass import CompElliptic.CurveOrder +import CompElliptic.CurveCycle import CompElliptic.Isogenies.ThreeIsogeny import CompElliptic.Curves.Pasta import CompElliptic.Curves.IsoPasta diff --git a/CompElliptic/CurveCycle.lean b/CompElliptic/CurveCycle.lean new file mode 100644 index 0000000..3b0f2d8 --- /dev/null +++ b/CompElliptic/CurveCycle.lean @@ -0,0 +1,379 @@ +/- +Copyright (c) 2026 CompElliptic Contributors. +Released under the Apache License, Version 2.0, or the MIT license, at your option, +as described in the files LICENSE-APACHE and LICENSE-MIT. +Authors: Danny Willems +-/ +import CompElliptic.Curves.PastaOrder +import Mathlib.Algebra.Squarefree.Basic +import Mathlib.RingTheory.Int.Basic +import Mathlib.RingTheory.AdjoinRoot +import Mathlib.Algebra.QuadraticDiscriminant + +/-! +# A 2-cycle of curves shares its CM discriminant + +The two curves of a cycle cannot be chosen independently: fixing one constrains the other so +tightly that both end up with Complex Multiplication by an order in the *same* imaginary +quadratic field. That is the fact usually quoted to explain why the Pasta curves have +`j`-invariant `0`, and it is the only half of that explanation which is a theorem; the other +half (that a cycle is only *findable* when the discriminant is small) is a statement about the +construction methods we know, not about what exists. + +## The argument + +Everything follows from *counting alone*. Write the trace of Frobenius by definition rather +than by any structure theory, + +`t(E) = #F + 1 - #E(F)`, + +and let `frobDisc E = t(E)² - 4·#F`. If `E₁/F₁` and `E₂/F₂` form a 2-cycle, meaning +`#E₁(F₁) = #F₂` and `#E₂(F₂) = #F₁`, then the two counting equations read +`#F₂ = #F₁ + 1 - t₁` and `#F₁ = #F₂ + 1 - t₂`. Adding them cancels the field sizes and leaves +`t₁ + t₂ = 2` (`trace_add_trace`), and substituting `t₂ = 2 - t₁` gives + +`t₂² - 4·#F₂ = (2 - t₁)² - 4(#F₁ + 1 - t₁) = t₁² - 4·#F₁`, + +which is `frobDisc_eq`: the two Frobenius discriminants are equal *as integers*, not merely up +to squares. Every invariant read off that integer therefore agrees, in particular the CM field +`ℚ(√(t² - 4·#F))`, its fundamental discriminant, and the conductor of the Frobenius order +(`cm_invariant_eq`, `hasCMDiscriminant_congr`). + +## The order `ℤ[π]`, as a definition + +Since the discriminant is only a shadow of the ring it comes from, that ring is defined too: +`frobCharPoly` is `X² - t·X + #F`, `frobeniusOrder` is `ℤ[X]/(frobCharPoly)`, which is `ℤ[π]`, +`frobeniusElt` is the class of `X`, which is `π`, and `frobeniusElt_charEq` is its defining +relation. The cycle statement then strengthens from an equality of integers to an isomorphism +of rings, `frobeniusOrderEquiv : ℤ[π₁] ≃ₐ[ℤ] ℤ[π₂]`, given explicitly by `π₁ ↦ π₂ + (t₁ - 1)`. +That is the form to reuse: it survives any later change of how the discriminant is packaged, +and it is what "the same order" actually means. + +## What is and is not assumed + +No arithmetic geometry enters, and in particular neither Hasse's theorem (which Mathlib lacks +for `WeierstrassCurve`) nor any theorem about endomorphism rings. The identity is an integer +computation over the two point counts, so it holds for *any* pair of curves satisfying the +cycle equations, ordinary or not. Ordinariness is what makes the shared integer meaningful as +a CM discriminant: for an ordinary curve the endomorphism ring is the order of discriminant +`t² - 4·#F` in an imaginary quadratic field, whereas for a supersingular curve the same integer +is not the discriminant of `End(E)`. The statement proved here is deliberately the +count-level one, which is the part the cycle forces. + +## Provenance + +This is Proposition 6.1 of Alessandro Chiesa, Lynn Chua and Matthew Weidner, *On cycles of +pairing-friendly elliptic curves*, SIAM J. Appl. Algebra Geom. 3(2):175-192, 2019 +(arXiv:1803.02067), restated as Proposition 3.3(iv) of Marta Bellés-Muñoz, Jorge Jiménez Urroz +and Javier Silva, *Revisiting cycles of pairing-friendly elliptic curves*, CRYPTO 2023 +(ia.cr/2022/1662). The proof there is the same three lines; this module mechanises it, and adds +the Pasta instance below. + +Both papers state the discriminant with the opposite sign, as the squarefree part of +`4·#F - t²`, which is positive by Hasse; the sign convention here is the one under which the +discriminant is that of the order `ℤ[π]`, so `D = -3` below is their `D = 3`. + +## The Pasta instance + +`Pasta.isCycle₂` feeds the Pallas and Vesta group orders (`Curves.Pasta.Pallas.card_eq` and +`Curves.Pasta.Vesta.card_eq`) into the general theorem, and `Pasta.frobDisc_pallas` +exhibits the shared discriminant explicitly: + +`t² - 4p = -3 · V²`, with `V = 0x93cd3a2c8198e2690c7c095a00000001`, + +so the fundamental discriminant is `D = -3` and the CM field is `ℚ(√-3)`. That is exactly the +`j = 0` case, which is why both curves have the form `y² = x³ + b` and why Simplified SWU +(needing `a ≠ 0`) has to detour through an isogenous curve. Note also that `V ≡ 1 (mod 2³²)`, +the 2-adicity that the search was steering for. +-/ + +namespace CompElliptic.CurveCycle + +open CompElliptic.CurveForms.ShortWeierstrass + +/-! ## Trace and Frobenius discriminant, by counting -/ + +section Defs + +variable {F : Type*} [Field F] [Fintype F] + +/-- The **trace of Frobenius** of `E/F`, *defined* as `#F + 1 - #E(F)` rather than as an +eigenvalue: this is the only property of the trace any statement below uses, and taking it as +the definition keeps the module free of arithmetic geometry. -/ +noncomputable def trace (E : SWCurve F) : ℤ := (Fintype.card F : ℤ) + 1 - (Nat.card (SWPoint E) : ℤ) + +/-- The **Frobenius discriminant** `t² - 4·#F` of `E/F`, i.e. the discriminant of the +characteristic polynomial `X² - tX + #F` of Frobenius. + +Unfolding the `ℤ[π]` this module keeps referring to, since it is not obvious: `π` is the +Frobenius endomorphism `(x, y) ↦ (x^#F, y^#F)` of `E`. It is an endomorphism because raising to +the `#F`-th power is a field homomorphism in characteristic `p`, and its fixed points are +exactly the rational points, `E(F) = ker (π - 1)`, because `x^#F = x` holds iff `x ∈ F`. Now +`End E` is a ring (add pointwise, multiply by composing) containing `ℤ` as the +multiplication-by-`n` maps, and `ℤ[π] = {a + b·π}` is the subring `π` generates over it. There +Frobenius satisfies `π² - t·π + #F = 0`, which is also where the counting definition of `t` +comes from (`#E(F) = deg (1 - π) = #F + 1 - t`), so + +`ℤ[π] ≅ ℤ[X]/(X² - tX + #F)`, + +and the integer defined here is the discriminant of *that* quadratic ring: `frobDisc E` is +`disc (ℤ[π])` on the nose, not an analogue of one. + +For an ordinary curve `π ∉ ℤ` and `t² - 4·#F < 0` by Hasse, so `ℤ[π]` is an order in the +imaginary quadratic field `K = ℚ(π) = ℚ(√(t² - 4·#F))`, sitting in a chain of orders +`ℤ[π] ⊆ End E ⊆ 𝒪_K`. Its squarefree part is then what the literature calls the curve's CM +discriminant, and writing `t² - 4·#F = D·f²` with `D` fundamental makes `f` the conductor of +`ℤ[π]` (the conductor of `End E` divides it, and can be smaller: that is exactly the gap +between "has CM by an order in `ℚ(√-3)`" and "has `j = 0`", see `Pasta.frobDisc_pallas`). + +`ℤ[π]` is not left as prose: `frobeniusOrder` below *is* that ring, `frobeniusElt` is its `π`, +and `frobeniusElt_charEq` is the relation above. The cycle theorem is then available in two +forms, as the integer identity `frobDisc_eq` and as the ring isomorphism +`frobeniusOrderEquiv`. -/ +noncomputable def frobDisc (E : SWCurve F) : ℤ := trace E ^ 2 - 4 * (Fintype.card F : ℤ) + +/-- `D` is a **CM discriminant** of `E` when the Frobenius discriminant is `D` times a square +with `D` squarefree, i.e. `D` is the squarefree part of `t² - 4·#F`. -/ +def HasCMDiscriminant (E : SWCurve F) (D : ℤ) : Prop := + Squarefree D ∧ ∃ f : ℤ, frobDisc E = D * f ^ 2 + +end Defs + +/-! ## `ℤ[π]` as a definition, not only as a comment -/ + +section FrobeniusOrder + +open Polynomial + +variable {F : Type*} [Field F] [Fintype F] + +/-- The **characteristic polynomial of Frobenius**, `X² - t·X + #F`, over `ℤ`. -/ +noncomputable def frobCharPoly (E : SWCurve F) : ℤ[X] := + X ^ 2 - C (trace E) * X + C (Fintype.card F : ℤ) + +theorem frobCharPoly_monic (E : SWCurve F) : (frobCharPoly E).Monic := by + unfold frobCharPoly + monicity! + +/-- `frobDisc` is the discriminant of that quadratic, in Mathlib's `discrim` sense. -/ +theorem frobDisc_eq_discrim (E : SWCurve F) : + frobDisc E = discrim 1 (-trace E) (Fintype.card F : ℤ) := by + simp only [frobDisc, discrim] + ring + +/-- The **Frobenius order** `ℤ[π] = ℤ[X]/(X² - t·X + #F)` of `E`. + +This is the abstract form of the ring the comments above describe. The geometric `π` itself is +not available here: as an endomorphism it acts on points over extensions of `F`, and on `E(F)` +alone it is the identity (`x^(#F) = x`), so nothing would be gained by defining it on `SWPoint`. +For an ordinary curve the ring below is genuinely `ℤ[π] ⊆ End E`, by the characteristic equation +`π² - t·π + #F = 0`. -/ +abbrev frobeniusOrder (E : SWCurve F) : Type := AdjoinRoot (frobCharPoly E) + +/-- The formal Frobenius: the image of `X` in `ℤ[X]/(X² - t·X + #F)`. -/ +noncomputable def frobeniusElt (E : SWCurve F) : frobeniusOrder E := AdjoinRoot.root _ + +theorem frobeniusElt_def (E : SWCurve F) : + frobeniusElt E = AdjoinRoot.root (frobCharPoly E) := rfl + +/-- **The characteristic equation**, `π² - t·π + #F = 0`, holding in `ℤ[π]` by construction. -/ +theorem frobeniusElt_charEq (E : SWCurve F) : + frobeniusElt E ^ 2 - (trace E : frobeniusOrder E) * frobeniusElt E + + ((Fintype.card F : ℤ) : frobeniusOrder E) = 0 := by + have h : AdjoinRoot.mk (frobCharPoly E) (frobCharPoly E) = 0 := AdjoinRoot.mk_self + rw [frobCharPoly] at h + simp only [map_add, map_sub, map_mul, map_pow, AdjoinRoot.mk_X, AdjoinRoot.mk_C] at h + simpa [frobeniusElt] using h + +end FrobeniusOrder + +/-! ## The cycle condition -/ + +section Cycle + +open Polynomial + +variable {F₁ F₂ : Type*} [Field F₁] [Fintype F₁] [Field F₂] [Fintype F₂] + {E₁ : SWCurve F₁} {E₂ : SWCurve F₂} + +/-- `E₁/F₁` and `E₂/F₂` form a **2-cycle**: each curve's group order is the other's field size. +(The Pasta cycle: `#Pallas(𝔽_p) = q` and `#Vesta(𝔽_q) = p`.) -/ +structure IsCycle₂ (E₁ : SWCurve F₁) (E₂ : SWCurve F₂) : Prop where + /-- The first curve's group order is the second curve's field size. -/ + card_fst : Nat.card (SWPoint E₁) = Fintype.card F₂ + /-- The second curve's group order is the first curve's field size. -/ + card_snd : Nat.card (SWPoint E₂) = Fintype.card F₁ + +/-- A 2-cycle read the other way round is again a 2-cycle. -/ +theorem IsCycle₂.symm (h : IsCycle₂ E₁ E₂) : IsCycle₂ E₂ E₁ := + ⟨h.card_snd, h.card_fst⟩ + +/-- **The traces of a 2-cycle sum to `2`.** Adding the two counting equations +`#F₂ = #F₁ + 1 - t₁` and `#F₁ = #F₂ + 1 - t₂` cancels both field sizes. + +This is the whole content of the cycle condition; `frobDisc_eq` is then substitution. -/ +theorem trace_add_trace (h : IsCycle₂ E₁ E₂) : trace E₁ + trace E₂ = 2 := by + simp only [trace, h.card_fst, h.card_snd] + ring + +/-- The second trace is determined by the first, `t₂ = 2 - t₁`. -/ +theorem trace_snd (h : IsCycle₂ E₁ E₂) : trace E₂ = 2 - trace E₁ := by + have := trace_add_trace h + linarith + +/-- **The two curves of a 2-cycle have equal Frobenius discriminants**, as integers: + +`t₂² - 4·#F₂ = (2 - t₁)² - 4(#F₁ + 1 - t₁) = t₁² - 4·#F₁`. + +Chiesa-Chua-Weidner, Proposition 6.1. Note the conclusion is stronger than the usual phrasing +"the same CM discriminant", which compares only squarefree parts. -/ +theorem frobDisc_eq (h : IsCycle₂ E₁ E₂) : frobDisc E₁ = frobDisc E₂ := by + simp only [frobDisc, trace, h.card_fst, h.card_snd] + ring + +/-! ### The two Frobenius orders are isomorphic + +`frobDisc_eq` says the two orders `ℤ[π₁]` and `ℤ[π₂]` have the same discriminant. Since both are +quadratic orders in the same field, that already forces them to be the *same* order, and the +isomorphism is explicit: inside `K`, `π₁ = (t₁ + √D)/2` and `π₂ = (t₂ + √D)/2` differ by the +integer `(t₁ - t₂)/2 = t₁ - 1`, using `t₁ + t₂ = 2`. So `π₁ ↦ π₂ + (t₁ - 1)` is a ring map, and +its mirror image is its inverse. This is the statement to reuse: it is strictly stronger than +equality of discriminants, and it needs no square roots to state. -/ + +/-- `π₂ + (t₁ - 1)` is a root of `E₁`'s characteristic polynomial, which is what makes +`frobeniusOrderHom` well defined. -/ +theorem aeval_frobCharPoly_shift (h : IsCycle₂ E₁ E₂) : + aeval (frobeniusElt E₂ + ((trace E₁ - 1 : ℤ) : frobeniusOrder E₂)) (frobCharPoly E₁) = 0 := by + have ht₁ : trace E₁ = (Fintype.card F₁ : ℤ) + 1 - (Fintype.card F₂ : ℤ) := by + simp [trace, h.card_fst] + have ht₂ : trace E₂ = (Fintype.card F₂ : ℤ) + 1 - (Fintype.card F₁ : ℤ) := by + simp [trace, h.card_snd] + have hrel := frobeniusElt_charEq E₂ + rw [ht₂] at hrel + -- Reduce `aeval` first: rewriting `C` into a cast before that would leave `aeval` stuck on the + -- coefficients. + simp only [frobCharPoly, ht₁, map_add, map_sub, map_mul, map_pow, aeval_X, aeval_C] + simp only [eq_intCast] + push_cast at hrel ⊢ + linear_combination hrel + +/-- **`π₁ ↦ π₂ + (t₁ - 1)`**, the comparison map between the two Frobenius orders of a 2-cycle. -/ +noncomputable def frobeniusOrderHom (h : IsCycle₂ E₁ E₂) : + frobeniusOrder E₁ →ₐ[ℤ] frobeniusOrder E₂ := + AdjoinRoot.liftAlgHom _ (Algebra.ofId ℤ (frobeniusOrder E₂)) + (frobeniusElt E₂ + ((trace E₁ - 1 : ℤ) : frobeniusOrder E₂)) + (aeval_frobCharPoly_shift h) + +@[simp] +theorem frobeniusOrderHom_frobeniusElt (h : IsCycle₂ E₁ E₂) : + frobeniusOrderHom h (frobeniusElt E₁) + = frobeniusElt E₂ + ((trace E₁ - 1 : ℤ) : frobeniusOrder E₂) := + AdjoinRoot.liftAlgHom_root _ _ _ _ + +/-- **The two curves of a 2-cycle have isomorphic Frobenius orders**, `ℤ[π₁] ≃ ℤ[π₂]`, by the +generator shift above in both directions: the round trip moves the generator by +`(t₁ - 1) + (t₂ - 1)`, which is `0` by `trace_add_trace`. -/ +noncomputable def frobeniusOrderEquiv (h : IsCycle₂ E₁ E₂) : + frobeniusOrder E₁ ≃ₐ[ℤ] frobeniusOrder E₂ := + AlgEquiv.ofAlgHom (frobeniusOrderHom h) (frobeniusOrderHom h.symm) + (by + have h2 : ((trace E₁ : frobeniusOrder E₂)) + (trace E₂ : frobeniusOrder E₂) = 2 := by + exact_mod_cast congrArg (fun n : ℤ => (n : frobeniusOrder E₂)) (trace_add_trace h) + ext + simp only [AlgHom.comp_apply, AlgHom.coe_id, id_eq, ← frobeniusElt_def, + frobeniusOrderHom_frobeniusElt, map_add, map_intCast] + push_cast + linear_combination h2) + (by + have h2 : ((trace E₁ : frobeniusOrder E₁)) + (trace E₂ : frobeniusOrder E₁) = 2 := by + exact_mod_cast congrArg (fun n : ℤ => (n : frobeniusOrder E₁)) (trace_add_trace h) + ext + simp only [AlgHom.comp_apply, AlgHom.coe_id, id_eq, ← frobeniusElt_def, + frobeniusOrderHom_frobeniusElt, map_add, map_intCast] + push_cast + linear_combination h2) + +/-- Every invariant computed from the Frobenius discriminant agrees across a 2-cycle: the CM +field, the fundamental discriminant, the squarefree part, the conductor of `ℤ[π]`. The integers +themselves coincide (`frobDisc_eq`), so this is a congruence; it is recorded because the +literature states the shared quantity as one of these derived invariants. -/ +theorem cm_invariant_eq {α : Type*} (f : ℤ → α) (h : IsCycle₂ E₁ E₂) : + f (frobDisc E₁) = f (frobDisc E₂) := + congrArg f (frobDisc_eq h) + +/-- **The CM discriminant is shared**: a squarefree `D` is a CM discriminant of one curve of a +2-cycle exactly when it is one of the other. No uniqueness of squarefree parts is needed, since +the two discriminants are the same integer. -/ +theorem hasCMDiscriminant_congr (h : IsCycle₂ E₁ E₂) {D : ℤ} : + HasCMDiscriminant E₁ D ↔ HasCMDiscriminant E₂ D := by + simp only [HasCMDiscriminant, frobDisc_eq h] + +end Cycle + +/-! ## The Pasta cycle: the shared discriminant is `-3`, i.e. `j = 0` -/ + +namespace Pasta + +open CompElliptic.Curves.Pasta CompElliptic.Fields.Pasta + +/-- The Pallas base field has `PALLAS_BASE_CARD` elements. -/ +theorem card_pallasBaseField : Fintype.card PallasBaseField = PALLAS_BASE_CARD := ZMod.card _ + +/-- The Vesta base field has `PALLAS_SCALAR_CARD` elements. -/ +theorem card_vestaBaseField : Fintype.card VestaBaseField = PALLAS_SCALAR_CARD := ZMod.card _ + +/-- **Pallas and Vesta form a 2-cycle**: `#Pallas(𝔽_p) = q = #𝔽_q` and `#Vesta(𝔽_q) = p = #𝔽_p`, +from the two unconditional order computations in `Curves.PastaOrder`. -/ +theorem isCycle₂ : IsCycle₂ Pallas.curve Vesta.curve where + card_fst := by rw [Pallas.card_eq, card_vestaBaseField] + card_snd := by rw [Vesta.card_eq, card_pallasBaseField] + +/-- The Pallas trace of Frobenius, `t = p + 1 - q`. -/ +theorem trace_pallas : trace Pallas.curve = -86663725065984043395317759 := by + simp only [trace, Pallas.card_eq, card_pallasBaseField] + decide + +/-- The Vesta trace, `2 - t`, as `trace_snd` predicts. -/ +theorem trace_vesta : trace Vesta.curve = 86663725065984043395317761 := by + rw [trace_snd isCycle₂, trace_pallas] + decide + +/-- **The Pasta cycle's shared Frobenius discriminant is `-3 · V²`** with +`V = 0x93cd3a2c8198e2690c7c095a00000001`, so the CM field is `ℚ(√-3)`. Equivalently +`4p = t² + 3V²`, the CM norm equation at `|D| = 3` that the Pasta search solved. + +Sharing the field is not by itself `j = 0`: an order of conductor `f > 1` in `ℚ(√-3)` has other +`j`-invariants. What a cycle forces is the field; what the search additionally fixed, by taking +`|D| = 3` and reading off the six twists per prime, is the *maximal* order `ℤ[ζ₃]`, whose extra +automorphisms are the `j = 0` ones. Pallas and Vesta are `y² = x³ + 5`, so they do realise it. -/ +theorem frobDisc_pallas : + frobDisc Pallas.curve = -3 * 196462116142286827589391630752301449217 ^ 2 := by + simp only [frobDisc, trace_pallas, card_pallasBaseField] + decide + +/-- `-3` is squarefree, as an integer. -/ +theorem squarefree_neg_three : Squarefree (-3 : ℤ) := + (Int.prime_iff_natAbs_prime.mpr (by decide)).irreducible.squarefree + +/-- Vesta's Frobenius discriminant, which by `frobDisc_eq` is the same integer as Pallas's. -/ +theorem frobDisc_vesta : + frobDisc Vesta.curve = -3 * 196462116142286827589391630752301449217 ^ 2 := + (frobDisc_eq isCycle₂).symm.trans frobDisc_pallas + +/-- **The Pasta CM discriminant is `-3`**, by the explicit factorisation above. -/ +theorem hasCMDiscriminant_pallas : HasCMDiscriminant Pallas.curve (-3) := + ⟨squarefree_neg_three, 196462116142286827589391630752301449217, frobDisc_pallas⟩ + +/-- The same for Vesta, obtained by transport along the cycle rather than by recounting. -/ +theorem hasCMDiscriminant_vesta : HasCMDiscriminant Vesta.curve (-3) := + (hasCMDiscriminant_congr isCycle₂).mp hasCMDiscriminant_pallas + +/-- **The two Pasta Frobenius orders are the same order**, `ℤ[π_Pallas] ≃ ℤ[π_Vesta]`, by the +generator shift `π_Pallas ↦ π_Vesta + (t - 1)`. -/ +noncomputable def frobeniusOrderEquiv : + frobeniusOrder Pallas.curve ≃ₐ[ℤ] frobeniusOrder Vesta.curve := + CurveCycle.frobeniusOrderEquiv isCycle₂ + +end Pasta + +end CompElliptic.CurveCycle diff --git a/CompElliptic/TrustBoundary.lean b/CompElliptic/TrustBoundary.lean index fc6cb6d..dccbd12 100644 --- a/CompElliptic/TrustBoundary.lean +++ b/CompElliptic/TrustBoundary.lean @@ -5,6 +5,7 @@ as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood -/ import CompElliptic.Curves.PastaOrder +import CompElliptic.CurveCycle import CompElliptic.Hashing.PastaSSWU import CompElliptic.Curves.Pasta.Fast.Projective import CompElliptic.Curves.Pasta.Fast.Msm @@ -48,6 +49,11 @@ open CompElliptic.Meta assert_axioms CompElliptic.CurveOrder.card_fibre_le_two assert_axioms CompElliptic.CurveOrder.card_eq_of_prime_witness_of_card_lt_two_mul assert_axioms CompElliptic.CurveOrder.card_eq_of_prime_witness_of_card_lt_three_mul +assert_axioms CompElliptic.CurveCycle.trace_add_trace +assert_axioms CompElliptic.CurveCycle.frobDisc_eq +assert_axioms CompElliptic.CurveCycle.hasCMDiscriminant_congr +assert_axioms CompElliptic.CurveCycle.frobeniusElt_charEq +assert_axioms CompElliptic.CurveCycle.frobeniusOrderEquiv assert_axioms CompElliptic.Fields.TonelliShanks.sqrt?_mul_self assert_axioms CompElliptic.Fields.TonelliShanks.sqrt?_isSome_of_isSquare @@ -90,6 +96,19 @@ assert_axioms CompElliptic.Curves.Pasta.Pallas.card_eq +native( CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt) assert_axioms CompElliptic.Curves.Pasta.Vesta.card_eq +native( CompElliptic.Curves.Pasta.Vesta.p_nsmul_Gpt) +assert_axioms CompElliptic.CurveCycle.Pasta.isCycle₂ +native( + CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt, + CompElliptic.Curves.Pasta.Vesta.p_nsmul_Gpt) +assert_axioms CompElliptic.CurveCycle.Pasta.frobDisc_pallas +native( + CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt) +assert_axioms CompElliptic.CurveCycle.Pasta.hasCMDiscriminant_pallas +native( + CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt) +assert_axioms CompElliptic.CurveCycle.Pasta.hasCMDiscriminant_vesta +native( + CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt, + CompElliptic.Curves.Pasta.Vesta.p_nsmul_Gpt) +assert_axioms CompElliptic.CurveCycle.Pasta.frobeniusOrderEquiv +native( + CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt, + CompElliptic.Curves.Pasta.Vesta.p_nsmul_Gpt) assert_axioms CompElliptic.Curves.Pasta.Pallas.q_nsmul_isoGpt +native( CompElliptic.Curves.Pasta.Pallas.q_nsmul_isoGpt) assert_axioms CompElliptic.Curves.Pasta.Vesta.p_nsmul_isoGpt +native( From d0dca0012381bbe83a7b185d13303f50e113bc79 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Tue, 18 Aug 2026 16:53:54 -0300 Subject: [PATCH 03/11] CurveCycle.lean: correct what ordinariness does and does not buy The module doc claimed that for an ordinary curve End(E) is the order of discriminant t^2 - 4*#F, and that for a supersingular curve that integer is not the discriminant of End(E). Both halves are wrong, and the first contradicts frobDisc's own docstring three paragraphs later. It is Z[pi], not End(E), that has discriminant t^2 - 4*#F. For an ordinary curve End(E) is an order in the right imaginary quadratic field but the inclusion Z[pi] subset End(E) can be strict, and Pasta is exactly such a case: disc Z[pi] = -3*V^2 while End = Z[zeta_3] has discriminant -3. Claiming equality there would have contradicted the j = 0 discussion in the same file. For a supersingular curve it is the GEOMETRIC endomorphism ring that is a maximal order in a quaternion algebra, hence has no quadratic discriminant to compare with; the F-rational endomorphisms can still form a quadratic order, over F_p an order in Q(sqrt(-p)) by Waterhouse's classification. The degenerate case t = +-2p over F_(p^2) is worth naming too, since there the integer is 0 and pi is already an integer. Also states the definition the paragraph was leaning on without giving: ordinary means p does not divide t, supersingular means it does. Co-Authored-By: Claude Opus 5 (1M context) --- CompElliptic/CurveCycle.lean | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/CompElliptic/CurveCycle.lean b/CompElliptic/CurveCycle.lean index 3b0f2d8..76f3798 100644 --- a/CompElliptic/CurveCycle.lean +++ b/CompElliptic/CurveCycle.lean @@ -54,11 +54,25 @@ and it is what "the same order" actually means. No arithmetic geometry enters, and in particular neither Hasse's theorem (which Mathlib lacks for `WeierstrassCurve`) nor any theorem about endomorphism rings. The identity is an integer computation over the two point counts, so it holds for *any* pair of curves satisfying the -cycle equations, ordinary or not. Ordinariness is what makes the shared integer meaningful as -a CM discriminant: for an ordinary curve the endomorphism ring is the order of discriminant -`t² - 4·#F` in an imaginary quadratic field, whereas for a supersingular curve the same integer -is not the discriminant of `End(E)`. The statement proved here is deliberately the -count-level one, which is the part the cycle forces. +cycle equations, ordinary or not. + +What ordinariness buys is only the *reading* of the shared integer, never the identity. In all +cases `t² - 4·#F` is the discriminant of `ℤ[π]` (see `frobDisc`). A curve is **ordinary** when +the characteristic `p` does not divide `t` and **supersingular** when it does; over a prime +field with `p > 3` supersingular means exactly `t = 0`. Then: + +* ordinary: `End E` is an order in the imaginary quadratic field `ℚ(√(t² - 4·#F))`, so the + integer is a discriminant *in the right field*, but not necessarily `End E`'s own, because + `ℤ[π] ⊆ End E` can be strict. Pasta is such a case: `disc ℤ[π] = -3·V²` while + `End = ℤ[ζ₃]` has discriminant `-3`. +* supersingular: the geometric endomorphism ring is a maximal order in a quaternion algebra, + noncommutative and of rank `4`, so it has no quadratic discriminant to compare with. The + `F`-rational endomorphisms can still form a quadratic order (over `𝔽_p` an order in + `ℚ(√-p)`, by Waterhouse's classification), and over `𝔽_(p²)` with `t = ±2p` the integer + degenerates to `0` because `π = ±p` is already an integer. + +The statement proved here is deliberately the count-level one, which is the part the cycle +forces. ## Provenance From c76f7e8bf6b9e8f6f366a56b0292f99c7f90334f Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 19 Aug 2026 09:54:07 -0300 Subject: [PATCH 04/11] CurveCycle.lean: document the three declarations that had no docstring frobCharPoly_monic, frobeniusElt_def and frobeniusOrderHom_frobeniusElt were stated bare. Each now says why it exists, per the convention that a declaration which cannot be justified probably should not exist. The honest case is frobCharPoly_monic, which nothing here consumes: it is recorded because monicity is what makes the quotient Z-free on {1, pi}, so frobeniusOrder is an order (a rank-2 lattice) rather than an arbitrary quotient ring, and it is the standing hypothesis of the AdjoinRoot lemmas that a later basis or discriminant computation would open with. The other two are load-bearing and now say where: frobeniusElt_def exists so simp can FOLD root back into frobeniusElt (simp cannot refold a definition by name), which is what the round-trip goals of frobeniusOrderEquiv need after ext; and frobeniusOrderHom_frobeniusElt is the value on the generator, which by AdjoinRoot.algHom_ext is the only fact about the map any proof needs. Co-Authored-By: Claude Opus 5 (1M context) --- CompElliptic/CurveCycle.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/CompElliptic/CurveCycle.lean b/CompElliptic/CurveCycle.lean index 76f3798..ca2bee1 100644 --- a/CompElliptic/CurveCycle.lean +++ b/CompElliptic/CurveCycle.lean @@ -165,6 +165,11 @@ variable {F : Type*} [Field F] [Fintype F] noncomputable def frobCharPoly (E : SWCurve F) : ℤ[X] := X ^ 2 - C (trace E) * X + C (Fintype.card F : ℤ) +/-- Monic, hence `ℤ[X]/(frobCharPoly E)` is `ℤ`-free on the power basis `{1, π}` rather than an +arbitrary quotient: that is what makes `frobeniusOrder` an *order* (a rank-2 lattice) and not +merely a ring. Nothing below consumes it yet; it is the standing hypothesis of the Mathlib +`AdjoinRoot` lemmas any later structural work needs, starting with a basis and the discriminant +computation `disc ℤ[π] = t² - 4·#F`. -/ theorem frobCharPoly_monic (E : SWCurve F) : (frobCharPoly E).Monic := by unfold frobCharPoly monicity! @@ -187,6 +192,10 @@ abbrev frobeniusOrder (E : SWCurve F) : Type := AdjoinRoot (frobCharPoly E) /-- The formal Frobenius: the image of `X` in `ℤ[X]/(X² - t·X + #F)`. -/ noncomputable def frobeniusElt (E : SWCurve F) : frobeniusOrder E := AdjoinRoot.root _ +/-- The definitional unfolding, stated as an equation so `simp` can *fold* an `AdjoinRoot.root` +back into `frobeniusElt` with `← frobeniusElt_def`; `simp` cannot refold a definition by name. +Used in the round-trip proofs of `frobeniusOrderEquiv`, where the `ext` lemma leaves the goal in +terms of `root`. -/ theorem frobeniusElt_def (E : SWCurve F) : frobeniusElt E = AdjoinRoot.root (frobCharPoly E) := rfl @@ -278,6 +287,9 @@ noncomputable def frobeniusOrderHom (h : IsCycle₂ E₁ E₂) : (frobeniusElt E₂ + ((trace E₁ - 1 : ℤ) : frobeniusOrder E₂)) (aeval_frobCharPoly_shift h) +/-- What the comparison map does to the generator, which is the only fact about it any proof +here needs: `AdjoinRoot.algHom_ext` reduces every identity between maps out of `ℤ[π₁]` to their +value on `π₁`, so this is the simp lemma the round trip in `frobeniusOrderEquiv` runs on. -/ @[simp] theorem frobeniusOrderHom_frobeniusElt (h : IsCycle₂ E₁ E₂) : frobeniusOrderHom h (frobeniusElt E₁) From 6438050d479706b70a10da7c8d7e75c982e988de Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 19 Aug 2026 09:57:36 -0300 Subject: [PATCH 05/11] CurveCycle.lean: drop three declarations nothing consumes Goal-directed pruning: a lemma earns its place when a target needs it, not because an API ought to have it. - cm_invariant_eq was congrArg dressed as a theorem, and the case anyone actually wants is already hasCMDiscriminant_congr. - frobCharPoly_monic was justified only by pointing at work nobody has started. It comes back the day a power basis or the discriminant of the order is needed, which is one line. - frobDisc_eq_discrim pinned frobDisc against Mathlib's discrim, which is a reasonable drift guard but is consumed by nothing today; its import goes with it. What stays is the two layers that carry the result, the integer identity and the isomorphism of Frobenius orders, plus the statement in the form the literature uses (HasCMDiscriminant) and the Pasta instance. No census entry changes: none of the three was in TrustBoundary.lean. Co-Authored-By: Claude Opus 5 (1M context) --- CompElliptic/CurveCycle.lean | 26 +------------------------- 1 file changed, 1 insertion(+), 25 deletions(-) diff --git a/CompElliptic/CurveCycle.lean b/CompElliptic/CurveCycle.lean index ca2bee1..23e58e0 100644 --- a/CompElliptic/CurveCycle.lean +++ b/CompElliptic/CurveCycle.lean @@ -8,7 +8,6 @@ import CompElliptic.Curves.PastaOrder import Mathlib.Algebra.Squarefree.Basic import Mathlib.RingTheory.Int.Basic import Mathlib.RingTheory.AdjoinRoot -import Mathlib.Algebra.QuadraticDiscriminant /-! # A 2-cycle of curves shares its CM discriminant @@ -37,7 +36,7 @@ and let `frobDisc E = t(E)² - 4·#F`. If `E₁/F₁` and `E₂/F₂` form a 2-c which is `frobDisc_eq`: the two Frobenius discriminants are equal *as integers*, not merely up to squares. Every invariant read off that integer therefore agrees, in particular the CM field `ℚ(√(t² - 4·#F))`, its fundamental discriminant, and the conductor of the Frobenius order -(`cm_invariant_eq`, `hasCMDiscriminant_congr`). +(`hasCMDiscriminant_congr`). ## The order `ℤ[π]`, as a definition @@ -165,21 +164,6 @@ variable {F : Type*} [Field F] [Fintype F] noncomputable def frobCharPoly (E : SWCurve F) : ℤ[X] := X ^ 2 - C (trace E) * X + C (Fintype.card F : ℤ) -/-- Monic, hence `ℤ[X]/(frobCharPoly E)` is `ℤ`-free on the power basis `{1, π}` rather than an -arbitrary quotient: that is what makes `frobeniusOrder` an *order* (a rank-2 lattice) and not -merely a ring. Nothing below consumes it yet; it is the standing hypothesis of the Mathlib -`AdjoinRoot` lemmas any later structural work needs, starting with a basis and the discriminant -computation `disc ℤ[π] = t² - 4·#F`. -/ -theorem frobCharPoly_monic (E : SWCurve F) : (frobCharPoly E).Monic := by - unfold frobCharPoly - monicity! - -/-- `frobDisc` is the discriminant of that quadratic, in Mathlib's `discrim` sense. -/ -theorem frobDisc_eq_discrim (E : SWCurve F) : - frobDisc E = discrim 1 (-trace E) (Fintype.card F : ℤ) := by - simp only [frobDisc, discrim] - ring - /-- The **Frobenius order** `ℤ[π] = ℤ[X]/(X² - t·X + #F)` of `E`. This is the abstract form of the ring the comments above describe. The geometric `π` itself is @@ -319,14 +303,6 @@ noncomputable def frobeniusOrderEquiv (h : IsCycle₂ E₁ E₂) : push_cast linear_combination h2) -/-- Every invariant computed from the Frobenius discriminant agrees across a 2-cycle: the CM -field, the fundamental discriminant, the squarefree part, the conductor of `ℤ[π]`. The integers -themselves coincide (`frobDisc_eq`), so this is a congruence; it is recorded because the -literature states the shared quantity as one of these derived invariants. -/ -theorem cm_invariant_eq {α : Type*} (f : ℤ → α) (h : IsCycle₂ E₁ E₂) : - f (frobDisc E₁) = f (frobDisc E₂) := - congrArg f (frobDisc_eq h) - /-- **The CM discriminant is shared**: a squarefree `D` is a CM discriminant of one curve of a 2-cycle exactly when it is one of the other. No uniqueness of squarefree parts is needed, since the two discriminants are the same integer. -/ From c1e5ab6b8e5bde50f417e0588d4f79b06c3aa058 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 19 Aug 2026 10:22:23 -0300 Subject: [PATCH 06/11] CurveCycle.lean: keep the module doc to what the result needs Review feedback on two counts, both about the "what is and is not assumed" section. The ordinary/supersingular material was definitional elliptic-curve theory, not CM-discriminant material: it defined both notions, classified the endomorphism ring in each case, and described the quaternion order and the degenerate t = +-2p case, none of which any statement here uses. That belongs to a module encoding a theory of elliptic curves. What survives is the one sentence the reader needs, that ordinariness is a hypothesis nowhere below and governs only whether the shared integer may be CALLED a CM discriminant. The parenthetical claiming Mathlib lacks Hasse for WeierstrassCurve is dropped rather than corrected. It was loose (Mathlib has plenty of arithmetic geometry for these curves; what it lacks is Hasse and Weil bounds, and the function-field vocabulary of #30), and an accurate version would still be a claim about Mathlib's contents in a file that proves a counting identity. The section now says what this proof uses and stops there. Co-Authored-By: Claude Opus 5 (1M context) --- CompElliptic/CurveCycle.lean | 29 +++++++---------------------- 1 file changed, 7 insertions(+), 22 deletions(-) diff --git a/CompElliptic/CurveCycle.lean b/CompElliptic/CurveCycle.lean index 23e58e0..1feac88 100644 --- a/CompElliptic/CurveCycle.lean +++ b/CompElliptic/CurveCycle.lean @@ -50,28 +50,13 @@ and it is what "the same order" actually means. ## What is and is not assumed -No arithmetic geometry enters, and in particular neither Hasse's theorem (which Mathlib lacks -for `WeierstrassCurve`) nor any theorem about endomorphism rings. The identity is an integer -computation over the two point counts, so it holds for *any* pair of curves satisfying the -cycle equations, ordinary or not. - -What ordinariness buys is only the *reading* of the shared integer, never the identity. In all -cases `t² - 4·#F` is the discriminant of `ℤ[π]` (see `frobDisc`). A curve is **ordinary** when -the characteristic `p` does not divide `t` and **supersingular** when it does; over a prime -field with `p > 3` supersingular means exactly `t = 0`. Then: - -* ordinary: `End E` is an order in the imaginary quadratic field `ℚ(√(t² - 4·#F))`, so the - integer is a discriminant *in the right field*, but not necessarily `End E`'s own, because - `ℤ[π] ⊆ End E` can be strict. Pasta is such a case: `disc ℤ[π] = -3·V²` while - `End = ℤ[ζ₃]` has discriminant `-3`. -* supersingular: the geometric endomorphism ring is a maximal order in a quaternion algebra, - noncommutative and of rank `4`, so it has no quadratic discriminant to compare with. The - `F`-rational endomorphisms can still form a quadratic order (over `𝔽_p` an order in - `ℚ(√-p)`, by Waterhouse's classification), and over `𝔽_(p²)` with `t = ±2p` the integer - degenerates to `0` because `π = ±p` is already an integer. - -The statement proved here is deliberately the count-level one, which is the part the cycle -forces. +The proof is counting plus integer algebra: no theorem about endomorphism rings, and no +arithmetic geometry. It therefore holds for *any* pair of curves satisfying the cycle +equations. + +Ordinariness is a hypothesis nowhere below. It governs only whether the shared integer may be +*called* a CM discriminant, which needs `End E` to be a quadratic order; the statement proved +here is the count-level one, which is the part the cycle forces. ## Provenance From 743b0a9097476024b761326c4fd75f355c543d13 Mon Sep 17 00:00:00 2001 From: soc Date: Wed, 19 Aug 2026 10:48:13 -0300 Subject: [PATCH 07/11] CurveCycle.lean: drop the group-hash aside from the Pasta paragraph The paragraph explained that D = -3 is the j = 0 case, hence the curves have the form y^2 = x^3 + b, hence Simplified SWU needs a detour through an isogenous curve. That last step is group-hash material and has no bearing on the shared discriminant, which is what this module is for; the reader who wants it is already in Hashing/. What replaces it keeps only what the file's own statements need: the discriminant and the CM field, a pointer to frobDisc_pallas for the j = 0 nuance, and the provenance of the constant V, which is a search parameter of the CM norm equation rather than something derived here. Co-Authored-By: Claude Opus 5 (1M context) --- CompElliptic/CurveCycle.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/CompElliptic/CurveCycle.lean b/CompElliptic/CurveCycle.lean index 1feac88..f10164f 100644 --- a/CompElliptic/CurveCycle.lean +++ b/CompElliptic/CurveCycle.lean @@ -79,10 +79,10 @@ exhibits the shared discriminant explicitly: `t² - 4p = -3 · V²`, with `V = 0x93cd3a2c8198e2690c7c095a00000001`, -so the fundamental discriminant is `D = -3` and the CM field is `ℚ(√-3)`. That is exactly the -`j = 0` case, which is why both curves have the form `y² = x³ + b` and why Simplified SWU -(needing `a ≠ 0`) has to detour through an isogenous curve. Note also that `V ≡ 1 (mod 2³²)`, -the 2-adicity that the search was steering for. +so the fundamental discriminant is `D = -3` and the CM field is `ℚ(√-3)`; +`Pasta.frobDisc_pallas` records what that does and does not imply about `j`. The constant `V` +is a search parameter rather than a derived quantity: the Pasta primes were produced from the +CM norm equation `4p = t² + 3V²`, with `V ≡ 1 (mod 2³²)` chosen for 2-adicity. -/ namespace CompElliptic.CurveCycle From 171d43cd26f7f94bb663f84f48c69eb5b7f79ff3 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 19 Aug 2026 10:55:31 -0300 Subject: [PATCH 08/11] CurveCycle.lean: say what V is on the theorem that states it V appeared as a bare 128-bit constant in frobDisc_pallas, which invited the question of where it came from. It answers two questions at once, and both are about the discriminant, so the docstring of that theorem is where it belongs rather than the module header. Over K = Q(sqrt(-3)) with O_K the Eisenstein integers, Frobenius is an element of O_K of norm p, and (t, V) are its coordinates: pi = (t + V*sqrt(-3))/2 with N(pi) = (t^2 + 3V^2)/4 = p, so the theorem is N(pi) = p rewritten. Comparing disc Z[pi] = -3V^2 with disc O_K = -3 in disc = D*f^2 identifies V as the conductor [O_K : Z[pi]], i.e. how far Frobenius is from generating the whole ring. That is the same gap as the j = 0 caveat already in the docstring, now quantified: f = V > 1. It also explains the search. The units of O_K are mu_6, so the six unit multiples of pi are the six sextic twists with traces +-t and +-(t +- 3V)/2: six candidate orders per prime rather than one, which is what |D| = 3 buys, and for Pasta exactly one of the six is prime and equals q. The congruences t = V = 1 mod 2^32 then force 2^32 to divide both p - 1 and q - 1 = p - t, so one choice of (t, V) fixes the 2-adicity of both fields at once; searching over p directly gives no handle on q. Co-Authored-By: Claude Opus 5 (1M context) --- CompElliptic/CurveCycle.lean | 29 ++++++++++++++++++++++++----- 1 file changed, 24 insertions(+), 5 deletions(-) diff --git a/CompElliptic/CurveCycle.lean b/CompElliptic/CurveCycle.lean index f10164f..c1829fc 100644 --- a/CompElliptic/CurveCycle.lean +++ b/CompElliptic/CurveCycle.lean @@ -326,13 +326,32 @@ theorem trace_vesta : trace Vesta.curve = 86663725065984043395317761 := by decide /-- **The Pasta cycle's shared Frobenius discriminant is `-3 · V²`** with -`V = 0x93cd3a2c8198e2690c7c095a00000001`, so the CM field is `ℚ(√-3)`. Equivalently -`4p = t² + 3V²`, the CM norm equation at `|D| = 3` that the Pasta search solved. +`V = 0x93cd3a2c8198e2690c7c095a00000001`, so the CM field is `ℚ(√-3)`. + +`V` is not an arbitrary constant, and it is worth knowing what it is, because the same integer +answers two questions. Over `K = ℚ(√-3)` with `𝒪_K = ℤ[ζ₃]` the Eisenstein integers, Frobenius +is an element of `𝒪_K` of norm `p`, and `(t, V)` are its coordinates: + +`π = (t + V√-3)/2`, `N π = (t² + 3V²)/4 = p`, + +so the statement below is exactly `N π = p` rewritten, and it is the CM norm equation the Pasta +search solved. Second, comparing `disc ℤ[π] = -3V²` with `disc 𝒪_K = -3` in `disc = D·f²` makes + +`V = [𝒪_K : ℤ[π]]`, + +the conductor: `V` measures how far Frobenius is from generating the whole Eisenstein ring. + +That also explains the shape of the search. The units of `𝒪_K` are `μ₆`, so `u·π` for the six +units gives the six sextic twists, with traces `±t` and `±(t ± 3V)/2`: six candidate orders per +prime instead of one, which is what `|D| = 3` buys. For Pasta exactly one of the six is prime, +and it is `q`. The congruences `t ≡ V ≡ 1 (mod 2³²)` then force `2³² ∣ p - 1` and +`2³² ∣ p - t = q - 1` at once, which is how one choice of `(t, V)` fixes the 2-adicity of both +fields; searching over `p` directly would give no handle on `q`. Sharing the field is not by itself `j = 0`: an order of conductor `f > 1` in `ℚ(√-3)` has other -`j`-invariants. What a cycle forces is the field; what the search additionally fixed, by taking -`|D| = 3` and reading off the six twists per prime, is the *maximal* order `ℤ[ζ₃]`, whose extra -automorphisms are the `j = 0` ones. Pallas and Vesta are `y² = x³ + 5`, so they do realise it. -/ +`j`-invariants, and here `f = V > 1`. What a cycle forces is the field; what the search +additionally fixed is the *maximal* order `ℤ[ζ₃]` as `End`, whose extra automorphisms are the +`j = 0` ones. Pallas and Vesta are `y² = x³ + 5`, so they do realise it. -/ theorem frobDisc_pallas : frobDisc Pallas.curve = -3 * 196462116142286827589391630752301449217 ^ 2 := by simp only [frobDisc, trace_pallas, card_pallasBaseField] From 9920f533663198aafb8bc2d114c41070ff91beaf Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Wed, 19 Aug 2026 13:03:54 -0300 Subject: [PATCH 09/11] CurveCycle.lean: spell out the AdjoinRoot arguments instead of _ Review preference, and it costs three sites: frobeniusElt now names frobCharPoly E, frobeniusOrderHom names it too, and the proof of frobeniusOrderHom_frobeniusElt names all four arguments of AdjoinRoot.liftAlgHom_root rather than writing _ _ _ _. The gain is that a reader sees which polynomial's root is meant, and which instance of the general lemma is being used, without running the elaborator in their head; a mismatch is also reported at the argument rather than as a failure to infer. Co-Authored-By: Claude Opus 5 (1M context) --- CompElliptic/CurveCycle.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/CompElliptic/CurveCycle.lean b/CompElliptic/CurveCycle.lean index c1829fc..b6a1a8a 100644 --- a/CompElliptic/CurveCycle.lean +++ b/CompElliptic/CurveCycle.lean @@ -159,7 +159,8 @@ For an ordinary curve the ring below is genuinely `ℤ[π] ⊆ End E`, by the ch abbrev frobeniusOrder (E : SWCurve F) : Type := AdjoinRoot (frobCharPoly E) /-- The formal Frobenius: the image of `X` in `ℤ[X]/(X² - t·X + #F)`. -/ -noncomputable def frobeniusElt (E : SWCurve F) : frobeniusOrder E := AdjoinRoot.root _ +noncomputable def frobeniusElt (E : SWCurve F) : frobeniusOrder E := + AdjoinRoot.root (frobCharPoly E) /-- The definitional unfolding, stated as an equation so `simp` can *fold* an `AdjoinRoot.root` back into `frobeniusElt` with `← frobeniusElt_def`; `simp` cannot refold a definition by name. @@ -252,7 +253,7 @@ theorem aeval_frobCharPoly_shift (h : IsCycle₂ E₁ E₂) : /-- **`π₁ ↦ π₂ + (t₁ - 1)`**, the comparison map between the two Frobenius orders of a 2-cycle. -/ noncomputable def frobeniusOrderHom (h : IsCycle₂ E₁ E₂) : frobeniusOrder E₁ →ₐ[ℤ] frobeniusOrder E₂ := - AdjoinRoot.liftAlgHom _ (Algebra.ofId ℤ (frobeniusOrder E₂)) + AdjoinRoot.liftAlgHom (frobCharPoly E₁) (Algebra.ofId ℤ (frobeniusOrder E₂)) (frobeniusElt E₂ + ((trace E₁ - 1 : ℤ) : frobeniusOrder E₂)) (aeval_frobCharPoly_shift h) @@ -263,7 +264,8 @@ value on `π₁`, so this is the simp lemma the round trip in `frobeniusOrderEqu theorem frobeniusOrderHom_frobeniusElt (h : IsCycle₂ E₁ E₂) : frobeniusOrderHom h (frobeniusElt E₁) = frobeniusElt E₂ + ((trace E₁ - 1 : ℤ) : frobeniusOrder E₂) := - AdjoinRoot.liftAlgHom_root _ _ _ _ + AdjoinRoot.liftAlgHom_root (frobCharPoly E₁) (Algebra.ofId ℤ (frobeniusOrder E₂)) + (frobeniusElt E₂ + ((trace E₁ - 1 : ℤ) : frobeniusOrder E₂)) (aeval_frobCharPoly_shift h) /-- **The two curves of a 2-cycle have isomorphic Frobenius orders**, `ℤ[π₁] ≃ ℤ[π₂]`, by the generator shift above in both directions: the round trip moves the generator by From 4140e072780d0eec767ab55ee9aa4e67e7d4723f Mon Sep 17 00:00:00 2001 From: soc Date: Wed, 19 Aug 2026 13:06:41 -0300 Subject: [PATCH 10/11] CurveCycle.lean: drop frobeniusElt_def for Lean's generated eq_def Review is right that the lemma was redundant, though not because it was obvious: obviousness does not disqualify an equation lemma, since simp and rw work syntactically and cannot fold a definition by name (simp [<- frobeniusElt] is rejected outright, with the compiler pointing at exactly this kind of lemma). What disqualifies it is that Lean already generates the equation as frobeniusElt.eq_def, so writing it by hand duplicated the elaborator. The two round-trip proofs in frobeniusOrderEquiv now fold with <- frobeniusElt.eq_def, which is the idiomatic spelling and appears in Mathlib. Co-Authored-By: Claude Opus 5 (1M context) --- CompElliptic/CurveCycle.lean | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) diff --git a/CompElliptic/CurveCycle.lean b/CompElliptic/CurveCycle.lean index b6a1a8a..4a024f4 100644 --- a/CompElliptic/CurveCycle.lean +++ b/CompElliptic/CurveCycle.lean @@ -162,13 +162,6 @@ abbrev frobeniusOrder (E : SWCurve F) : Type := AdjoinRoot (frobCharPoly E) noncomputable def frobeniusElt (E : SWCurve F) : frobeniusOrder E := AdjoinRoot.root (frobCharPoly E) -/-- The definitional unfolding, stated as an equation so `simp` can *fold* an `AdjoinRoot.root` -back into `frobeniusElt` with `← frobeniusElt_def`; `simp` cannot refold a definition by name. -Used in the round-trip proofs of `frobeniusOrderEquiv`, where the `ext` lemma leaves the goal in -terms of `root`. -/ -theorem frobeniusElt_def (E : SWCurve F) : - frobeniusElt E = AdjoinRoot.root (frobCharPoly E) := rfl - /-- **The characteristic equation**, `π² - t·π + #F = 0`, holding in `ℤ[π]` by construction. -/ theorem frobeniusElt_charEq (E : SWCurve F) : frobeniusElt E ^ 2 - (trace E : frobeniusOrder E) * frobeniusElt E @@ -277,7 +270,7 @@ noncomputable def frobeniusOrderEquiv (h : IsCycle₂ E₁ E₂) : have h2 : ((trace E₁ : frobeniusOrder E₂)) + (trace E₂ : frobeniusOrder E₂) = 2 := by exact_mod_cast congrArg (fun n : ℤ => (n : frobeniusOrder E₂)) (trace_add_trace h) ext - simp only [AlgHom.comp_apply, AlgHom.coe_id, id_eq, ← frobeniusElt_def, + simp only [AlgHom.comp_apply, AlgHom.coe_id, id_eq, ← frobeniusElt.eq_def, frobeniusOrderHom_frobeniusElt, map_add, map_intCast] push_cast linear_combination h2) @@ -285,7 +278,7 @@ noncomputable def frobeniusOrderEquiv (h : IsCycle₂ E₁ E₂) : have h2 : ((trace E₁ : frobeniusOrder E₁)) + (trace E₂ : frobeniusOrder E₁) = 2 := by exact_mod_cast congrArg (fun n : ℤ => (n : frobeniusOrder E₁)) (trace_add_trace h) ext - simp only [AlgHom.comp_apply, AlgHom.coe_id, id_eq, ← frobeniusElt_def, + simp only [AlgHom.comp_apply, AlgHom.coe_id, id_eq, ← frobeniusElt.eq_def, frobeniusOrderHom_frobeniusElt, map_add, map_intCast] push_cast linear_combination h2) From f9e3f1ee8c852731bb2ed0909cd7b682bec5abf1 Mon Sep 17 00:00:00 2001 From: soc Date: Wed, 19 Aug 2026 13:18:37 -0300 Subject: [PATCH 11/11] CurveCycle.lean: say why being a root is the well-definedness condition aeval_frobCharPoly_shift asserted that the root property is what makes frobeniusOrderHom well defined without saying why. Four lines of context: a map out of Z[X]/(f) is a map out of Z[X] that kills the ideal, the ideal is principal, so killing the generator is the entire obligation; aeval is the map out of the free algebra with X mapsto x, and is eval2 at the canonical algebraMap, which is the shape liftAlgHom asks for. Notes too that the shift is an integer only because the traces sum to 2, which is the sole use of the cycle hypothesis in this construction. Co-Authored-By: Claude Opus 5 (1M context) --- CompElliptic/CurveCycle.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/CompElliptic/CurveCycle.lean b/CompElliptic/CurveCycle.lean index 4a024f4..1d67013 100644 --- a/CompElliptic/CurveCycle.lean +++ b/CompElliptic/CurveCycle.lean @@ -227,7 +227,11 @@ its mirror image is its inverse. This is the statement to reuse: it is strictly equality of discriminants, and it needs no square roots to state. -/ /-- `π₂ + (t₁ - 1)` is a root of `E₁`'s characteristic polynomial, which is what makes -`frobeniusOrderHom` well defined. -/ +`frobeniusOrderHom` well defined: a map out of `ℤ[π₁] = ℤ[X]/(frobCharPoly E₁)` is a map out of +`ℤ[X]` that kills the ideal, and that ideal is principal, so killing its generator is the whole +obligation. (`aeval x` is the map out of the free algebra with `X ↦ x`; it is `eval₂` at the +canonical `algebraMap`, which is the shape `AdjoinRoot.liftAlgHom` asks for.) The shift is an +integer at all only because `t₁ + t₂ = 2`, which is the sole use of the cycle here. -/ theorem aeval_frobCharPoly_shift (h : IsCycle₂ E₁ E₂) : aeval (frobeniusElt E₂ + ((trace E₁ - 1 : ℤ) : frobeniusOrder E₂)) (frobCharPoly E₁) = 0 := by have ht₁ : trace E₁ = (Fintype.card F₁ : ℤ) + 1 - (Fintype.card F₂ : ℤ) := by