Eisenstein - #33
Draft
dannywillems wants to merge 4 commits into
Draft
Conversation
Mechanically checks the finite claims behind Eisenstein recoding for GLV on j = 0 curves. No elliptic curves are involved: every finite statement is a kernel `decide` over a 64-element ring, so all censused results sit at the standard-axioms tier and no `native_decide` appears in the module. `Eisenstein R` is `R[X]/(X^2 + X + 1)` as a pair of coefficients. Modelling it parametrically rather than as a quotient type is what keeps the finite statements decidable: `Eisenstein` commutes with base change, so `Eisenstein (ZMod (2^w))` IS the quotient `Z[omega]/2^w` and inherits `Fintype` and `DecidableEq` from `ZMod`. It is deliberately not `Zsqrtd (-3)`, which is the suborder of index 2 and would be wrong precisely where the 2-adic structure matters, while still typechecking. Basic.lean: the `CommRing` instance, conjugation, the norm form of discriminant -3, its multiplicativity, functoriality, and the universal property `evalHom` -- evaluation at any root of `X^2 + X + 1`, which is the bridge to the curve side, since the GLV scalar satisfies exactly that relation. Mod.lean: 2 is inert, so `Z[omega]/2` is F_4; and an element is even exactly when both coordinates are, so halving is exact and coordinate-wise. Orbits.lean: the 48 odd classes, which are the units because inertness makes `Z[omega]/8` local with maximal ideal (2); the unit action on those is free, so `48 / 6 = 8` is a theorem and not a division; and eight representatives whose orbits are disjoint and cover all 48. It also settles the count over ALL nonzero residues, where the action is not free: -1 fixes the four 2-torsion classes while the other nonidentity units fix only zero, because `u - 1` then has odd norm and is invertible. So the count is Burnside's, 12 orbits including zero, and the three nonzero 2-torsion classes form one orbit of size 3 whose representative (4, 0) has two unit factorizations. `orbit_mul_unit` discharges the resulting obligation: the bucket does not depend on which factorization is chosen. The same norm computation gives more than the published argument. Since `N(u - 1)` is 1, 3 or 4 for the five nontrivial units, `2^w` can never divide `u - 1` for `w >= 2`, so the action is free on the units at every width and w = 3 is a cost choice rather than a structural one. Co-Authored-By: Claude <noreply@anthropic.com>
Completes the ring layer with the arithmetic proved over Z rather than checked
mod 8. Everything follows from one identity, `4*N = (2a - b)^2 + 3*b^2`, which
makes the norm positive definite and bounds the solutions of `N = 1` to a box
small enough to enumerate.
`isUnit_iff_norm_eq_one` and `isUnit_iff_mem_mu6Z`: the unit group of Z[omega]
is exactly mu_6 = {+-1, +-omega, +-omega^2}, six elements. Those are the six
automorphisms of a j = 0 curve, which is why the orbit structure in Orbits.lean
is the curve's own symmetry group acting.
`prime_two` states inertness abstractly rather than as a 16-case check: 2 is a
prime element of Z[omega]. The concrete input stays the decidable
`mul_eq_zero_mod_two`, transported along the reduction to F_4.
`not_two_pow_dvd_unit_sub_one` proves what the Orbits docstrings so far only
asserted. For a nontrivial unit u, `N(u - 1)` is 1, 3 or 4, while
`2^w | u - 1` would force `4^w | N(u - 1)` and so `4^w <= 4`. Hence the
reduction mu_6 -> (Z[omega]/2^w)^x is injective, and the unit action free on
the odd classes, for EVERY width w >= 2. The bound is tight: at w = 1 the
argument fails at `4 <= 4`, and indeed -1 is congruent to 1 mod 2, so the six
units collapse to three.
Five further results join the census, all at the standard-axioms tier.
Co-Authored-By: Claude <noreply@anthropic.com>
…perties
The module already showed Z[omega]/2 has four elements, no zero divisors, and
an inverse for every nonzero class. Those are the PROPERTIES of F_4; they did
not name the field. This closes that gap with an explicit isomorphism onto
`GaloisField 2 2`, which is Mathlib's F_4.
The route is the classification of finite fields: a finite field is determined
up to isomorphism by its cardinality, so a four-element field IS F_4. To use it
the quotient has to be a field rather than merely a domain, so:
`coeffHom` and `instAlgebra` (Basic.lean) make `R[omega]` an R-algebra, free of
rank two on {1, omega}. The isomorphism is then one of ZMod 2-algebras, so it
respects the coefficient embedding and not only the ring structure.
`invTwo` and `instFieldModTwo` give the field structure, and it stays
COMPUTABLE: the multiplicative group of a four-element field has order 3, so
`x^3 = 1` for nonzero x and therefore `x⁻¹ = x^2`. Inversion is squaring, not a
search, and `mul_invTwo` is a four-case `decide`.
`algEquivGaloisField` and `nonempty_ringEquiv_galoisField` are the
identification itself. It is noncomputable because the classification produces
the isomorphism by choice, but it still censuses at the standard-axioms tier.
Why this is worth stating rather than leaving implicit: being F_4 is exactly
what INERT means. Were 2 split, the quotient would be F_2 x F_2, which also has
four elements but has zero divisors and is not a field. Everything downstream
that treats "odd" and "unit" as interchangeable mod 2^w, and the locality of
Z[omega]/2^w with maximal ideal (2), rests on the field case rather than the
product case, so the distinction is load-bearing.
Co-Authored-By: Claude <noreply@anthropic.com>
Proves the FORM of the automorphism group of `y^2 = x^3 + B` over a field with
a primitive cube root of unity z: the maps are exactly
(x, y) |-> (z^k * x, +-y), k in {0, 1, 2}
and there are six of them. Instantiated on Pallas and Vesta.
Why that is the shape: preserving `y^2 = x^3 + B` lets x be scaled only by a
cube root, since that is what leaves x^3 alone, and lets y carry only a sign,
since that is what leaves y^2 alone. The curve constrains nothing else. So the
group is mu_3 x mu_2, cyclic of order 6 because 3 and 2 are coprime, generated
by sigma(x, y) = (z*x, -y) with sigma^3 the negation map and sigma^2 the
endomorphism used for GLV.
`Endomorphism.lean` is carried over unchanged from the earlier GLV endomorphism
work; it compiles against current main as-is and supplies the x-scaling phi
together with the proof that it commutes with the chord-and-tangent group law.
The six automorphisms are then built by composing phi with negation, so no new
reasoning about the addition formulas is needed. `phi_eq_lambda_nsmul` is NOT
carried over, since it depends on a HasseBound that does not exist here; the
underlying `phiPt_eq_nsmul` does come across and needs only `Nat.card`.
Automorphisms.lean: `autPt_x` and `autPt_y` are the form itself, and the second
is the one that matters downstream -- the map only ever applies a sign to y and
never mixes the coordinates, which is why an orbit has three x-coordinates but
a single +-y pair. `autPt_add` makes each map a homomorphism, `autPt_comp` the
group law (exponents add, signs multiply), and `autEquiv` packages each as an
additive automorphism with the inverse of (k, s) given by (2k, s).
It also connects the two places mu_6 shows up. The unit group of Z[omega] is
mu_6, and `autOfUnit` makes the six units act as the six automorphisms:
`unitIndex` reads a unit eps*omega^k as its exponent and sign, `unitIndex_injOn`
shows the six units give six different maps, and `autOfUnit_mul` shows the
action is multiplicative. So the coincidence of the two mu_6's is a theorem
rather than a remark.
PastaAut.lean pins zeta for each curve and checks the six are genuinely
distinct at G = (-1, 2), so the automorphism group really does contain mu_6
rather than collapsing. `ZETA_quad` records that zeta satisfies the same
relation `z^2 + z + 1 = 0` that the adjoined omega does, which is what
identifies the x-scalings with the cube roots of unity in Z[omega].
Everything is kernel `decide`; the two `native_decide` strings in
Endomorphism.lean are docstring prose, not uses. Nine further results join the
census, all at the standard-axioms tier.
Co-Authored-By: Claude <noreply@anthropic.com>
dannywillems
marked this pull request as draft
September 2, 2026 17:45
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.
No description provided.