Evenness of Construction A lattices

The norm of a Construction A vector is the dot product of any integer lift divided by the modulus, so the lattice P_m(C) is even exactly when 2m divides ∑ i, zᵢ² for every integer lift z of a codeword. That divisibility is precisely the vanishing of the quadratic value

q_m(c) = (∑ i, lift (cᵢ)²) / (2m)  mod ℤ

of the standard coordinate discriminant module over ℤ/m, which exists when m is even. So for even m the Construction A lattice of C is even exactly when C is a quadratically isotropic subgroup of that module, equivalently when every codeword has Euclidean weight divisible by 2m. For odd m and a nonempty coordinate type the lattice is never even, because it always contains a coordinate vector of norm m.

At m = 2 the quadratic value is a quarter of the Hamming weight, so evenness of the lattice is divisibility of all codeword weights by four. With the unimodularity criterion, a self-orthogonal binary code therefore has an even unimodular Construction A lattice exactly when it is a Type II code, doubly even and Euclidean self-dual (isEven_and_isUnimodular_integralLattice_two_iff_isTypeII); like every Construction A lattice it is also positive definite (isPosDef_integralLattice). More generally, 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: self-dual with every Euclidean weight divisible by 2^(r+1).

References

• W. Ebeling, Lattices and Codes, §1.3, Proposition 1.3, for the binary criteria.
• A. Munemasa and H. Tamura, The codes and the lattices of Hadamard matrices, §4, for the general ℤ/m normalization.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 7, §§2, 6, for Construction A and its Type II form.
• S. T. Dougherty, T. A. Gulliver, and M. Harada, Type II self-dual codes over finite rings and even unimodular lattices, J. Algebraic Combin. 9 (1999), 233–250, for Type II codes over ℤ/2^r and their even unimodular Construction A lattices.

theorem TauCeti.ConstructionA.isEven_integralLattice_iff_intCast (m : ℕ) [NeZero m] {ι : Type u_1} [Fintype ι] (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : (integralLattice m C hC).IsEven ↔ ∀ (z : ι → ℤ), (fun (i : ι) => ↑(z i)) ∈ C → 2 * ↑m ∣ ∑ i : ι, z i ^ 2

A Construction A lattice is even exactly when 2m divides the sum of the squares of every integer lift of a codeword.

theorem TauCeti.ConstructionA.isEven_integralLattice_iff_isIsotropic (m : ℕ) [NeZero m] {ι : Type u_1} [Fintype ι] (hm : Even m) (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : (integralLattice m C hC).IsEven ↔ ((FiniteQuadraticModule.zmodStandard m hm).coordinatePower ι).IsIsotropic C

Over an even modulus, a Construction A lattice is even exactly when its code is quadratically isotropic in the standard coordinate discriminant module over ℤ/m.

theorem TauCeti.ConstructionA.isEven_integralLattice_iff (m : ℕ) [NeZero m] {ι : Type u_1} [Fintype ι] (hm : Even m) (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : (integralLattice m C hC).IsEven ↔ ∀ x ∈ C, 2 * m ∣ ∑ i : ι, (x i).val ^ 2

Over an even modulus, a Construction A lattice is even exactly when 2m divides the sum of the squares of the canonical representatives of every codeword.

theorem TauCeti.ConstructionA.isEven_integralLattice_iff_euclideanWeight (m : ℕ) [NeZero m] {ι : Type u_1} [Fintype ι] (hm : Even m) (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : (integralLattice m C hC).IsEven ↔ ∀ x ∈ C, 2 * m ∣ euclideanWeight x

Over an even modulus, a Construction A lattice is even exactly when every codeword has Euclidean weight divisible by 2m.

theorem TauCeti.ConstructionA.not_isEven_integralLattice_of_odd (m : ℕ) [NeZero m] {ι : Type u_1} [Fintype ι] (hm : Odd m) [Nonempty ι] (C : AddSubgroup (ι → ZMod m)) (hC : (AddSubgroup.toZModSubmodule m) C ≤ ((AddSubgroup.toZModSubmodule m) C).euclideanDual) : ¬(integralLattice m C hC).IsEven

Over an odd modulus a Construction A lattice is never even: the coordinate vector m eᵢ has norm m.

The binary case

theorem TauCeti.ConstructionA.exists_sum_eq_two_mul {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (hC : BinaryCode.IsEven C) {x : ι → ℚ} (hx : x ∈ lattice 2 (Submodule.toAddSubgroup C)) : ∃ (k : ℤ), ∑ i : ι, x i = 2 * ↑k

Every Construction A vector of an even binary code has an even coordinate sum.

theorem TauCeti.ConstructionA.isEven_integralLattice_two_iff {ι : Type u_1} [Fintype ι] (C : AddSubgroup (ι → ZMod 2)) (hC : (AddSubgroup.toZModSubmodule 2) C ≤ ((AddSubgroup.toZModSubmodule 2) C).euclideanDual) : (integralLattice 2 C hC).IsEven ↔ ∀ x ∈ C, 4 ∣ hammingNorm x

A Construction A lattice at modulus two is even exactly when every codeword weight is divisible by four.

theorem TauCeti.ConstructionA.isEven_integralLattice_two_iff_isDoublyEven {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (hC : (AddSubgroup.toZModSubmodule 2) (Submodule.toAddSubgroup C) ≤ ((AddSubgroup.toZModSubmodule 2) (Submodule.toAddSubgroup C)).euclideanDual) : (integralLattice 2 (Submodule.toAddSubgroup C) hC).IsEven ↔ BinaryCode.IsDoublyEven C

A Construction A lattice at modulus two is even exactly when its binary linear code is doubly even.

theorem TauCeti.ConstructionA.isEven_and_isUnimodular_integralLattice_two_iff_isTypeII {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) (hC : Submodule.IsSelfOrthogonal C) : (integralLattice 2 (Submodule.toAddSubgroup C) ⋯).IsEven ∧ (integralLattice 2 (Submodule.toAddSubgroup C) ⋯).IsUnimodular ↔ BinaryCode.IsTypeII C

A self-orthogonal binary linear code has an even unimodular Construction A lattice exactly when it is a Type II code, doubly even and Euclidean self-dual.

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

The Construction A lattice of a doubly even binary linear code is even. Like every Construction A lattice it is also positive definite, by isPosDef_integralLattice.

Type II codes over ℤ/2^r

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

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.

theorem TauCeti.ConstructionA.isEven_integralLattice_of_isTypeII {ι : Type u_1} [Fintype ι] {r : ℕ} (hr : r ≠ 0) {C : AdditiveCode (ZMod (2 ^ r)) ι} (hC : TwoPowCode.IsTypeII r C) : (integralLattice (2 ^ r) C ⋯).IsEven

The Construction A lattice of a Type II code over ℤ/2^r, r ≥ 1, is even.

theorem TauCeti.ConstructionA.isUnimodular_integralLattice_of_isTypeII {ι : Type u_1} [Fintype ι] {r : ℕ} {C : AdditiveCode (ZMod (2 ^ r)) ι} (hC : TwoPowCode.IsTypeII r C) : (integralLattice (2 ^ r) C ⋯).IsUnimodular

The Construction A lattice of a Type II code over ℤ/2^r, r ≥ 1, is unimodular.