Generator criteria for doubly-even binary codes

A binary code generated by a set of words is doubly even exactly when the generators have weights divisible by four and are pairwise orthogonal. For a matrix presentation, this becomes the finite check that each row has weight divisible by four and the Gram matrix vanishes. No independence of the generators is required.

These criteria allow double evenness of explicit binary codes, such as the extended binary Golay code, to be verified on a small generating family instead of enumerating every codeword. The key fact is that for two words of weight divisible by four, their sum has weight divisible by four exactly when their dot product vanishes.

References

W. C. Huffman and V. Pless, Fundamentals of Error-Correcting Codes, Chapter 9.

theorem TauCeti.BinaryCode.isDoublyEven_span_iff_of_isSelfOrthogonal {ι : Type u_1} [Fintype ι] {s : Set (ι → ZMod 2)} (hs : (Submodule.span (ZMod 2) s).IsSelfOrthogonal) : IsDoublyEven (Submodule.span (ZMod 2) s) ↔ ∀ x ∈ s, 4 ∣ hammingNorm x

In a self-orthogonal binary code, double evenness can be checked on any spanning set.

@[simp]

theorem TauCeti.BinaryCode.isDoublyEven_span_iff {ι : Type u_1} [Fintype ι] {s : Set (ι → ZMod 2)} : IsDoublyEven (Submodule.span (ZMod 2) s) ↔ (∀ x ∈ s, 4 ∣ hammingNorm x) ∧ ∀ x ∈ s, ∀ y ∈ s, x ⬝ᵥ y = 0

A binary span is doubly even exactly when the generators have weight divisible by four and every pair of generators is orthogonal.

@[simp]

theorem TauCeti.BinaryCode.isDoublyEven_generatedBy_iff {ι : Type u_1} {ρ : Type u_2} [Fintype ι] [Fintype ρ] {G : Matrix ρ ι (ZMod 2)} : IsDoublyEven G.generatedBy ↔ (∀ (r : ρ), 4 ∣ hammingNorm (G.row r)) ∧ G * G.transpose = 0

A binary row code is doubly even exactly when every row has weight divisible by four and its Gram matrix is zero. The matrix may have dependent rows or no rows.