Finite-field linear codes and Hamming weight enumerators

Word. For arbitrary types $F$ and $\iota$, a word over $F$ with coordinate set $\iota$ is defined to be an arbitrary function $\iota \to F$. No algebraic, finiteness, or decidable-equality assumptions are imposed. In particular, if $\iota$ is empty, there is exactly one such word, regardless of $F$.

LinearCode. For arbitrary types $F$ and $\iota$, assuming $F$ is a field, a linear code over $F$ with coordinate set $\iota$ is defined to be an $F$-submodule of the function space $\iota \to F$. Neither $F$ nor $\iota$ is assumed finite here. Every such code contains the zero word and therefore is nonempty; if $\iota$ is empty, the word space has only its zero element.

dotForm. For arbitrary types $F$ and $\iota$, assuming that $F$ is a field and that $\iota$ is finite, dotForm is the $F$-bilinear form on words $u,v:\iota\to F$ given by the coordinatewise sum $\operatorname{dotForm}(u,v)=\sum_{i\in\iota}u_i v_i$. No decidable-equality assumption on $\iota$ is required. The quantification permits $\iota$ to be empty, in which case the sum is empty and the bilinear form is identically zero.

dualCode. For arbitrary types $F$ and $\iota$, assuming that $F$ is a field and that $\iota$ is finite, and for every $F$-submodule $C\subseteq(\iota\to F)$, the dual code is defined to be the orthogonal submodule of $C$ under the coordinatewise bilinear form: it consists of precisely those words $w:\iota\to F$ such that $\sum_{i\in\iota}c_iw_i=0$ for every $c\in C$. No finiteness or decidable-equality assumption on $F$ is imposed. Empty $\iota$ is included; then the word space has one element, every displayed sum is zero, and the orthogonal submodule is the whole one-element word space.

hammingWeightEnumeratorPolynomial. For arbitrary types $F$ and $\iota$, assuming that $F$ is a field, that both $F$ and $\iota$ are finite, and that decidable equalities on both types are supplied, and for every linear code $C\subseteq(\iota\to F)$, this defines a polynomial with integer coefficients in two variables indexed by the two-element type $\operatorname{Fin}(2)$, namely variables $X_0$ and $X_1$. Writing $\operatorname{wt}(c)$ for the Hamming norm of the word $c$, i.e. the number of coordinates at which $c$ is nonzero, the polynomial is $\displaystyle \sum_{c\in C}X_0^{\,|\iota|-\operatorname{wt}(c)}X_1^{\,\operatorname{wt}(c)}.$ The code is finite under the stated assumptions, and the sum ranges over all of its elements, each contributing one monomial; codewords of the same weight therefore contribute repeatedly and produce the corresponding integer coefficient. The subtraction in the first exponent is natural-number subtraction, which is a total operation truncated at zero. The assumptions allow $\iota$ to be empty; then the word space and its only linear code contain exactly one word of weight zero, so the polynomial is $X_0^0X_1^0=1$.

hammingWeightEnumerator. For arbitrary types $F$ and $\iota$, assuming that $F$ is a field, that $F$ and $\iota$ are finite, and that decidable equalities on both types are supplied, for every linear code $C\subseteq(\iota\to F)$ and every pair of complex numbers $X,Y$, the complex Hamming weight enumerator is defined by evaluating the preceding integer-coefficient polynomial after casting its coefficients into $\mathbb C$, substituting $X$ for the variable indexed by $0$ and $Y$ for the variable indexed by $1$. Equivalently, it is $\displaystyle \sum_{c\in C}X^{\,|\iota|-\operatorname{wt}(c)}Y^{\,\operatorname{wt}(c)}.$ There are no restrictions on $X$ or $Y$, so zero values are included and exponent-zero factors use the usual convention $z^0=1$, including $0^0=1$ as a monoid power. Empty $\iota$ is included and gives value $1$ for every $X,Y$.

hammingWeightEnumeratorPolynomial_eval. For arbitrary types $F$ and $\iota$, assuming that $F$ is a field, that $F$ and $\iota$ are finite, and that decidable equalities on both types are supplied, for every linear code $C\subseteq(\iota\to F)$ and all complex numbers $X,Y$, evaluating the integer polynomial $\sum_{c\in C}X_0^{\,|\iota|-\operatorname{wt}(c)}X_1^{\,\operatorname{wt}(c)}$ by casting integer coefficients into $\mathbb C$ and substituting $X$ and $Y$ for its two variables is equal to hammingWeightEnumerator applied to $C,X,Y$, which is defined to be that same evaluation. Thus the assertion is the defining equality and places no additional condition on the code or on $X,Y$; it also includes the empty-coordinate and zero-evaluation cases.