The listed E₈ coroots are all the norm-two vectors #
The two hundred and forty coroots of type E₈ are enumerated in
TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E8.Basic as coordinate vectors in the
simple-coroot basis. This file proves that the enumeration is complete: a vector of
Fin 8 → ℤ whose E₈ norm is two is one of the two hundred and forty listed coroots
(TauCeti.DynkinType.exists_e8Coroot_eq).
Completeness is what turns reflection into a permutation of the root indices, since the reflection of a norm-two vector in another one is again of norm two, by an identity of bilinear algebra. It therefore replaces the two hundred and forty by two hundred and forty table of reflected indices that a direct construction would have to tabulate and check.
The argument #
The E₈ norm (v ᵥ* CartanMatrix.E 8) ⬝ᵥ v is the Gram form of the simple-coroot basis, so the
norm-two vectors are the minimal vectors of the E₈ lattice, read in that basis. They are counted
in the Euclidean model instead, where the lattice is described by congruences rather than by a Gram
matrix. To keep the coordinates integral the model is scaled by two: IsDoubledE8 describes
2 · Γ₈, whose vectors of norm eight are of exactly two shapes, (±2) in two coordinates and
(±1) in all eight with an even number of minus signs. Those shapes are the 112 even minimal
vectors (the norm-two roots of type D₈ scaled by two, supplied by
TauCeti.DynkinType.typeDRootEquiv) and the 128 odd minimal vectors with an even number of minus
signs.
The map e8DoubledEmbed sends the simple-coroot coordinates to the doubled Euclidean model by
multiplying with TauCeti.DynkinType.e8DoubledSimpleRoot, the shared integral table of
TauCeti.LinearAlgebra.RootSystem.E8Coordinates; it multiplies the norm by four, so it carries
norm-two vectors to norm-eight vectors of 2 · Γ₈. It is injective, and the listed coroots are two
hundred and forty distinct norm-two vectors, so their images already exhaust the two hundred and
forty vectors of the enumeration, and no norm-two vector is left over. The classification is used
only through this counting step: neither the surjectivity of e8DoubledEmbed onto 2 · Γ₈ nor the
equality of the two lattices is needed, and neither is proved. The counting scaffold built on the
table is therefore private to this file; the completeness statement is its only public consequence.
Main results #
TauCeti.DynkinType.exists_e8Coroot_eq: a norm-two vector of the simple-coroot lattice is one of the listedE₈coroots.
References #
The Euclidean model of the E₈ lattice and its two hundred and forty minimal vectors are Bourbaki,
Lie Groups and Lie Algebras, Chapters 4--6, Plate VII, and Conway--Sloane, Sphere Packings,
Lattices and Groups, chapter 4, section 8. This supports the target "a named datum per valid type"
in Layer 6 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md.
The doubled E₈ lattice and its vectors of norm eight #
The doubled Euclidean model #
Completeness of the enumeration #
The listed E₈ coroots are all the norm-two vectors of the simple-coroot lattice. The
enumeration of the two hundred and forty coroots is complete: nothing of norm two is missing from
it.