Construction B

For a binary linear code C with coordinates ι, Construction B is the sublattice of the Construction A carrier {x ∈ ℤ^ι : x mod 2 ∈ C} cut out by the congruence ∑ xᵢ ≡ 0 (mod 4). It carries the Construction A form, the dot product halved, and is an integral lattice whenever C is self-orthogonal.

When C is even, every Construction A vector has an even coordinate sum, so half the coordinate sum reduced modulo two is an additive character ConstructionB.sumHalf of the Construction A carrier. Its kernel is the Construction B carrier, and it is surjective as soon as there is a coordinate. Hence Construction B has index two in Construction A, and its discriminant is four times the discriminant of Construction A.

When C is doubly even, write a Construction A vector as c + 2z, where c is the 0/1 lift of its reduction modulo two. It lies in Construction B exactly when ∑ zᵢ is even, because the weight of c is divisible by four. Construction B then inherits evenness from Construction A.

Applied to the extended binary Golay code, Construction B is the index-two sublattice of the Golay Construction A lattice from which the Leech lattice is obtained by gluing in an odd shift.

Main declarations

• TauCeti.ConstructionB.lattice: the Construction B carrier, characterized by mem_lattice and intCast_mem_lattice.
• TauCeti.ConstructionB.val_add_two_mul_mem_lattice_iff: the parity description of membership for doubly even codes.
• TauCeti.ConstructionB.sumHalf: half the coordinate sum modulo two, with kernel ker_sumHalf and surjectivity sumHalf_surjective.
• TauCeti.ConstructionB.relIndex_lattice: Construction B has index two in Construction A.
• TauCeti.ConstructionB.integralLattice: Construction B as an integral lattice, with discriminant_integralLattice and isEven_integralLattice.

References

• J. Leech and N. J. A. Sloane, Sphere packing and error-correcting codes, Canadian Journal of Mathematics 23 (1971), reprinted as Chapter 5 of J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups.

def TauCeti.ConstructionB.lattice {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) : Submodule ℤ (ι → ℚ)

The rational carrier of Construction B: the Construction A vectors of the binary code C whose coordinate sum is divisible by four.

theorem TauCeti.ConstructionB.mem_lattice {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} {x : ι → ℚ} : x ∈ lattice C ↔ x ∈ ConstructionA.lattice 2 (Submodule.toAddSubgroup C) ∧ ∃ (k : ℤ), ∑ i : ι, x i = 4 * ↑k

Membership in Construction B: a Construction A vector whose coordinate sum is divisible by four.

theorem TauCeti.ConstructionB.lattice_le {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) : lattice C ≤ ConstructionA.lattice 2 (Submodule.toAddSubgroup C)

Construction B lies inside Construction A.

@[simp]

