Pin the Pasta group orders without assuming Hasse - #6
Merged
Conversation
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>
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>
daira
force-pushed
the
unconditional-pasta-order
branch
from
July 16, 2026 01:26
51083b5 to
082b57a
Compare
daira
marked this pull request as ready for review
July 16, 2026 02:25
martyall
added a commit
to l-adic/snarky
that referenced
this pull request
Jul 16, 2026
…ve axioms CompElliptic upstream (daira/CompElliptic#6, synced into the fork as l-adic/CompElliptic#2, submodule bumped) pins both Pasta group orders UNCONDITIONALLY: the elementary fibre bound #E <= 2#F + 1 plus the native_decide prime-order witness replace Hasse's theorem, with Vesta's leftover #E = 2p case excluded because -5 is not a cube in its base field. Gpt and Gpt_ne_zero now discharge by kernel decide. So Pasta.{pallas,vesta}_hasse are deleted (HasseBound no longer even exists to state them), and every hypothesis they fed evaporates: pallas/vesta_card read the unconditional card_eq through the SWPoint bridge, the Module instances lose their axiom transit, and Endo.lean's Hasse-parametrized eigen_of_hasse layer collapses into the pallas/vesta_eigen theorems themselves. Trust accounting after this commit: - pasta declares NO axioms; its gate allows standard logic + ofReduceBool only, everything else is a named native_decide certificate. - kimchi's gate drops both hasse allowlist entries; all 91 roots reduce to standard axioms + certificates. - the terminal theorem kimchiVesta_run_sound_algebraic_ft's full closure is propext/Classical.choice/Quot.sound + kimchi_fiat_shamir_vesta + native_decide certificates (p_nsmul_Gpt, the field primality witnesses) — no curve axioms of any kind. - EndoMul faithfulness closes on exactly two certificates: the prime-order witness and the eigenvalue anchor. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD
martyall
added a commit
to l-adic/CompElliptic
that referenced
this pull request
Jul 16, 2026
Sync with upstream: unconditional Pasta group orders (daira#6)
martyall
added a commit
to l-adic/snarky
that referenced
this pull request
Jul 17, 2026
…the Hasse axioms (#247) * formal/pasta: prove the GLV eigenvalue relations, delete the eigen axioms The CM eigenvalue relations Pasta.{pallas,vesta}_eigen were axioms; they are now theorems with byte-identical statements, so the pasta trust surface shrinks to the two Hasse bounds plus the native_decide certificates. Proof (new Pasta/Endo.lean): the coordinate map (x,y) ↦ (βx,y) with β³ = 1 commutes with the short-Weierstrass a=0 addition formulas over any field — pure field algebra, no on-curve or characteristic hypotheses (division junk cases degrade consistently since λ' = β²λ). Lifting to SWPoint gives an additive endomorphism; under the Hasse bound the point group has prime order, so it is cyclic on the fixed generator, and the anchor certificate {pallas,vesta}_lam_nsmul_Gpt (λ • G = φ(G), native_decide at the standard generator, in the style of CompElliptic's point counts) pins the eigenvalue there; the homomorphism extends it to every point. Transport through toPt lands the Mathlib Affine.Point statements. The anchors are the only native_decides in the workspace packages; the pasta and kimchi axiom gates permit exactly those two declarations by name. The CompElliptic submodule is untouched. Endo.lean is public/private split: public = {pallas,vesta}_eigen_of_hasse (what Basic.lean consumes) + the anchors with their statement components; every intermediate (endoPair, endoPair_add, endoPt, endoHom, toPtHom, the SWPoint-level relations) is private. deadcode.lean now demangles private names in isOurs — without that the walk refuses to enter private helpers and everything referenced only through them reports dead (it also silently hid two genuinely dead private kimchi helpers, now visible in the report). Housekeeping in the same pass (privatization pilot): delete the unreferenced zsmul_mod, SWCurve.Pt, and {pallas,vesta}_endo_ne_one; mark glv_no_short_of_cert private; manifest gains SWCurve.toAffine and moves eigen to the derived section. Kimchi's axiom gate drops the eigen allowlist entries — its 91 roots now reduce to standard axioms + Hasse + the trusted native_decide certificates only. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD * formal/pasta: consolidate the GLV story into Endo.lean The endomorphism material was spread over three modules: the concrete constants (Constants.lean), the eigenvalue machinery (Endo.lean), and the consumer-facing facts — the closed eigen theorems and the lattice short-basis bounds (Basic.lean). It is one story — this endomorphism exists, is additive, and acts as [λ] — so it is now one module. Endo.lean reads top to bottom: constants (β, λ, the cube-root proofs) → additivity → the SWPoint hom → the native_decide anchors → the transport to Mathlib points → the consumer theorems {pallas,vesta}_eigen (closed with the Hasse axioms) and {pallas,vesta}_glv_no_short_relation. With everything in one file, the eigen_of_hasse pair loses its only cross-file consumer and becomes private; the public surface is the constants, the two anchors with their statement components, and the four consumer theorems. Basic.lean is now purely the trust base and group orders: the Hasse axioms, the point counts, primality, and the Fact instances. Endo imports Basic (for the axioms); Basic no longer imports Endo. Constants.lean is deleted; its two external consumers re-point to Pasta.Endo (poseidon's FqSponge and kimchi's Fixture/PS). This gives up the fast-lane leaf import — the poseidon FS layer now pays the full-Mathlib import cone. No declaration names change; roots.txt and the gates are untouched. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD * formal: delete the Hasse axioms — the workspace has zero declared curve axioms CompElliptic upstream (daira/CompElliptic#6, synced into the fork as l-adic/CompElliptic#2, submodule bumped) pins both Pasta group orders UNCONDITIONALLY: the elementary fibre bound #E <= 2#F + 1 plus the native_decide prime-order witness replace Hasse's theorem, with Vesta's leftover #E = 2p case excluded because -5 is not a cube in its base field. Gpt and Gpt_ne_zero now discharge by kernel decide. So Pasta.{pallas,vesta}_hasse are deleted (HasseBound no longer even exists to state them), and every hypothesis they fed evaporates: pallas/vesta_card read the unconditional card_eq through the SWPoint bridge, the Module instances lose their axiom transit, and Endo.lean's Hasse-parametrized eigen_of_hasse layer collapses into the pallas/vesta_eigen theorems themselves. Trust accounting after this commit: - pasta declares NO axioms; its gate allows standard logic + ofReduceBool only, everything else is a named native_decide certificate. - kimchi's gate drops both hasse allowlist entries; all 91 roots reduce to standard axioms + certificates. - the terminal theorem kimchiVesta_run_sound_algebraic_ft's full closure is propext/Classical.choice/Quot.sound + kimchi_fiat_shamir_vesta + native_decide certificates (p_nsmul_Gpt, the field primality witnesses) — no curve axioms of any kind. - EndoMul faithfulness closes on exactly two certificates: the prime-order witness and the eigenvalue anchor. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD * formal: bump CompElliptic — field-file generator reproducibility fix The fork's generator scripts now emit the absolute field names (Fp/Fq), fixing the regenerate-and-diff CI gate on l-adic/CompElliptic#2. Scripts only; no Lean content change. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD * formal/pasta: drop the duplicate ℕ eigenvalue numerals pallas/vesta_lam_nat repeated the eigenvalue numerals just to put them in nsmul position for the native_decide anchors; pallas_lam.toNat does that from the single ℤ constant. The anchors keep their names (the gates pin them), the eigen proofs' cast step becomes pallas_lam = ↑pallas_lam.toNat by decide, and pallas_endoGpt joins its Vesta twin as private. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD * formal/pasta: eigen theorems construct their own nonsingularity pallas/vesta_eigen took the nonsingularity of the endomorphism image as a hypothesis (h' : Nonsingular (endo * x) y) — an artifact of the axiom shape, which could not construct proofs. But phi maps curve points to curve points ((beta*x)^3 = x^3, and on-curve implies nonsingular on a nonsingular curve), so the theorem now supplies it: new pallas/vesta_endo_nonsingular transport theorems, and the eigen conclusions read Point.some _ _ (pallas_endo_nonsingular h) = lam . Point.some _ _ h — one hypothesis, strictly stronger statement. EndoMul's call sites drop their second argument (their own h-phi-T-ns proof agrees by proof irrelevance). Also folds in the endo_cube privatization (no external consumers; out of the manifest). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD * formal/pasta: anchors speak about φ itself — endoGpt and its rfl bridges die The native_decide anchors were stated against hand-written image points (pallas/vesta_endoGpt := ⟨β·G.1, G.2, _⟩), re-related to the development's endomorphism by rfl bridges (pallas/vesta_endoPt_Gpt, SWPoint.ext_pair rfl). Worthless indirection: the anchors now read pallas_lam.toNat • Gpt = endoPt Pallas.curve rfl pallas_endo_cube Gpt — λ•G = φ(G) against THE φ used everywhere, native_decide evaluating the endomorphism directly. Four decls deleted (two image points, two bridges); the eq_lam_smul rewrite chains lose a step. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD * formal/pasta: inline endoPt into endoHom endoPt's only remaining role was endoHom's toFun; everything else — the anchors, the extension theorems, the eigen proofs — now applies the hom directly. Bonus: the hhom bridging haves in the eq_lam_smul proofs die, because map_zsmul rewrites straight into a goal that is syntactically a hom application. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD * formal/pasta: dissolve Curve.lean and Module.lean into Basic.lean pasta is now three modules, three stories: Basic (the unconditional group orders + the two-declaration generic vocabulary order/toAffine + the point-group Module instances with their computational reading), Endo (the GLV endomorphisms in full), Shifted (the wire scalar-shift algebra). The three Fact.out wrappers die properly this time: order_smul, order_prime, and short were dot-notation over Fact.out / one-line lemmas, inlined at their ~22 kimchi call sites (statements untouched — only proof text changes; the two gate-chain proofs get a local hshort : ... := Fact.out). The manifest's sugar section shrinks to the two genuine vocabulary entries, order and toAffine; the stale zsmul_mod and order_smul references leave refactor_baseline.lean. Gate: 13 pasta roots. deadcode 132/0. All four gates green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD * formal/pasta: order-primality theorems and their Fact wrappers collapse into named instances pallas/vesta_order_prime existed twice — a public theorem and an anonymous Fact instance wrapping it. One named instance each now carries the fact; the manifest and gate keep the same root names, and consumers were already reading it back with Fact.out. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD * formal: repin CompElliptic to fork main (l-adic/CompElliptic#2 merged) Content-identical to the previously pinned sync-branch tip — the pointer now sits on the merge commit on main. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD * formal/pasta: doc pass — statements only, no derivation narration Docstrings state what a declaration is; proofs show how. Removed the changelog register (former axioms / now theorems / PROVED), the re-told CompElliptic derivations (fibre bound, prime-order witnesses, cube-residue case), and the usage mechanics (Fact.out read-back, rewrite routes). Section headers reduce to titles; per-declaration docstrings to the claim plus at most a purpose note. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD --------- Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
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
2 participants
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.
Pins the Pallas and Vesta group orders to their known primes (
PALLAS_SCALAR_CARD,PALLAS_BASE_CARD) with no assumption. Mathlib has no Hasse bound forWeierstrassCurve, so instead of assuming it this uses an elementary point-count bound in its place — and drops theHasseBoundhypothesis the library previously carried.How
Fixing a prime-order curve group's order to
rneeds a prime-order witness ([r]·G = 𝒪, givingr ∣ #E) plus an upper bound on#E. The bound is elementary:y² = x³ + A·x + Bhas at most twoyperx, so#E(F) ≤ 2·#F + 1(card_le_two_mul_card_add_one). Looser than Hasse (a factor of ~2 vs2√q) but enough whenr ≈ #F, leaving a closed comparison of#Fandr. The Pasta cycle puts the curves on opposite sides:q, base fieldp < q):2p + 1 < 2qcloses it directly.p, base fieldq > p): only2q + 1 < 3p, so#E = 2pmust be excluded separately. It would need a 2-torsion point, i.e.y = 0, i.e.x³ = -5— but-5is not a cube in the Vesta base field.Trust
Nat.card (SWPoint curve) = …for both curves, resting onpropext, Classical.choice, Quot.soundplus a single inheritednative_decideaxiom — the≈2^254prime-order-witness scalar multiplication (q_nsmul_Gpt/p_nsmul_Gpt). NoHasseBound; every new general theorem (the fibre bound, the two pinning lemmas,neg_five_not_isCube) is on the standard three, per the README's rule for quantified theorems.Gpt/Gpt_ne_zerodischarge by kerneldecide, so they contribute nonative_decideaxioms.Notes
Fields/Residue.leanis new for one lemma.-5needs a cubic non-residue certificate, and Mathlib's residue theory is quadratic-only (noIsNthPow);not_exists_pow_eq_of_pow_ne_oneis the easy direction, which is all a negative needs.card_fibre_le_twouses the equal-or-negation identity (y₁ = ±y₂fromy₁² = y₂²) directly rather thanPolynomial.nthRoots— nonthRootsdependency, and the geometry is visible in the proof.Builds green (
lake build), no warnings, nosorry.🤖 Generated with Claude Code