Algebraic codes and code-lattice constructions

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremThe MacWilliams identity#

for a linear code C over a finite field F with q elements, #C · W_{C⊥}(X, Y) = W_C(X + (q - 1) Y, X - Y) in ℤ[X, Y].

Submodule.natCard_mul_weightEnumerator_euclideanDual.{u_1, u_4} {ι : Type u_1} [Fintype ι]
  {F : Type u_4} [Field F] [Finite F] [DecidableEq F] (C : Submodule F (ι → F)) :
  ↑(Nat.card ↥C) * (↑C.euclideanDual).weightEnumerator =
    (MvPolynomial.aeval
        ![MvPolynomial.X 0 + (↑(Nat.card F) - 1) * MvPolynomial.X 1,
          MvPolynomial.X 0 - MvPolynomial.X 1])
      (↑C).weightEnumerator
Lean

Formalized in Tau Ceti as Submodule.natCard_mul_weightEnumerator_euclideanDual.

Sources
LeanSubmodule.natCard_mul_weightEnumerator_euclideanDual
Uses 1 · Used by 1
Statement usesSet.weightEnumerator
Used byTauCeti.BinaryCode.IsTypeII.eight_dvd_card

TheoremTauCeti.BinaryCode.IsTypeII.eight_dvd_card#

A Type II binary code has length divisible by eight.

TauCeti.BinaryCode.IsTypeII.eight_dvd_card.{u_1} {ι : Type u_1} [Fintype ι]
  {C : TauCeti.LinearCode (ZMod 2) ι} (hC : TauCeti.BinaryCode.IsTypeII C) : 8 ∣ Fintype.card ι
Lean

Formalized in Tau Ceti as TauCeti.BinaryCode.IsTypeII.eight_dvd_card.

Sources
LeanTauCeti.BinaryCode.IsTypeII.eight_dvd_card
Uses 2
Proof usesThe MacWilliams identity · Set.weightEnumerator

TheoremTauCeti.BinaryGolay.weightEnumerator_code#

The homogeneous weight enumerator is X²⁴ + 759 X¹⁶Y⁸ + 2576 X¹²Y¹² + 759 X⁸Y¹⁶ + Y²⁴.

TauCeti.BinaryGolay.weightEnumerator_code :
  (↑TauCeti.BinaryGolay.code).weightEnumerator =
    MvPolynomial.X 0 ^ 24 + 759 * MvPolynomial.X 0 ^ 16 * MvPolynomial.X 1 ^ 8 +
          2576 * MvPolynomial.X 0 ^ 12 * MvPolynomial.X 1 ^ 12 +
        759 * MvPolynomial.X 0 ^ 8 * MvPolynomial.X 1 ^ 16 +
      MvPolynomial.X 1 ^ 24
Lean

Formalized in Tau Ceti as TauCeti.BinaryGolay.weightEnumerator_code.

Sources
LeanTauCeti.BinaryGolay.weightEnumerator_code
Uses 1
Statement usesSet.weightEnumerator

TheoremGluing 2 ℤ²⁴ along the Golay code gives an even lattice, because the glue is quadratic-isotropic# 

TauCeti.BinaryGolay.isEven_ofIsotropicSubgroup_codeInZeroLatticeDiscriminantGroup :
  ((TauCeti.ConstructionA.zeroLattice 2 (Fin 24)).ofIsotropicSubgroup ⋯
      (TauCeti.ConstructionA.codeInZeroLatticeDiscriminantGroup 2 (Fin 24)
        (Submodule.toAddSubgroup TauCeti.BinaryGolay.code))
      TauCeti.BinaryGolay.isIsotropic_codeInZeroLatticeDiscriminantQuadraticModule).IsEven
Lean

Formalized in Tau Ceti as TauCeti.BinaryGolay.isEven_ofIsotropicSubgroup_codeInZeroLatticeDiscriminantGroup.

Sources
LeanTauCeti.BinaryGolay.isEven_ofIsotropicSubgroup_codeInZeroLatticeDiscriminantGroup
Uses 4
Statement usesTauCeti.ConstructionA.lattice · TauCeti.FiniteQuadraticModule · TauCeti.IntegralLattice · TauCeti.IntegralLattice.discriminantQuadraticModule

TheoremGluing 2 ℤ²⁴ along the Golay code gives a unimodular lattice, because the glue is Lagrangian# 

TauCeti.BinaryGolay.isUnimodular_ofIsotropicSubgroup_codeInZeroLatticeDiscriminantGroup :
  ((TauCeti.ConstructionA.zeroLattice 2 (Fin 24)).ofIsotropicSubgroup ⋯
      (TauCeti.ConstructionA.codeInZeroLatticeDiscriminantGroup 2 (Fin 24)
        (Submodule.toAddSubgroup TauCeti.BinaryGolay.code))
      TauCeti.BinaryGolay.isIsotropic_codeInZeroLatticeDiscriminantQuadraticModule).IsUnimodular