theorem TauCeti.ConstructionB.intCast_mem_lattice {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (z : ι → ℤ) : (fun (i : ι) => ↑(z i)) ∈ lattice C ↔ (fun (i : ι) => ↑(z i)) ∈ C ∧ 4 ∣ ∑ i : ι, z i

An integer vector lies in Construction B exactly when it reduces to a codeword modulo two and its coordinate sum is divisible by four.

theorem TauCeti.ConstructionB.val_add_two_mul_mem_lattice_iff {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (hC : BinaryCode.IsDoublyEven C) {c : ι → ZMod 2} (hc : c ∈ C) (z : ι → ℤ) : (fun (i : ι) => ↑(c i).val + 2 * ↑(z i)) ∈ lattice C ↔ Even (∑ i : ι, z i)

The parity form of Construction B. For a doubly even code, the Construction A vector c + 2z, with c the 0/1 lift of a codeword, lies in Construction B exactly when ∑ zᵢ is even. Together with ConstructionA.exists_eq_val_add_mul this describes every Construction B vector.

instance TauCeti.ConstructionB.isLattice {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) : Submodule.IsLattice ℚ (lattice C)

The Construction B carrier is a full lattice: it lies in Construction A and contains four times every Construction A vector.

Half the coordinate sum

noncomputable def TauCeti.ConstructionB.sumHalf {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (hC : BinaryCode.IsEven C) : ↥(ConstructionA.lattice 2 (Submodule.toAddSubgroup C)) →+ ZMod 2

Half the coordinate sum modulo two, an additive character of the Construction A carrier of an even binary code. Its kernel is the Construction B carrier, by ker_sumHalf.

theorem TauCeti.ConstructionB.sumHalf_apply_of_sum_eq {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (hC : BinaryCode.IsEven C) {x : ↥(ConstructionA.lattice 2 (Submodule.toAddSubgroup C))} {k : ℤ} (hk : ∑ i : ι, ↑x i = 2 * ↑k) : (sumHalf C hC) x = ↑k

sumHalf sends a vector of coordinate sum 2k to k modulo two.

theorem TauCeti.ConstructionB.sumHalf_eq_zero_iff {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (hC : BinaryCode.IsEven C) (x : ↥(ConstructionA.lattice 2 (Submodule.toAddSubgroup C))) : (sumHalf C hC) x = 0 ↔ ↑x ∈ lattice C

sumHalf vanishes exactly on the Construction B carrier.

theorem TauCeti.ConstructionB.ker_sumHalf {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (hC : BinaryCode.IsEven C) : (sumHalf C hC).ker = (lattice C).toAddSubgroup.addSubgroupOf (ConstructionA.lattice 2 (Submodule.toAddSubgroup C)).toAddSubgroup

The kernel of sumHalf is the Construction B carrier.

theorem TauCeti.ConstructionB.sumHalf_surjective {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) [Nonempty ι] (hC : BinaryCode.IsEven C) : Function.Surjective ⇑(sumHalf C hC)

sumHalf is surjective once there is a coordinate: it sends 2eᵢ to 1.

theorem TauCeti.ConstructionB.relIndex_lattice {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) [Nonempty ι] (hC : BinaryCode.IsEven C) : (lattice C).toAddSubgroup.relIndex (ConstructionA.lattice 2 (Submodule.toAddSubgroup C)).toAddSubgroup = 2

Construction B has index two in Construction A, for an even binary code with at least one coordinate.

The integral lattice

noncomputable def TauCeti.ConstructionB.integralLattice {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (hC : Submodule.IsSelfOrthogonal C) : IntegralLattice (ι → ℚ)

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.

@[simp]

theorem TauCeti.ConstructionB.integralLattice_carrier {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (hC : Submodule.IsSelfOrthogonal C) : (integralLattice C hC).carrier = lattice C

The carrier of the bundled Construction B lattice.

@[simp]

theorem TauCeti.ConstructionB.integralLattice_form {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (hC : Submodule.IsSelfOrthogonal C) : (integralLattice C hC).form = ConstructionA.form 2

The form of the bundled Construction B lattice is the halved dot product of Construction A.

instance TauCeti.ConstructionB.isNondegenerate_integralLattice {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (hC : Submodule.IsSelfOrthogonal C) : (integralLattice C hC).IsNondegenerate

Construction B is nondegenerate, since its form is that of Construction A.

theorem TauCeti.ConstructionB.isPosDef_integralLattice {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (hC : Submodule.IsSelfOrthogonal C) : (integralLattice C hC).IsPosDef

Construction B is positive definite.

@[simp]

theorem TauCeti.ConstructionB.finrank_integralLattice {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (hC : Submodule.IsSelfOrthogonal C) : Module.finrank ℤ ↥(integralLattice C hC).carrier = Fintype.card ι

Construction B has rank equal to the length of the code.

theorem TauCeti.ConstructionB.discriminant_integralLattice {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) [Nonempty ι] (hC : Submodule.IsSelfOrthogonal C) : (integralLattice C hC).discriminant = 4 * (ConstructionA.integralLattice 2 (Submodule.toAddSubgroup C) ⋯).discriminant

The discriminant of Construction B is four times that of Construction A, for a self-orthogonal binary code with at least one coordinate.

theorem TauCeti.ConstructionB.isEven_integralLattice {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} (hC : BinaryCode.IsDoublyEven C) : (integralLattice C ⋯).IsEven

Construction B of a doubly even code is even, as a sublattice of the even Construction A lattice.