Normalized MacWilliams identities

The weight enumerator of a dual code is the MacWilliams substitution divided by the cardinality of the code. For a self-dual code over a field of size q, homogeneity absorbs this factor into the variables: the enumerator is fixed by (X, Y) ↦ ((X + (q - 1) Y) / √q, (X - Y) / √q).

The statements allow values in arbitrary algebras, so they apply to polynomial variables as well as numerical evaluations. The coefficient normalization is over ℚ, whereas the variable normalization only requires an invertible square root of q. The real-algebra corollary uses the positive square root. The rational identity also holds over a finite commutative ring carrying a primitive additive character with values in a characteristic zero domain.

References

F. J. MacWilliams and N. J. A. Sloane, The Theory of Error-Correcting Codes, North-Holland (1977), Chapter 5, §2; W. C. Huffman and V. Pless, Fundamentals of Error-Correcting Codes, Cambridge University Press (2003), §7.2.

theorem Submodule.aeval_weightEnumerator_euclideanDual_of_isPrimitive {ι : Type u_1} [Fintype ι] {R : Type u_2} {S : Type u_3} [CommRing R] [Finite R] [DecidableEq R] [CommRing S] [IsDomain S] [CharZero S] {ψ : AddChar R S} (C : Submodule R (ι → R)) (hψ : ψ.IsPrimitive) {A : Type u_4} [CommRing A] [Algebra ℚ A] (x y : A) : (MvPolynomial.aeval ![x, y]) (↑C.euclideanDual).weightEnumerator = (↑(Nat.card ↥C))⁻¹ • (MvPolynomial.aeval ![x + (↑(Nat.card R) - 1) * y, x - y]) (↑C).weightEnumerator

The rational normalized MacWilliams identity over a finite commutative ring carrying a primitive additive character into a characteristic zero domain, evaluated in any commutative ℚ-algebra.

theorem Submodule.aeval_weightEnumerator_euclideanDual {ι : Type u_1} [Fintype ι] {F : Type u_2} [Field F] [Finite F] [DecidableEq F] (C : Submodule F (ι → F)) {A : Type u_3} [CommRing A] [Algebra ℚ A] (x y : A) : (MvPolynomial.aeval ![x, y]) (↑C.euclideanDual).weightEnumerator = (↑(Nat.card ↥C))⁻¹ • (MvPolynomial.aeval ![x + (↑(Nat.card F) - 1) * y, x - y]) (↑C).weightEnumerator

The rational normalized MacWilliams identity for a linear code over a finite field F with q elements: W_{C⊥}(x, y) = (1/#C) · W_C(x + (q-1)y, x - y). The variables may lie in any commutative ℚ-algebra, including ℚ[X, Y].

theorem Submodule.aeval_weightEnumerator_normalized_of_isSelfDual_of_mul_self {ι : Type u_1} [Fintype ι] {F : Type u_2} [Field F] [Finite F] [DecidableEq F] (C : Submodule F (ι → F)) {A : Type u_3} [CommRing A] (hC : C.IsSelfDual) (s t : A) (hs : s * s = ↑(Nat.card F)) (hst : t * s = 1) (x y : A) : (MvPolynomial.aeval ![t * (x + (↑(Nat.card F) - 1) * y), t * (x - y)]) (↑C).weightEnumerator = (MvPolynomial.aeval ![x, y]) (↑C).weightEnumerator

A self-dual code's weight enumerator is fixed by the MacWilliams substitution normalized by any invertible square root s of the alphabet size, with inverse t. This holds over any commutative ring containing such a square root.

theorem Submodule.aeval_weightEnumerator_normalized_of_isSelfDual {ι : Type u_1} [Fintype ι] {F : Type u_2} [Field F] [Finite F] [DecidableEq F] (C : Submodule F (ι → F)) {A : Type u_3} [CommRing A] [Algebra ℝ A] (hC : C.IsSelfDual) (x y : A) : (MvPolynomial.aeval ![(√↑(Nat.card F))⁻¹ • (x + (↑(Nat.card F) - 1) * y), (√↑(Nat.card F))⁻¹ • (x - y)]) (↑C).weightEnumerator = (MvPolynomial.aeval ![x, y]) (↑C).weightEnumerator

A self-dual code's weight enumerator is fixed by the normalized MacWilliams substitution. The variables may lie in any commutative real algebra; in particular this is an identity in ℝ[X, Y].