CurveCycle.lean: a 2-cycle of curves shares its CM discriminant by dannywillems · Pull Request #31 · daira/CompElliptic

dannywillems · 2026-08-18T18:54:36Z

Stacks on #27 (indiff-counting), so the diff to read is the single commit CurveCycle.lean: a 2-cycle of curves shares its CM discriminant.

The zcash/ironwood group-hash page explains the j = 0 shape of the Pasta curves with two claims glued together: that the two curves of a 2-cycle necessarily share their CM discriminant, and that with known methods a cycle is only findable when that discriminant is tiny. Only the first is a theorem. This PR adds it as one, and instantiates it at Pasta.

What is proved

CompElliptic/CurveCycle.lean:

trace and frobDisc, defined by counting (#F + 1 - #E(F) and t^2 - 4*#F) rather than as eigenvalue data, which keeps the module free of arithmetic geometry.
trace_add_trace: the two counting equations of a 2-cycle add to t1 + t2 = 2.
frobDisc_eq: substituting t2 = 2 - t1 gives t2^2 - 4*#F2 = t1^2 - 4*#F1. The two Frobenius discriminants are equal as integers, which is stronger than the usual "same CM discriminant" phrasing (that compares only squarefree parts), so both curves have CM by an order in the same imaginary quadratic field.
hasCMDiscriminant_congr: a squarefree D is a CM discriminant of one curve exactly when it is one of the other. No uniqueness-of-squarefree-part lemma is needed, precisely because the integers coincide.

`Z[pi]` as a definition, not a comment

A discriminant is a shadow of the ring it comes from, so that ring is defined and the conclusion is also stated there:

frobCharPoly E = X^2 - t*X + #F, with frobDisc_eq_discrim tying it back to Mathlib's discrim.
frobeniusOrder E = AdjoinRoot (frobCharPoly E), which is Z[pi] = Z[X]/(X^2 - tX + #F); frobeniusElt E is the class of X, which is pi; and frobeniusElt_charEq is the characteristic equation pi^2 - t*pi + #F = 0.
frobeniusOrderEquiv : Z[pi_1] ~=a[Z] Z[pi_2] for a 2-cycle, given explicitly by pi_1 |-> pi_2 + (t_1 - 1). Inside K the two generators are (t_i + sqrt D)/2, so they differ by the integer (t_1 - t_2)/2 = t_1 - 1, which is an integer exactly because the traces sum to 2; the mirror map inverts it. This is the reusable form: strictly stronger than equality of discriminants, and it needs no square roots to state.

The geometric pi is deliberately not defined: as an endomorphism it acts on points over extensions of the base field, and on E(F) alone it is the identity, so there is nothing to gain from putting it on SWPoint.

The Pasta instance

Off the orders already pinned in Curves/PastaOrder.lean: t = -86663725065984043395317759 and

t^2 - 4p = -3 * V^2, V = 0x93cd3a2c8198e2690c7c095a00000001

so the CM field is Q(sqrt(-3)), and 4p = t^2 + 3V^2 is the CM norm equation at |D| = 3 that the Pasta search solved. (V = 1 mod 2^32, the 2-adicity the search was steering for.) Pasta.frobeniusOrderEquiv is the corresponding identification of Z[pi_Pallas] with Z[pi_Vesta].

Nothing about endomorphism rings is assumed, so neither Hasse (which Mathlib lacks for WeierstrassCurve) nor any arithmetic geometry is needed; the identity holds for any pair of curves satisfying the cycle equations, ordinary or not. Ordinariness is what makes the shared integer mean a CM discriminant, and the module says so.

Provenance

Proposition 6.1 of Chiesa, Chua and 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 Belles-Munoz, Jimenez Urroz and Silva, Revisiting cycles of pairing-friendly elliptic curves, CRYPTO 2023 (ia.cr/2022/1662). Both state the discriminant with the opposite sign (squarefree part of 4q - t^2), so their D = 3 is the D = -3 here; the module notes the convention. I could not find an existing mechanisation.

Trust boundary

lake build --wfail is green and there is no sorry. The general results (trace_add_trace, frobDisc_eq, hasCMDiscriminant_congr, frobeniusElt_charEq, frobeniusOrderEquiv) depend on [propext, Classical.choice, Quot.sound] only; the Pasta corollaries inherit exactly the two prime-order native_decide witnesses (Pallas.q_nsmul_Gpt, Vesta.p_nsmul_Gpt) and nothing else. Both tiers are registered in TrustBoundary.lean, so the census enforces them.

Deliberately not in this PR

The ironwood wording. For the record, the second half of that sentence is not a theorem: nothing known rules out a 2-cycle with a large discriminant, and the CM method is generally reckoned feasible up to |D| ~ 10^16 (ia.cr/2022/1662, section 2.1). What |D| = 3 buys is a cheap search: h(-3) = 1 means the curve is written down directly, and the six sextic twists give six candidate orders per prime. Also worth separating: a cycle forces the CM field, while j = 0 needs the maximal order, since an order of conductor f > 1 in Q(sqrt(-3)) has other j-invariants.

🤖 Claude Opus 5 (1M context)

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 <daira@jacaranda.org>

dannywillems · 2026-08-18T19:00:34Z

This aims to complement a statement made in the patch ironwood/199:

Daira-Emma Hopwood's ZK Study Club talk "Optimizing Halo and Constructing Graphs of Elliptic Curves" (part 1, bonus session, slides) explains why the Pasta curves have this form: the two curves of a 2-cycle necessarily share their CM discriminant, and with known methods a cycle can only feasibly be found when that discriminant is tiny (the Pasta search fixed the smallest, D=−3, which is exactly the case j=0).

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) <noreply@anthropic.com>

dannywillems · 2026-08-18T19:53:28Z

+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


This is a correct reference at the time of writing.

Source: https://eprint.iacr.org/2022/1662.pdf

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) <noreply@anthropic.com>