Lean

Formalized in Tau Ceti as TauCeti.BinaryGolay.isUnimodular_ofIsotropicSubgroup_codeInZeroLatticeDiscriminantGroup.

Sources
LeanTauCeti.BinaryGolay.isUnimodular_ofIsotropicSubgroup_codeInZeroLatticeDiscriminantGroup
Uses 5
Statement usesTauCeti.ConstructionA.lattice · TauCeti.FiniteQuadraticModule · TauCeti.IntegralLattice · TauCeti.IntegralLattice.discriminantQuadraticModule
Proof usesGluing along a code gives a unimodular lattice exactly when the code is Lagrangian

DefinitionThe Golay root lattice is A₁²⁴#

The zero-code lattice generated by all Golay roots is isometric to the orthogonal sum of twenty-four copies of the existing A₁ lattice. The ambient isometry doubles every coordinate.

TauCeti.BinaryGolay.rootLatticeIsometry :
  (TauCeti.IntegralLattice.a1.coordinatePower (Fin 24)).Isometry
    (TauCeti.ConstructionA.zeroLattice 2 (Fin 24))
Lean

Formalized in Tau Ceti as TauCeti.BinaryGolay.rootLatticeIsometry.

Sources
LeanTauCeti.BinaryGolay.rootLatticeIsometry
Uses 2
Statement usesTauCeti.ConstructionA.lattice · TauCeti.IntegralLattice

TheoremOver ℤ/2^r with r ≥ 1, a self-orthogonal code has an even unimodular Construction A lattice exactly when it is a Type II code# 

TauCeti.ConstructionA.isEven_and_isUnimodular_integralLattice_iff_isTypeII.{u_1} {ι : Type u_1}
  [Fintype ι] {r : ℕ} (hr : r ≠ 0) (C : TauCeti.AdditiveCode (ZMod (2 ^ r)) ι)
  (hC :
    (AddSubgroup.toZModSubmodule (2 ^ r)) C ≤
      ((AddSubgroup.toZModSubmodule (2 ^ r)) C).euclideanDual) :
  (TauCeti.ConstructionA.integralLattice (2 ^ r) C hC).IsEven ∧
      (TauCeti.ConstructionA.integralLattice (2 ^ r) C hC).IsUnimodular ↔
    TauCeti.TwoPowCode.IsTypeII r C
Lean

Formalized in Tau Ceti as TauCeti.ConstructionA.isEven_and_isUnimodular_integralLattice_iff_isTypeII.

Sources
LeanTauCeti.ConstructionA.isEven_and_isUnimodular_integralLattice_iff_isTypeII
Uses 3
Statement usesTauCeti.ConstructionA.lattice · TauCeti.IntegralLattice
Proof usesTauCeti.FiniteQuadraticModule

DefinitionThe discriminant bilinear module of a Construction A lattice is C⊥ / C#

For a self-orthogonal additive code C over ℤ/m, the discriminant bilinear module of P_m(C) is the orthogonal quotient of C in the coordinate alphabet (ℤ/m)^ι.

TauCeti.ConstructionA.discriminantBilinearOrthogonalQuotientIsometry.{u_1} (m : ℕ) [NeZero m]
  (ι : Type u_1) [Fintype ι] (C : TauCeti.AdditiveCode (ZMod m) ι)
  (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) :
  (TauCeti.ConstructionA.integralLattice m C hC).discriminantBilinearModule.Isometry
    (((TauCeti.FiniteBilinearModule.zmodStandard m).coordinatePower ι).orthogonalQuotient C)
Lean

Formalized in Tau Ceti as TauCeti.ConstructionA.discriminantBilinearOrthogonalQuotientIsometry.

Sources
LeanTauCeti.ConstructionA.discriminantBilinearOrthogonalQuotientIsometry
Uses 2
Statement usesTauCeti.ConstructionA.lattice · TauCeti.IntegralLattice

TheoremGluing along a code gives a unimodular lattice exactly when the code is Lagrangian#

For an even modulus and a quadratically isotropic code C, the overlattice of the zero-code lattice m ℤ^ι glued along the discriminant subgroup of C is unimodular exactly when C equals its orthogonal complement in the coordinate alphabet (ℤ/m)^ι.

