formal: prove the eigen relations, consolidate the GLV story, delete the Hasse axioms - #247
Merged
Merged
Conversation
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
There was a problem hiding this comment.
Your trial has ended. Reactivate Greptile to resume code reviews.
…ioms
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
martyall
force-pushed
the
eigen-discharge
branch
from
July 16, 2026 21:46
dd80662 to
9d23a71
Compare
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
…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
changed the title
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
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
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
…ges 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
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
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
…se 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
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
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
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.
Summary
Three commits that end with the workspace declaring zero curve axioms:
Eigen discharge — the CM eigenvalue relations
Pasta.{pallas,vesta}_eigenwere axioms; now theorems. Proof:(x,y) ↦ (βx,y)withβ³ = 1commutes with the short-Weierstrassa = 0addition over any field (pure field algebra, junk-division cases degrade consistently) → anAddMonoidHomonSWPoint→ prime order makes the group cyclic on the generator → anative_decideanchorλ • G = φ(G)pins the eigenvalue there →toPttransports to the MathlibPointstatements. The anchors are the onlynative_decides in the workspace packages; the gates permit exactly those two declarations by name.GLV consolidation — constants (β, λ, cube-root proofs), the endomorphism machinery, the anchors, the eigen theorems, and the lattice short-basis bounds now all live in
Pasta/Endo.lean, reading top-to-bottom as one story. Everything non-interface isprivate(including the formerly-publiceigen_of_hasselayer).Constants.leandeleted;Basic.leanreduced to the trust base + group orders.Hasse deletion — CompElliptic upstream (daira/CompElliptic#6, synced into our fork as l-adic/CompElliptic#2, submodule bumped) pins both Pasta group orders unconditionally (fibre bound
#E ≤ 2·#F + 1+ prime-order witness; Vesta's#E = 2pcase dies because−5is not a cube).Pasta.{pallas,vesta}_hasseare deleted —HasseBoundno longer exists to state them — and all their plumbing evaporates.Trust accounting (after)
Lean.ofReduceBoolonly.native_decidecertificates.kimchiVesta_run_sound_algebraic_ft's full closure:propext, Classical.choice, Quot.sound+kimchi_fiat_shamir_vesta(the declared FS axiom) + certificates (p_nsmul_Gpt, the field primality witnesses). No curve axioms of any kind.deadcode fix (commit 1)
isOursnow demanglesprivatenames — the walk previously refused to enter private helpers, so anything referenced only through one reported dead (this also unhid two genuinely dead private kimchi helpers).Verification
lake build Kimchi Snarky Pasta Poseidon FixtureKit Bulletproof— green (8587 jobs)🤖 Generated with Claude Code
https://claude.ai/code/session_01RhavGeUhGukSRQTRH6JEaD