Established in scope
Glue elements, two orbits, spinor swap and halfway stage are explicitly formalized
In the question: Formal carrier core: unbounded Pascal uniqueness and finite glue
The concrete element/orbit and arithmetic statements are available. No fresh kernel run, nor a newly checked single Lean theorem about all abstract subgroups or lattice isomorphisms. The general subgroup conclusion also uses finite group theory; concrete E8 basis embedding and physical carrier selection are separate.
Read the exact result, assumptions and evidence
Result
In Fin4 x Fin4 with qZ=(5x^2+3y^2) mod8, named Lean declarations classify all six isotropic elements and four odd-coordinate isotropic generators. Explicit orbit identities give H1 and H2; klein_not_isotropic gives the nonisotropic Klein witness, spinor_swap_exchanges swaps the two orbits, and unique_halfway_stage classifies the only nonzero isotropic order-two element (2,2). Index and sector arithmetic are additional separate declarations.
Required assumptions
- Specified finite carrier discriminant form
The model is El=Fin4 x Fin4 with componentwise addition modulo4 and qZ(x,y)=(5x^2+3y^2) mod8. Its identification with a concrete physical carrier is not inferred without premises.
Original evidence
- GlueUniqueness.lean lines 34–132
Source checked at this snapshot
Original location and fingerprint
experiments/lean4-carrier-rigidity/TfptCarrier/GlueUniqueness.lean
51e98673e96f4344fec729c2874a947dcc1f31f5787983af3267e113fd329df2
- 005-source.tex lines 166–182
Source checked at this snapshot
Original location and fingerprint
documents/tfpt_1_architecture_e8/sections/005-source.tex
2de406bb3e912bb795eca44e8552d11040413587aba14b3924e07b145b91bdcd
finding:finite-carrier-glue-elements-orbits-and-halfway