TauCeti.ConstructionA.isUnimodular_ofIsotropicSubgroup_codeInZeroLatticeDiscriminantGroup_iff.{u_1}
  (m : ℕ) [NeZero m] (ι : Type u_1) [Fintype ι] (hm : Even m) (C : TauCeti.AdditiveCode (ZMod m) ι)
  (hC : ((TauCeti.FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).IsIsotropic C) :
  ((TauCeti.ConstructionA.zeroLattice m ι).ofIsotropicSubgroup ⋯
        (TauCeti.ConstructionA.codeInZeroLatticeDiscriminantGroup m ι C) ⋯).IsUnimodular ↔
    ((TauCeti.FiniteBilinearModule.zmodStandard m).coordinatePower ι).IsLagrangian C
Lean

Formalized in Tau Ceti as TauCeti.ConstructionA.isUnimodular_ofIsotropicSubgroup_codeInZeroLatticeDiscriminantGroup_iff.

Sources
LeanTauCeti.ConstructionA.isUnimodular_ofIsotropicSubgroup_codeInZeroLatticeDiscriminantGroup_iff
Uses 5 · Used by 1
Statement usesTauCeti.ConstructionA.lattice · TauCeti.FiniteQuadraticModule · TauCeti.IntegralLattice · TauCeti.IntegralLattice.discriminantQuadraticModule
Proof usesEven overlattices correspond to quadratic-isotropic subgroups
Used byGluing 2 ℤ²⁴ along the Golay code gives a unimodular lattice, because the glue is Lagrangian

DefinitionSet.weightEnumerator#

The homogeneous Hamming weight enumerator W_C(X, Y) = ∑_w A_w(C) X^(n-w) Y^w, where n is the length, A_w(C) is the weight distribution, and the variables 0, 1 are X, Y.

Set.weightEnumerator.{u_1, u_2} {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)]
  [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) : MvPolynomial (Fin 2) ℤ
Lean

Formalized in Tau Ceti as Set.weightEnumerator.

Sources
LeanSet.weightEnumerator
Used by 3
Used byTauCeti.BinaryCode.IsTypeII.eight_dvd_card · TauCeti.BinaryGolay.weightEnumerator_code · The MacWilliams identity

DefinitionTauCeti.ConstructionA.lattice#

The rational carrier of Construction A: the integer vectors reducing to the additive code C modulo m.

TauCeti.ConstructionA.lattice.{u_1} {ι : Type u_1} (m : ℕ) (C : AddSubgroup (ι → ZMod m)) :
  Submodule ℤ (ι → ℚ)
Lean

Formalized in Tau Ceti as TauCeti.ConstructionA.lattice.

Sources
LeanTauCeti.ConstructionA.lattice
Used by 12
Used byGluing 2 ℤ²⁴ along the Golay code gives a unimodular lattice, because the glue is Lagrangian · Gluing 2 ℤ²⁴ along the Golay code gives an even lattice, because the glue is quadratic-isotropic · Gluing along a code gives a unimodular lattice exactly when the code is Lagrangian · Over ℤ/2^r with r ≥ 1, a self-orthogonal code has an even unimodular Construction A lattice exactly when it is a Type II code · The discriminant bilinear module of a Construction A lattice is C⊥ / C · The Golay root lattice is A₁²⁴ · Construction B · Construction B vectors have norm at least four · The carrier decomposition of the Leech lattice · The Leech lattice · The Leech lattice is even · The Leech lattice is unimodular, being glued along a Lagrangian subgroup

DefinitionTauCeti.monomialAutEquivEuclideanDual#

The monomial automorphism groups of a linear code and of its Euclidean dual are isomorphic, by taking contragredients.

TauCeti.monomialAutEquivEuclideanDual.{u_2, u_4} {ι : Type u_2} {K : Type u_4} [Field K] [Fintype ι]
  [DecidableEq ι] (C : Submodule K (ι → K)) :
  ↥(TauCeti.monomialAut C) ≃* ↥(TauCeti.monomialAut C.euclideanDual)
Lean

Formalized in Tau Ceti as TauCeti.monomialAutEquivEuclideanDual.

Sources
LeanTauCeti.monomialAutEquivEuclideanDual

TheoremTauCeti.IsMonomialEquivalent.hammingMinDist_eq#

Monomially equivalent codes have the same minimum distance.

TauCeti.IsMonomialEquivalent.hammingMinDist_eq.{u_1, u_2, u_3} {R : Type u_3} {ι : Type u_1}
  {κ : Type u_2} [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} [Fintype ι]
  [Fintype κ] [DecidableEq R] (h : TauCeti.IsMonomialEquivalent C D) :
  (↑C).hammingMinDist = (↑D).hammingMinDist
Lean

Formalized in Tau Ceti as TauCeti.IsMonomialEquivalent.hammingMinDist_eq.

Sources
LeanTauCeti.IsMonomialEquivalent.hammingMinDist_eq

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.