feat: the GLV endomorphism, and φ = [λ] on Pallas and Vesta#5
Draft
dannywillems wants to merge 6 commits into
Draft
feat: the GLV endomorphism, and φ = [λ] on Pallas and Vesta#5dannywillems wants to merge 6 commits into
φ = [λ] on Pallas and Vesta#5dannywillems wants to merge 6 commits into
Conversation
For `y² = x³ + B` over a field with a primitive cube root of unity `ζ`, the map `φ (x, y) = (ζ x, y)` is a group endomorphism, and on a prime-order group it must act as multiplication by some scalar. This is the basis of the GLV scalar decomposition; the concrete Pasta constants follow separately. Three layers, mirroring `CurveOrder.lean`: * Pure finite-group theory (`endo_eq_nsmul_of_prime_card`): no elliptic curves at all. An endomorphism of a group of prime order `r` that sends one non-identity `g` to `[lam] g` is `[lam]` everywhere, via Mathlib's `mem_multiples_of_prime_card` (which derives `Finite` internally from `Nat.card G = r` and primality, so no `IsCyclic` / `zpowers` machinery is needed). This is what reduces `φ = [λ]` on the whole group to a single closed, spot-checkable fact about one point. * Raw computable kernel: `phi` on `F × F`, with `phi_add` proving it commutes with the raw `add`. This needs *no* hypotheses beyond `ζ³ = 1`: not `Valid`, not `IsElliptic`, not `B ≠ 0`. The slope scales by `ζ²` in *both* branches (`3(ζx)²/(2y) = ζ²·s` doubling, `(y₂-y₁)/(ζx₂-ζx₁) = ζ⁻¹·s = ζ²·s` for distinct `x`), the branch guards are preserved exactly (`ζ ≠ 0`), and the degenerate divisions agree because both sides produce `0/0 = 0`. The branch walk is explicit, not `split_ifs <;> simp_all`, which blows the recursion limit on the nested `ite`s (cf. `add_neg`). * Rich bundled types: `SWPoint.phiPt` / `SWPoint.phiHom` (`φ` as an `AddMonoidHom`), and the capstone `SWPoint.phiPt_eq_nsmul` combining the two layers above. `A = 0` is essential (for `A ≠ 0`, `y² = (ζx)³ + A(ζx) + B` fails), which covers the Pasta curves and every curve GLV is used on in practice. No `sorry`; every declaration depends only on `propext` / `Classical.choice` / `Quot.sound`. No `decide` or `native_decide` here: the numeric facts (`ζ³ = 1` and the spot-check) are per-curve closed facts, and land with the curves.
Records the design for GLV on the Pasta curves: the endomorphism itself (this PR), the concrete Pallas / Vesta constants and the `φ = [λ]` spot-check, the Plausible property-test harness, and the scalar decomposition that follows. Includes the findings that shaped it: the slope scales by `ζ²` in both branches of `add` (so `phi_add` needs no side conditions); `mem_multiples_of_prime_card` removes the need for any cyclic-group machinery; the `ζ` / `λ` numeric facts are kernel-`decide`-able, so only the point spot-check needs `native_decide` (`binNsmul` is well-founded recursion, so kernel `decide` gets stuck, not merely slow); and Plausible's stock generators cap at 100, so a crypto-size field needs a uniform `Arbitrary (ZMod n)` built on `Gen.choose`. Also notes that the `plausible` *tactic* closes goals with `sorry` when it finds no counterexample, so only `#test` / `#eval Testable.check` are usable here.
Instantiates `CurveForms/Endomorphism.lean` at the two Pasta curves. Both are `y² = x³ + 5`, so `A = 0` and the endomorphism applies, and `p ≡ q ≡ 1 mod 3`, so both fields have primitive cube roots of unity. The payoff is `phi_eq_lambda_nsmul`: `φ = [λ]` on the whole group, assuming Hasse's bound (via `card_eq`). Everything general was proved outright in `Endomorphism.lean`; only closed numeric facts remain here: * the field-level facts (`ζ³ = 1`, `ζ ≠ 1`, `ζ² + ζ + 1 = 0`, and the `λ` analogues) are kernel-`decide`d, so the *definition* of `φ` carries no `native_decide`; * the single point fact `φ G = [λ] G` (`phi_Gpt`) is `native_decide`d. Kernel `decide` cannot do it — not merely slowly, but at all: `binNsmul` is defined by well-founded recursion, so its equations do not reduce definitionally and `decide` gets stuck at `instDecidableEqSWPoint`. This is the same reason `PastaOrder.lean`'s `[order] G = 𝒪` witness is `native_decide`. `λ` is a `ℕ` (not a scalar-field element) so that `LAMBDA • _` is the fast `binNsmul` action, which is what makes the spot-check `native_decide`-able. The `(ζ, λ) `pairing is not free: each field has *two* primitive cube roots of unity, and a given `ζ` acts as `[λ]` for exactly one of the two candidates. The wrong pairing still yields a perfectly good endomorphism, just `[λ²]` rather than `[λ]` — a silent, wrong-by-a-cube-root bug. `phi_Gpt` is precisely the check that rules this out, which is why it is machine-checked rather than a comment; the other cube root was confirmed to fail it, so the check has teeth. The Pasta cycle crosses the two curves' constants (Pallas's `ζ` lives in `𝔽ₚ` and its `λ` in `𝔽_q`; Vesta's the other way round). Also adds `phi_phi_phi` / `SWPoint.phiPt_phiPt_phiPt` (`φ³ = id`) to `Endomorphism.lean`: purely computational from `ζ³ = 1`, so it needs neither the group order nor the `φ = [λ]` identification. Axiom footprint of `phi_eq_lambda_nsmul`: the standard three, the pre-existing `PastaOrder` `native_decide` axioms, and exactly one new one (`phi_Gpt`). No new *kind* of trust.
The form-level endomorphism and the Pallas/Vesta instantiation are done; the Plausible property-test harness and the GLV scalar decomposition are not. Notes the constraints found along the way (`A = 0` is essential; the `(ζ, λ)` pairing must be checked, not assumed; Plausible's stock generators are useless at 254 bits and its tactic form emits `sorry`).
dannywillems
changed the title
φ = [λ] on Pallas and Vesta
…k conventions Review pass against the conventions actually used on main. Move `CurveForms/Endomorphism.lean` to `Endomorphism.lean`, namespace `CompElliptic.Endomorphism`. TODO.md states that `CurveForms/` holds one module per curve *form*, and that namespaces mirror the directory path throughout; the endomorphism is neither a curve form nor was its namespace (`CompElliptic.CurveForms.ShortWeierstrass`) mirroring its path. `CurveOrder.lean` is the precedent for exactly this shape of module — a cross-cutting layer over the short-Weierstrass form, at top level, with its own namespace, opening `ShortWeierstrass`, split into "pure group theory" and "curve" layers, and instantiated by a `Curves/Pasta*.lean` — so follow it. The layer-3 declarations lose their `SWPoint.` prefix accordingly (it would have created a bogus `CompElliptic.Endomorphism.SWPoint` namespace). Drop `set_option maxRecDepth 10000` from `PastaEndo.lean`: it is not needed (every `decide` there compiles without it), and main uses no `set_option` anywhere. Add the `native_decide` sanity checks the concrete-curve modules all carry (`Curves/Pasta.lean` has 14, `Fields/Pasta.lean` 6; `PastaEndo.lean` had none): `φ` fixes `𝒪`, moves `G`, cubes to the identity, is additive on a concrete pair, and — the one that matters — is *not* `[λ²]`. That last check is what gives `phi_Gpt` its teeth: `λ²` is the other primitive cube root of unity in the scalar field, and pairing `ζ` with it would yield a well-typed, perfectly valid endomorphism that is simply the wrong one. It is now machine-checked, not merely asserted. Add the missing docstrings (`ZETA_cube`, `LAMBDA_cube` on both curves, `phiPt_coords`).
dannywillems
force-pushed
the
glv-endomorphism
branch
from
23db4de to
eb10b34
Compare
…amespaces Every name borrowed from another module now carries its source namespace at the use site, so where each definition comes from is readable without chasing imports: `ShortWeierstrass.add`, `ShortWeierstrass.SWPoint`, `CurveOrder.HasseBound`, `Endomorphism.phiPt`, `Fields.Pasta.PallasBaseField`. Only `CompElliptic.CurveForms` is opened, never the `ShortWeierstrass` leaf. That keeps the provenance visible while stopping the short-Weierstrass names from expanding to a full `CurveForms.ShortWeierstrass.…` path on every line (which pushed `phiHom`'s signature past 170 characters). `Curves/Pasta.lean` and `Curves/PastaOrder.lean` still open the leaf namespace; they are left alone here to keep this PR to the GLV work. No change to what is proved: `lake build` is green and the axiom footprints are unchanged (`phi_add` on the standard three; `phi_eq_lambda_nsmul` on those plus the pre-existing `PastaOrder` `native_decide` axioms plus `phi_Gpt`).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
GLV on the Pasta curves. For
y² = x³ + Bover a field with a primitive cuberoot of unity
ζ, the mapφ (x, y) = (ζ x, y)is a group endomorphism, and ona prime-order group it must act as multiplication by some scalar
λ. This PRbuilds that machinery and pins
λfor Pallas and Vesta. Scalar decompositionfollows separately.
Design notes:
design/glv-endomorphism-plan.md.CurveForms/Endomorphism.lean— the form-level endomorphismThree layers, mirroring
CurveOrder.lean:Pure finite-group theory (
endo_eq_nsmul_of_prime_card), no ellipticcurves at all: an endomorphism of a group of prime order
rthat sends onenon-identity
gto[lam] gis[lam]everywhere. Mathlib'smem_multiples_of_prime_cardderivesFiniteinternally fromNat.card G = rplus primality, so noIsCyclic/zpowersmachinery isneeded and the proof is five lines. This is what reduces
φ = [λ]on thewhole group to one closed, spot-checkable fact about a single point, in the
Independently re-checkable trust style.
Raw computable kernel:
phionF × F, withphi_add(commutes with theraw
add),onCurve_phi,valid_phi, andphi_phi_phi(φ³ = id).phi_addneeds no hypotheses beyondζ³ = 1: notValid, notIsElliptic, notB ≠ 0. The slope scales byζ²in both branches(
3(ζx)²/(2y) = ζ²·sfor doubling,(y₂-y₁)/(ζx₂-ζx₁) = ζ⁻¹·s = ζ²·sfordistinct
x), the branch guards are preserved exactly (ζ ≠ 0), and thedegenerate divisions agree because both sides produce
0/0 = 0.Rich bundled types:
SWPoint.phiPt/SWPoint.phiHom(φas anAddMonoidHom), and the capstoneSWPoint.phiPt_eq_nsmul.A = 0is essential: forA ≠ 0,y² = (ζx)³ + A(ζx) + Bfails. That coversthe Pasta curves and every curve GLV is used on in practice.
Curves/PastaEndo.lean— Pallas and Vestaphi_eq_lambda_nsmul:φ = [λ]on the whole group, assumingHasseBound(via the existing
card_eq). Only closed numeric facts live here:ζ³ = 1,ζ ≠ 1,ζ² + ζ + 1 = 0, and theλanalogues) are kernel-
decided, so the definition ofφcarries nonative_decide;φ G = [λ] G(phi_Gpt) isnative_decided. Kerneldecidecannot do it — not merely slowly, but at all:binNsmuliswell-founded recursion, so its equations do not reduce definitionally and
decidegets stuck atinstDecidableEqSWPoint. Same reasonPastaOrder's[order] G = 𝒪witness isnative_decide.λis kept as aℕ(not a scalar-field element) soLAMBDA • _is the fastbinNsmulaction, which is what makes the spot-checknative_decide-able.Why
phi_GptexistsThe
(ζ, λ)pairing is not free. Each field has two primitive cube rootsof unity, and a given
ζacts as[λ]for exactly one of the two candidates.Pairing them wrongly still gives a perfectly good endomorphism, just equal to
[λ²]rather than[λ]— a silent, wrong-by-a-cube-root bug that no type wouldcatch.
phi_Gptis precisely the check that rules it out, so it ismachine-checked rather than asserted in a comment. I confirmed it has teeth: the
other cube root of unity provably fails it.
The Pasta cycle crosses the two curves' constants (Pallas's
ζis in𝔽ₚandits
λin𝔽_q; Vesta's the other way round).Trust
No
sorry.Endomorphism.leanuses nodecide/native_decideat all anddepends only on
propext/Classical.choice/Quot.sound. The axiomfootprint of
phi_eq_lambda_nsmulis those three, plus the pre-existingPastaOrdernative_decideaxioms, plus exactly one new one (phi_Gpt). No newkind of trust.
Notes for review
phi_addbranch walk is explicit (by_cases+rw [if_pos/if_neg])rather than
split_ifs <;> simp_all, which blows the recursion limit on thenested
ites, as theadd_negdocstring already warns.[DecidableEq F]is deliberately not in scope untilphi_add: everythingbefore it needs only
[Field F].design/glv-endomorphism-plan.mdalso records what is not here — thePlausible property-test harness and the scalar decomposition. Drop that commit
if you would rather the plan not live in the repo.