Completeness of the E₇ coroot enumeration #
The 126 coroots of type E₇ are enumerated in
TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E7.Basic as coordinate vectors in the
simple-coroot basis. This file proves that the enumeration is complete: a vector of Fin 7 → ℤ
whose E₇ norm is two is one of the listed coroots.
The proof realizes the E₇ lattice as the principal seven-node sublattice of the pinned E₈
lattice. Extending a coordinate vector by zero preserves its norm, so the existing completeness
theorem TauCeti.DynkinType.exists_e8Coroot_eq supplies an E₈ root. The 63-entry map below checks
that the positive E₈ roots with zero eighth coordinate are exactly the listed positive E₇
roots; the negative halves then agree automatically. This avoids a 126 × 126 reflection table.
Main result #
TauCeti.DynkinType.exists_e7Coroot_eq: every norm-two vector of theE₇simple-coroot lattice occurs in the pinned enumeration.
References #
The principal-subsystem realization and coordinates follow Bourbaki, Lie Groups and Lie
Algebras, Chapters 4--6, Plates VI and VII. The counting argument reuses the formal E₈ lattice
completeness development in
TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E8.Lattice.
The listed E₇ coroots are all the norm-two vectors of the simple-coroot lattice. The
enumeration of 126 coroots is complete.