The extended binary Golay code

The extended binary Golay code is the row space of the systematic matrix [I₁₂ | B], where B is the bordered reverse-circulant matrix over ZMod 2. The first twelve coordinates recover the message. The generator is also a parity-check matrix.

This doubly-even self-dual binary code has parameters [24, 12, 8]. Its self-duality and divisibility of weights by four make it an input to Construction A, which associates an even unimodular lattice to such a code. The weight distribution and homogeneous weight enumerator describe the numbers of codewords of each weight, and every one of the twenty-four coordinates is met by a codeword of weight eight, an octad.

The matrix convention is that of Huffman and Pless, Fundamentals of Error-Correcting Codes, §1.9.1 and Chapter 9.

def TauCeti.BinaryGolay.block : Matrix (Fin 12) (Fin 12) (ZMod 2)

The bordered reverse-circulant block in the binary Golay generator. Its interior is indexed by sums modulo eleven in {0, 1, 3, 4, 5, 9}.

@[simp]

theorem TauCeti.BinaryGolay.block_apply (i j : Fin 12) : block i j = if i = 0 then if j = 0 then 0 else 1 else if j = 0 then 1 else if (↑i + ↑j - 2) % 11 ∈ {0, 1, 3, 4, 5, 9} then 1 else 0

The entries of the border and of the reverse-circulant interior.

def TauCeti.BinaryGolay.generator : Matrix (Fin 12) (Fin 24) (ZMod 2)

The systematic generator [I₁₂ | B], in the conventional coordinate order.

noncomputable def TauCeti.BinaryGolay.code : LinearCode (ZMod 2) (Fin 24)

The extended binary Golay code, with twenty-four ordered coordinates.

theorem TauCeti.BinaryGolay.code_def : code = generator.generatedBy

The code is the row space of its displayed generator.

theorem TauCeti.BinaryGolay.generator_def : generator = fun (i : Fin 12) => Fin.append (1 i) (block i)

The generator has the systematic block form [I₁₂ | B].

@[simp]

theorem TauCeti.BinaryGolay.generator_castAdd (i j : Fin 12) : generator i (Fin.castAdd 12 j) = if i = j then 1 else 0

The information columns of the generator form the identity matrix.

@[simp]

theorem TauCeti.BinaryGolay.generator_addNat (i j : Fin 12) : generator i (j.addNat 12) = block i j

The last twelve columns of the generator form block.

@[simp]

theorem TauCeti.BinaryGolay.vecMul_generator (a : Fin 12 → ZMod 2) : Matrix.vecMul a generator = Fin.append a (Matrix.vecMul a block)

Encoding a message keeps it in the first twelve coordinates and appends its product with block.

@[simp]

theorem TauCeti.BinaryGolay.mem_code_iff {x : Fin 24 → ZMod 2} : x ∈ code ↔ ∃ (a : Fin 12 → ZMod 2), Fin.append a (Matrix.vecMul a block) = x

Membership in the extended Golay code is systematic encoding of a message.

@[simp]

theorem TauCeti.BinaryGolay.generator_mul_transpose_eq_zero : generator * generator.transpose = 0

The generator has zero Euclidean Gram matrix.

theorem TauCeti.BinaryGolay.vecMul_generator_injective : Function.Injective fun (a : Fin 12 → ZMod 2) => Matrix.vecMul a generator

Encoding is injective because the generator is systematic.

noncomputable def TauCeti.BinaryGolay.encodingEquiv : (Fin 12 → ZMod 2) ≃ₗ[ZMod 2] ↥code

Systematic encoding gives a linear equivalence between messages and codewords.

@[simp]

theorem TauCeti.BinaryGolay.encodingEquiv_apply (a : Fin 12 → ZMod 2) : ↑(encodingEquiv a) = Fin.append a (Matrix.vecMul a block)

The encoding equivalence sends a message to its systematic encoding.

@[simp]

