Weight enumerators of repetition and single-parity-check codes

The repetition code consists of constant words, and the single-parity-check code consists of words whose coordinate sum is zero. They are Euclidean duals. Their homogeneous weight enumerators give explicit examples of the MacWilliams transform, alongside the zero code and the whole word space.

For a coordinate type of cardinality n over a finite alphabet with q letters, the positive-length repetition enumerator is X^n + (q - 1) Y^n, and the parity-check enumerator satisfies q W(X,Y) = (X + (q - 1) Y)^n + (q - 1) (X - Y)^n over the integers at every length. The nonempty hypothesis for the repetition formula matters: at length zero the repetition code has one word, rather than q words.

Together, the repetition and parity-check enumerators give an independent check of the MacWilliams identity. More generally, over a finite additive group A with q elements, the words with coordinate sum a have enumerator

q W(X,Y) = (X + (q - 1) Y)^n + (q - 1) (X - Y)^n    if a = 0,
q W(X,Y) = (X + (q - 1) Y)^n - (X - Y)^n            if a ≠ 0.

References

W. C. Huffman and V. Pless, Fundamentals of Error-Correcting Codes, Cambridge University Press (2003), §§1.2–1.4 and §7.2.

@[simp]

theorem TauCeti.weightEnumerator_repetitionCode (R : Type u_1) (ι : Type u_2) [Fintype ι] [Semiring R] [DecidableEq R] [Finite R] [Nonempty ι] : (↑(repetitionCode R ι)).weightEnumerator = MvPolynomial.X 0 ^ Fintype.card ι + (↑(Nat.card R) - 1) * MvPolynomial.X 1 ^ Fintype.card ι

The positive-length repetition code has enumerator X^n + (q - 1) Y^n.

theorem TauCeti.natCard_mul_weightEnumerator_setOf_sum_eq (ι : Type u_2) [Fintype ι] {A : Type u_3} [AddCommGroup A] [DecidableEq A] [Finite A] (a : A) : ↑(Nat.card A) * {x : ι → A | ∑ i : ι, x i = a}.weightEnumerator = (MvPolynomial.X 0 + (↑(Nat.card A) - 1) * MvPolynomial.X 1) ^ Fintype.card ι + (if a = 0 then ↑(Nat.card A) - 1 else -1) * (MvPolynomial.X 0 - MvPolynomial.X 1) ^ Fintype.card ι

The weight enumerator of a coset of the parity-check code. Over a finite additive group with q elements, the words of length n with coordinate sum a have enumerator W with q W(X,Y) = (X + (q - 1) Y)^n + (q - 1) (X - Y)^n when a = 0, and q W(X,Y) = (X + (q - 1) Y)^n - (X - Y)^n otherwise.

theorem TauCeti.natCard_mul_weightEnumerator_singleParityCheckCode (R : Type u_1) (ι : Type u_2) [Fintype ι] [Ring R] [Finite R] [DecidableEq R] : ↑(Nat.card R) * (↑(singleParityCheckCode R ι)).weightEnumerator = (MvPolynomial.X 0 + (↑(Nat.card R) - 1) * MvPolynomial.X 1) ^ Fintype.card ι + (↑(Nat.card R) - 1) * (MvPolynomial.X 0 - MvPolynomial.X 1) ^ Fintype.card ι

The integral weight-enumerator formula for a single-parity-check code at any length.