Niemeier glue data and explicit Leech constructions
The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.
DefinitionThe Leech lattice#
The Leech lattice, glued from the Golay Construction B lattice along the order-two
subgroup generated by the odd shift (-3/2, 1/2, …, 1/2). Its carrier is the union of the
Construction B lattice and its translate by the shift, by mem_leechLattice_carrier_iff.
TauCeti.leechLattice : TauCeti.IntegralLattice (Fin 24 → ℚ)
Uses 5 · Used by 3
TheoremThe Leech lattice is unimodular, being glued along a Lagrangian subgroup#
TauCeti.isUnimodular_leechLattice : TauCeti.leechLattice.IsUnimodular
TheoremThe Leech lattice is even#
TauCeti.isEven_leechLattice : TauCeti.leechLattice.IsEven
Uses 6
TheoremThe carrier decomposition of the Leech lattice#
a vector lies in the Leech lattice exactly when it or its difference with the odd shift lies in the Golay Construction B lattice.
TauCeti.mem_leechLattice_carrier_iff (x : Fin 24 → ℚ) :
x ∈ TauCeti.leechLattice.carrier ↔
x ∈ TauCeti.BinaryGolay.constructionBLattice.carrier ∨
x - TauCeti.leechShift ∈ TauCeti.BinaryGolay.constructionBLattice.carrier
Uses 6
TheoremThe norm bound for the Leech lattice in congruence coordinates#
Let m ∈ {0, 1} and let
b be an integer vector reducing to a Golay codeword modulo two, and put a = 2b + m 𝟙. If
∑ aᵢ ≡ 4m (mod 8) and a ≠ 0, then ∑ aᵢ² ≥ 32. These are the congruence conditions that
describe the Leech lattice in the coordinates x = a / 2, in which the halved dot product of x
with itself is ∑ aᵢ² / 8; so the bound says that such an x has norm at least 4.
TauCeti.BinaryGolay.thirtyTwo_le_sum_sq {m : ℤ} (hm : m = 0 ∨ m = 1) {b : Fin 24 → ℤ}
(hb : (fun i => ↑(b i)) ∈ TauCeti.BinaryGolay.code) (hsum : ∑ i, (2 * b i + m) ≡ 4 * m [ZMOD 8])
(hne : (fun i => 2 * b i + m) ≠ 0) : 32 ≤ ∑ i, (2 * b i + m) ^ 2
TheoremThe minimum norm of the discriminant class labelled a : ZMod (n + 1)#
The class
typeADiscriminantGroupEquiv n a = a.val • ω₁ of Aₙ has minimum norm
a.val (n + 1 - a.val) / (n + 1), the shortest norm of the Conway–Sloane glue label [a] of an
Aₙ component.
TauCeti.IntegralLattice.isLeast_form_self_typeADiscriminantGroupEquiv {n : ℕ} (a : ZMod (n + 1)) :
IsLeast
{q |
∃ x,
Submodule.Quotient.mk x = (TauCeti.IntegralLattice.typeADiscriminantGroupEquiv n) a ∧
((TauCeti.IntegralLattice.typeARootLattice n).form ↑x) ↑x = q}
(↑a.val * (↑n + 1 - ↑a.val) / (↑n + 1))
Lean
Formalized in Tau Ceti as TauCeti.IntegralLattice.isLeast_form_self_typeADiscriminantGroupEquiv.
Sources
- Tau Ceti documentation:
TauCeti.IntegralLattice.isLeast_form_self_typeADiscriminantGroupEquiv - Source of
TauCeti.IntegralLattice.isLeast_form_self_typeADiscriminantGroupEquivin TauCeti/LinearAlgebra/IntegralLattice/RootLattice/TypeA/CosetMinimum.lean - Tau Ceti roadmap status: Niemeier glue data and explicit Leech constructions
Uses 1
TheoremTauCeti.IntegralLattice.isLeast_form_self_orthogonalSum#
Attained least norms in two discriminant cosets add to the attained least norm of the corresponding coset of the orthogonal sum.
TauCeti.IntegralLattice.isLeast_form_self_orthogonalSum.{u, v} {V : Type u} {W : Type v}
[AddCommGroup V] [_root_.Module ℚ V] [AddCommGroup W] [_root_.Module ℚ W]
(L : TauCeti.IntegralLattice V) (M : TauCeti.IntegralLattice W) {a : L.DiscriminantGroup}
{b : M.DiscriminantGroup} {r s : ℚ}
(hL : IsLeast {q | ∃ x, Submodule.Quotient.mk x = a ∧ (L.form ↑x) ↑x = q} r)
(hM : IsLeast {q | ∃ y, Submodule.Quotient.mk y = b ∧ (M.form ↑y) ↑y = q} s) :
IsLeast
{q |
∃ x,
Submodule.Quotient.mk x = (L.discriminantGroupOrthogonalSumEquiv M).symm (a, b) ∧
((L.orthogonalSum M).form ↑x) ↑x = q}
(r + s)
Lean
Formalized in Tau Ceti as TauCeti.IntegralLattice.isLeast_form_self_orthogonalSum.
Sources
Uses 1
DefinitionThe positive root lattice of a simply-laced Dynkin type t#
the integral lattice on
Fin t.rank → ℚ whose Gram matrix in the standard basis is the Cartan matrix t.cartanMatrix.
The standard coordinate vectors are the simple roots, in Bourbaki numbering.
TauCeti.DynkinType.rootLattice (t : TauCeti.DynkinType) (ht : t.IsSimplyLaced) :
TauCeti.IntegralLattice (Fin t.rank → ℚ)
Uses 1 · Used by 1
DefinitionThe root lattice of type Dₙ is the checkerboard lattice#
For 4 ≤ n, the isometry
sends the i-th simple root to the i-th Bourbaki simple root of the Conway--Sloane coordinate
model {x ∈ ℤⁿ | ∑ xᵢ even}; both bases have Gram matrix CartanMatrix.D n.
TauCeti.DynkinType.rootLatticeIsometryCheckerboard (n : ℕ) (hn : 4 ≤ n)
(ht : (TauCeti.DynkinType.D n).IsSimplyLaced) :
((TauCeti.DynkinType.D n).rootLattice ht).Isometry (TauCeti.IntegralLattice.checkerboardLattice n)
Lean
Formalized in Tau Ceti as TauCeti.DynkinType.rootLatticeIsometryCheckerboard.
Sources
Uses 2
DefinitionConstruction B#
Construction B of a self-orthogonal binary linear code, as an integral lattice: the Construction A vectors whose coordinate sum is divisible by four, with the halved dot product.
TauCeti.ConstructionB.integralLattice.{u_1} {ι : Type u_1} [Fintype ι]
(C : TauCeti.LinearCode (ZMod 2) ι) (hC : Submodule.IsSelfOrthogonal C) :
TauCeti.IntegralLattice (ι → ℚ)
Uses 2 · Used by 4
TheoremConstruction B vectors have norm at least four#
If every nonzero codeword of C has
weight at least eight, every nonzero vector of the Construction B carrier has Construction A norm,
the dot product halved, at least 4.
TauCeti.ConstructionB.four_le_form_self.{u_1} {ι : Type u_1} [Fintype ι]
{C : TauCeti.LinearCode (ZMod 2) ι} (hC : ∀ c ∈ C, c ≠ 0 → 8 ≤ hammingNorm c) {x : ι → ℚ}
(hx : x ∈ TauCeti.ConstructionB.lattice C) (hne : x ≠ 0) :
4 ≤ ((TauCeti.ConstructionA.form 2) x) x
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.