theorem TauCeti.BinaryGolay.encodingEquiv_symm_apply (x : ↥code) (i : Fin 12) : encodingEquiv.symm x i = ↑x (Fin.castAdd 12 i)

Decoding reads the first twelve coordinates.

@[simp]

theorem TauCeti.BinaryGolay.finrank_code : Module.finrank (ZMod 2) ↥code = 12

The extended binary Golay code has dimension twelve.

@[simp]

theorem TauCeti.BinaryGolay.rank_generator : generator.rank = 12

Its displayed generator has rank twelve.

@[simp]

theorem TauCeti.BinaryGolay.natCard_code : Nat.card ↥code = 4096

The extended binary Golay code has 4096 words.

theorem TauCeti.BinaryGolay.isSelfDual_code : Submodule.IsSelfDual code

The extended binary Golay code is Euclidean self-dual.

@[simp]

theorem TauCeti.BinaryGolay.euclideanDual_code : Submodule.euclideanDual code = code

The Euclidean dual of the extended binary Golay code is the code itself.

@[simp]

theorem TauCeti.BinaryGolay.checkedBy_generator : generator.checkedBy = code

The same matrix is a parity-check matrix for the extended Golay code.

theorem TauCeti.BinaryGolay.hammingNorm_mem {x : Fin 24 → ZMod 2} (hx : x ∈ code) : hammingNorm x ∈ {0, 8, 12, 16, 24}

The only weights of the extended binary Golay code are 0, 8, 12, 16, and 24.

@[simp]

theorem TauCeti.BinaryGolay.isDoublyEven_code : BinaryCode.IsDoublyEven code

The extended binary Golay code is doubly even.

theorem TauCeti.BinaryGolay.isTypeII_code : BinaryCode.IsTypeII code

The extended binary Golay code is Type II: doubly even and Euclidean self-dual.

@[simp]

theorem TauCeti.BinaryGolay.weightDistribution_code (w : ℕ) : (↑code).weightDistribution w = if w = 0 ∨ w = 24 then 1 else if w = 8 ∨ w = 16 then 759 else if w = 12 then 2576 else 0

The full weight distribution of the extended binary Golay code.

@[simp]

theorem TauCeti.BinaryGolay.weightEnumerator_code : (↑code).weightEnumerator = MvPolynomial.X 0 ^ 24 + 759 * MvPolynomial.X 0 ^ 16 * MvPolynomial.X 1 ^ 8 + 2576 * MvPolynomial.X 0 ^ 12 * MvPolynomial.X 1 ^ 12 + 759 * MvPolynomial.X 0 ^ 8 * MvPolynomial.X 1 ^ 16 + MvPolynomial.X 1 ^ 24

The homogeneous weight enumerator is X²⁴ + 759 X¹⁶Y⁸ + 2576 X¹²Y¹² + 759 X⁸Y¹⁶ + Y²⁴.

theorem TauCeti.BinaryGolay.exists_mem_code_hammingNorm_eq_eight_and_apply_ne_zero (i : Fin 24) : ∃ x ∈ code, hammingNorm x = 8 ∧ x i ≠ 0

Every coordinate of the extended binary Golay code is met by an octad, a codeword of weight eight.

theorem TauCeti.BinaryGolay.code_le_singleParityCheckCode : code ≤ singleParityCheckCode (ZMod 2) (Fin 24)

The extended binary Golay code has only even weights, so it lies in the single-parity-check code.

@[simp]

theorem TauCeti.BinaryGolay.hammingMinDist_code : (↑code).hammingMinDist = 8

The extended binary Golay code has minimum distance eight.

theorem TauCeti.BinaryGolay.eight_le_hammingNorm {x : Fin 24 → ZMod 2} (hx : x ∈ code) (hx0 : x ≠ 0) : 8 ≤ hammingNorm x

Every nonzero codeword of the extended binary Golay code has weight at least eight.