Weight-enumerator symmetries of binary codes #
The weight enumerator of a doubly-even code is invariant under multiplying its second argument
by a fourth root of unity. For a self-dual binary code, the MacWilliams substitution gives
W_C(X + Y, X - Y) = 2^(n/2) W_C(X, Y) in ℤ[X, Y]. Together these symmetries give the
length restriction for Type II codes.
Main statements #
IsDoublyEven.aeval_weightEnumerator_mul_second: the fourth-root symmetry over any commutative ring.IsDoublyEven.aeval_weightEnumerator_mul_I: its polynomial identity overℂ.aeval_weightEnumerator_add_sub_of_isSelfDual: the integral self-dual MacWilliams symmetry.
See Huffman and Pless, Fundamentals of Error-Correcting Codes, Chapters 7 and 9.
@[simp]
theorem
TauCeti.BinaryCode.IsDoublyEven.aeval_weightEnumerator_mul_second
{ι : Type u_1}
[Fintype ι]
{C : LinearCode (ZMod 2) ι}
{R : Type u_2}
[CommRing R]
(hC : IsDoublyEven C)
{ζ : R}
(hζ : ζ ^ 4 = 1)
(x y : R)
:
(MvPolynomial.aeval ![x, ζ * y]) (↑C).weightEnumerator = (MvPolynomial.aeval ![x, y]) (↑C).weightEnumerator
The weight enumerator of a doubly-even code is unchanged when its second argument is
multiplied by a fourth root of unity. Taking R = ℂ[X,Y] gives the polynomial symmetry.
theorem
TauCeti.BinaryCode.IsDoublyEven.aeval_weightEnumerator_mul_I
{ι : Type u_1}
[Fintype ι]
{C : LinearCode (ZMod 2) ι}
(hC : IsDoublyEven C)
:
Replacing Y by iY leaves the homogeneous weight enumerator of a doubly-even code
unchanged, as a polynomial identity over ℂ.
theorem
TauCeti.BinaryCode.aeval_weightEnumerator_add_sub_of_isSelfDual
{ι : Type u_1}
[Fintype ι]
{C : LinearCode (ZMod 2) ι}
(hC : Submodule.IsSelfDual C)
:
(MvPolynomial.aeval ![MvPolynomial.X 0 + MvPolynomial.X 1, MvPolynomial.X 0 - MvPolynomial.X 1]) (↑C).weightEnumerator = 2 ^ (Fintype.card ι / 2) * (↑C).weightEnumerator
The integral MacWilliams symmetry of a self-dual binary code.