Type II codes over ℤ/2^r

Following Dougherty, Gulliver, and Harada, a Type II code over ℤ/2^r is an additive code which is self-dual for the ℤ/2^r dot product and all of whose Euclidean weights are divisible by 2^(r+1). For r ≥ 1, these are exactly the codes whose Construction A lattices are even and unimodular.

The notion is specific to moduli which are powers of two, so the predicate is stated only for codes over ℤ/2^r; it is not a predicate on codes over an arbitrary ℤ/m. The intended range is r ≥ 1: at r = 0 every code over the trivial ring ℤ/1 satisfies it. The evenness characterization therefore requires r ≠ 0. At r = 1 it is the binary Type II condition, since binary Euclidean weights are Hamming weights.

References

• 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.

def TauCeti.TwoPowCode.IsTypeII {ι : Type u_1} [Fintype ι] (r : ℕ) (C : AdditiveCode (ZMod (2 ^ r)) ι) : Prop

A Type II code over ℤ/2^r is an additive code which is Euclidean self-dual and all of whose Euclidean weights are divisible by 2^(r+1).

theorem TauCeti.TwoPowCode.isTypeII_iff {ι : Type u_1} [Fintype ι] {r : ℕ} {C : AdditiveCode (ZMod (2 ^ r)) ι} : IsTypeII r C ↔ (AddSubgroup.toZModSubmodule (2 ^ r)) C = ((AddSubgroup.toZModSubmodule (2 ^ r)) C).euclideanDual ∧ ∀ x ∈ C, 2 ^ (r + 1) ∣ euclideanWeight x

theorem TauCeti.TwoPowCode.IsTypeII.eq_euclideanDual {ι : Type u_1} [Fintype ι] {r : ℕ} {C : AdditiveCode (ZMod (2 ^ r)) ι} (hC : IsTypeII r C) : (AddSubgroup.toZModSubmodule (2 ^ r)) C = ((AddSubgroup.toZModSubmodule (2 ^ r)) C).euclideanDual

A Type II code over ℤ/2^r is Euclidean self-dual.

theorem TauCeti.TwoPowCode.IsTypeII.le_euclideanDual {ι : Type u_1} [Fintype ι] {r : ℕ} {C : AdditiveCode (ZMod (2 ^ r)) ι} (hC : IsTypeII r C) : (AddSubgroup.toZModSubmodule (2 ^ r)) C ≤ ((AddSubgroup.toZModSubmodule (2 ^ r)) C).euclideanDual

A Type II code over ℤ/2^r is Euclidean self-orthogonal.

theorem TauCeti.TwoPowCode.IsTypeII.two_pow_succ_dvd_euclideanWeight {ι : Type u_1} [Fintype ι] {r : ℕ} {C : AdditiveCode (ZMod (2 ^ r)) ι} (hC : IsTypeII r C) {x : ι → ZMod (2 ^ r)} (hx : x ∈ C) : 2 ^ (r + 1) ∣ euclideanWeight x

Every word of a Type II code over ℤ/2^r has Euclidean weight divisible by 2^(r+1).