Documentation

TauCeti.InformationTheory.Coding.Binary.Basic

Even and doubly-even binary codes #

Binary Hamming weights detect Euclidean orthogonality: the dot product is the parity of the intersection of supports, and the weight of a sum subtracts twice that intersection. Consequently, a binary linear code whose weights are all divisible by four is self-orthogonal.

An even code is characterized by membership of the all-ones word in its dual. In particular, a binary self-dual code is even and contains the all-ones word. These facts supply the elementary parity constraints used in the study of doubly-even self-dual codes.

The conventions and weight-intersection argument follow Huffman and Pless, Fundamentals of Error-Correcting Codes, Chapters 1 and 9.

source
theorem TauCeti.hammingNorm_add_add_two_mul_card_support_inter {ι : Type u_1} [Fintype ι] (x y : ι → ZMod 2) :
hammingNorm (x + y) + 2 * {i : ι | x i ≠ 0 ∧ y i ≠ 0}.card = hammingNorm x + hammingNorm y

For binary words, the weight of a sum plus twice the size of the support intersection is the sum of the weights.

source
theorem TauCeti.dotProduct_eq_card_support_inter {ι : Type u_1} [Fintype ι] (x y : ι → ZMod 2) :
x ⬝ᵥ y = ↑{i : ι | x i ≠ 0 ∧ y i ≠ 0}.card

The binary dot product is the cardinality of the support intersection, reduced modulo two.

source
@[simp]
theorem TauCeti.dotProduct_self_eq_hammingNorm {ι : Type u_1} [Fintype ι] (x : ι → ZMod 2) :
x ⬝ᵥ x = ↑(hammingNorm x)

A binary word has self-dot-product equal to its weight modulo two.

source
@[simp]
theorem TauCeti.dotProduct_one_eq_hammingNorm {ι : Type u_1} [Fintype ι] (x : ι → ZMod 2) :
x ⬝ᵥ 1 = ↑(hammingNorm x)

Pairing a binary word with the all-ones word gives its weight modulo two.

source
theorem TauCeti.sum_val_eq_hammingNorm {ι : Type u_1} [Fintype ι] (x : ι → ZMod 2) :
∑ i : ι, (x i).val = hammingNorm x

The coordinates of the 0/1 lift of a binary word sum to its weight.

source
@[simp]
theorem TauCeti.four_dvd_hammingNorm_add_iff {ι : Type u_1} [Fintype ι] {x y : ι → ZMod 2} (hx : 4 ∣ hammingNorm x) (hy : 4 ∣ hammingNorm y) :
4 ∣ hammingNorm (x + y) ↔ x ⬝ᵥ y = 0

The sum of two binary words of weights divisible by four again has weight divisible by four exactly when the two words are orthogonal.

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

A binary code is even if all its words have even Hamming weight.

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

    A binary code is doubly even if all its Hamming weights are divisible by four.

    Instances For
      source
      theorem TauCeti.BinaryCode.isEven_iff {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} :
      IsEven C ↔ ∀ x ∈ C, Even (hammingNorm x)

      Evenness can be checked word by word.

      source
      theorem TauCeti.BinaryCode.isDoublyEven_iff {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} :
      IsDoublyEven C ↔ ∀ x ∈ C, 4 ∣ hammingNorm x

      Double evenness can be checked by divisibility of the weight of each word by four.

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

      Every doubly-even code is even.

      source
      theorem TauCeti.BinaryCode.IsEven.mono {ι : Type u_1} [Fintype ι] {C D : LinearCode (ZMod 2) ι} (hD : IsEven D) (hCD : C ≤ D) :
      IsEven C

      Evenness passes to subcodes.

      source
      theorem TauCeti.BinaryCode.IsDoublyEven.mono {ι : Type u_1} [Fintype ι] {C D : LinearCode (ZMod 2) ι} (hD : IsDoublyEven D) (hCD : C ≤ D) :
      IsDoublyEven C

      Double evenness passes to subcodes.

      source
      theorem TauCeti.BinaryCode.isEven_iff_one_mem_euclideanDual {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} :
      IsEven C ↔ 1 ∈ Submodule.euclideanDual C

      An even binary code is precisely one whose dual contains the all-ones word.

      source
      theorem TauCeti.BinaryCode.isEven_iff_le_singleParityCheckCode {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} :
      IsEven C ↔ C ≤ singleParityCheckCode (ZMod 2) ι

      For binary codes, evenness is exactly containment in the single-parity-check code.

      source
      theorem TauCeti.BinaryCode.isEven_of_isSelfOrthogonal {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} (hC : Submodule.IsSelfOrthogonal C) :
      IsEven C

      Every self-orthogonal binary code is even.

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

      A doubly-even binary linear code is self-orthogonal.

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

      A self-dual binary code contains the all-ones word.