Coordinatewise Hamming character transform

Proved

CodingTheory.hammingCoordinateCharacterSum

by Rui Chao · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

charactersumscodingtheoryerror-correctingcodesfinitefieldsweightenumerator

Let $F$ be a finite field of cardinality $q$ , let $\iota$ be a finite coordinate type of cardinality $n$ , and let $\psi:F\to\mathbb C$ be a primitive additive character. For every word $c\in F^\iota$ and all $X,Y\in\mathbb C$ ,

\sum_{v\in F^\iota} X^{n-\operatorname{wt}(v)}Y^{\operatorname{wt}(v)} \psi(\langle c,v\rangle) = \bigl(X+(q-1)Y\bigr)^{n-\operatorname{wt}(c)} \bigl(X-Y\bigr)^{\operatorname{wt}(c)}.

This identity packages the coordinatewise finite-field transform used in the complete- and Hamming-weight-enumerator identities as an independently reusable statement.

Preamble

import Definitions.Def_CodingTheory
import Mathlib.NumberTheory.LegendreSymbol.Complex

Formal statement

namespace CodingTheory

open scoped BigOperators

/-- The coordinatewise character sum that produces the MacWilliams variable transform. -/
theorem hammingCoordinateCharacterSum
    (F ι : Type*) [Field F] [Fintype F] [DecidableEq F]
    [Fintype ι] [DecidableEq ι]
    (ψ : AddChar F ℂ) (hψ : ψ.IsPrimitive)
    (c : Word F ι) (X Y : ℂ) :
    (∑ v : Word F ι,
        X ^ (Fintype.card ι - hammingNorm v) * Y ^ hammingNorm v *
          ψ ((dotForm F ι) c v)) =
      (X + ((Fintype.card F - 1 : ℕ) : ℂ) * Y) ^
          (Fintype.card ι - hammingNorm c) *
        (X - Y) ^ hammingNorm c := by sorry

end CodingTheory

Source

F. J. MacWilliams and N. J. A. Sloane, The Theory of Error-Correcting Codes, Chapter 5, Lemma 9, p. 143, proof of Theorem 10, pp. 144–145, and proof of Theorem 13, p. 146, https://books.google.com/books?id=nv6WCJgcjxcC, chapter DOI: 10.1016/S0924-6509(08)70530-0; Violetta Weger, Coding Theory, Definition 11.10 and Lemma 11.11, pp. 157–158, and polynomial formula p. 159, https://home.cit.tum.de/~wvi/CT.pdf

Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

For every pair of types $F$ and $\iota$ , assuming that $F$ is a field equipped with a finite enumeration and decidable equality and that $\iota$ is equipped with a finite enumeration and decidable equality, let $\psi:F\to\mathbb C$ be an additive character—meaning $\psi(0)=1$ and $\psi(a+b)=\psi(a)\psi(b)$ for all $a,b\in F$ —which is primitive in the precise sense that, for every nonzero $a\in F$ , the character $x\mapsto\psi(ax)$ is not the constant-one character. For every arbitrary word $c:\iota\to F$ (with no requirement that $c$ belong to any code) and every $X,Y\in\mathbb C$ , define $\operatorname{wt}(u)=|\{i\in\iota:u(i)\ne0\}|$ . Then

\sum_{v:\iota\to F} X^{|\iota|-\operatorname{wt}(v)} Y^{\operatorname{wt}(v)} \psi\!\left(\sum_{i\in\iota}c(i)v(i)\right) = \left(X+\bigl((|F|-1)_{\mathbb N}\bigr)_{\mathbb C}Y\right)^{|\iota|-\operatorname{wt}(c)} (X-Y)^{\operatorname{wt}(c)}.

The sum ranges over all functions $v:\iota\to F$ , not over a specified code, and the argument of $\psi$ is the coordinatewise dot product $\sum_{i\in\iota}c(i)v(i)$ in $F$ . Every exponent is a natural number; each subtraction in an exponent is natural-number subtraction, which is truncated at zero, although $\operatorname{wt}(u)\le|\iota|$ because it counts a subset of the coordinates. Likewise, $|F|-1$ is computed in $\mathbb N$ before being coerced into $\mathbb C$ ; the field assumptions make $F$ nontrivial, so its finite cardinality is at least two. The statement includes the case $\iota=\varnothing$ , arbitrary zero or nonzero values of $X$ and $Y$ , and zero exponents, with complex natural powers using the convention $Z^0=1$ , including $0^0=1$ .

Human review

Endorsed by Shuze Chen · Sep 10, 2026
Endorsed by Rui Chao · Sep 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph