Documentation

TauCeti.InformationTheory.Coding.Binary.TypeII

Type II binary codes #

A Type II binary code is a doubly-even Euclidean self-dual code. Its length is divisible by eight. The two weight-enumerator symmetries underlying this restriction are the MacWilliams substitution and invariance under multiplying the second variable by I. The latter symmetry is stated for any fourth root of unity in a commutative ring, so it applies both to evaluation at complex numbers and to polynomials with complex coefficients.

A direct sum of binary codes is Type II exactly when both summands are, and the Type II property is invariant under coordinate permutations, monomial equivalences, and semilinear equivalences. Over the binary field the latter two are coordinate permutations.

The argument follows the classical weight-enumerator proof of the length restriction; see Huffman and Pless, Fundamentals of Error-Correcting Codes, Chapter 9.

source
def TauCeti.BinaryCode.IsTypeII {ι : Type u_1} [Fintype ι] (C : LinearCode (ZMod 2) ι) :
Prop

A Type II binary code is doubly even and Euclidean self-dual.

Instances For
    source
    theorem TauCeti.BinaryCode.IsDoublyEven.isTypeII {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} (hC : IsDoublyEven C) (hdual : Submodule.IsSelfDual C) :
    IsTypeII C

    A doubly-even Euclidean self-dual binary code is Type II.

    source
    theorem TauCeti.BinaryCode.IsTypeII.isDoublyEven {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} (hC : IsTypeII C) :
    IsDoublyEven C

    Every Type II code is doubly even.

    source
    theorem TauCeti.BinaryCode.IsTypeII.isSelfDual {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} (hC : IsTypeII C) :
    Submodule.IsSelfDual C

    Every Type II code is Euclidean self-dual.

    source
    theorem TauCeti.TwoPowCode.isTypeII_one_iff {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} :
    IsTypeII 1 (Submodule.toAddSubgroup C) ↔ BinaryCode.IsTypeII C

    Over ℤ/2 = ℤ/2^1, the Type II condition for codes over ℤ/2^r is the binary Type II condition: binary Euclidean weights are Hamming weights.

    Direct sums and equivalences #

    source
    @[simp]
    theorem TauCeti.BinaryCode.isTypeII_directSum_iff {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} {κ : Type u_2} [Fintype κ] {D : LinearCode (ZMod 2) κ} :
    IsTypeII (Submodule.directSum C D) ↔ IsTypeII C ∧ IsTypeII D

    A direct sum of binary codes is Type II exactly when both summands are Type II.

    source
    theorem TauCeti.BinaryCode.IsTypeII.directSum {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} {κ : Type u_2} [Fintype κ] {D : LinearCode (ZMod 2) κ} (hC : IsTypeII C) (hD : IsTypeII D) :
    IsTypeII (Submodule.directSum C D)

    The direct sum of two Type II binary codes is Type II.

    source
    theorem TauCeti.BinaryCode.isTypeII_iff_of_isPermutationEquivalent {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} {κ : Type u_2} [Fintype κ] {D : LinearCode (ZMod 2) κ} (h : IsPermutationEquivalent C D) :
    IsTypeII C ↔ IsTypeII D

    The Type II property of binary codes is invariant under permutation equivalence.

    source
    theorem TauCeti.BinaryCode.IsTypeII.of_isPermutationEquivalent {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} {κ : Type u_2} [Fintype κ] {D : LinearCode (ZMod 2) κ} (hC : IsTypeII C) (h : IsPermutationEquivalent C D) :
    IsTypeII D

    Permutation equivalence preserves the Type II property of binary codes.

    source
    theorem TauCeti.BinaryCode.isTypeII_iff_of_isMonomialEquivalent {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} {κ : Type u_2} [Fintype κ] {D : LinearCode (ZMod 2) κ} (h : IsMonomialEquivalent C D) :
    IsTypeII C ↔ IsTypeII D

    The Type II property of binary codes is invariant under monomial equivalence.

    source
    theorem TauCeti.BinaryCode.IsTypeII.of_isMonomialEquivalent {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} {κ : Type u_2} [Fintype κ] {D : LinearCode (ZMod 2) κ} (hC : IsTypeII C) (h : IsMonomialEquivalent C D) :
    IsTypeII D

    Monomial equivalence preserves the Type II property of binary codes.

    source
    theorem TauCeti.BinaryCode.isTypeII_iff_of_isSemilinearEquivalent {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} {κ : Type u_2} [Fintype κ] {D : LinearCode (ZMod 2) κ} (h : IsSemilinearEquivalent C D) :
    IsTypeII C ↔ IsTypeII D

    The Type II property of binary codes is invariant under semilinear equivalence.

    source
    theorem TauCeti.BinaryCode.IsTypeII.of_isSemilinearEquivalent {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} {κ : Type u_2} [Fintype κ] {D : LinearCode (ZMod 2) κ} (hC : IsTypeII C) (h : IsSemilinearEquivalent C D) :
    IsTypeII D

    Semilinear equivalence preserves the Type II property of binary codes.

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

    A Type II binary code has length divisible by eight.