dannywillems · 2026-08-19T12:46:25Z

+/-- 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) : ℤ)


Review comment: noncomputable because it depends on Nat.card.

Reviewer note: noncomputable means that the compiler won't emit executable code for this symbol.
Note: https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Computation/

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) <noreply@anthropic.com>

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) <noreply@anthropic.com>

dannywillems · 2026-08-19T13:00:42Z

@@ -0,0 +1,381 @@
+/-


Reviewer note: I'm checking the file to ensure that we do not encode too much here, and stay factual only about the Pasta curves (or a slightly more general, e.g. "curve cycles" with the properties the Zcash protocols and primitives require).

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 daira#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) <noreply@anthropic.com>

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) <noreply@anthropic.com>

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) <noreply@anthropic.com>

dannywillems · 2026-08-19T15:54:30Z

+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)


Reviewer note: AdjoinRoot creates the quotient by the polynomial.

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) <noreply@anthropic.com>

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) <noreply@anthropic.com>

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) <noreply@anthropic.com>

dannywillems · 2026-08-19T16:20:12Z

+  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


dannywillems · 2026-08-19T16:21:20Z

+`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


[...] Eisentein integers [...]

https://en.wikipedia.org/wiki/Eisenstein_integer

dannywillems · 2026-08-19T16:24:54Z

+`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 :


dannywillems

self ACK f9e3f1e

dannywillems force-pushed the curve-cycle-discriminant branch from b20fc68 to 6e187a2 Compare August 18, 2026 18:59

dannywillems force-pushed the curve-cycle-discriminant branch from 6e187a2 to 582272b Compare August 18, 2026 19:06

dannywillems force-pushed the curve-cycle-discriminant branch from 582272b to 62d6ece Compare August 18, 2026 19:16

dannywillems marked this pull request as draft August 18, 2026 19:47

dannywillems commented Aug 18, 2026

View reviewed changes

Comment thread CompElliptic/CurveCycle.lean Outdated

dannywillems commented Aug 18, 2026

View reviewed changes

Comment thread CompElliptic/CurveCycle.lean Outdated

dannywillems force-pushed the curve-cycle-discriminant branch from aac52be to d0dca00 Compare August 18, 2026 20:07

dannywillems mentioned this pull request Aug 18, 2026

Group-hash indifferentiability: security games, rejection-sampling simulator, and concrete endpoints zcash/ironwood#199

Merged