Character orthogonality over a linear code

Proved

CodingTheory.codeCharacterSum

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

characterorthogonalitycodingtheoryerror-correctingcodesfinitefields

Let $F$ be a finite field, let $\iota$ be a finite coordinate type, and let $C\subseteq F^\iota$ be a linear code. Let $\psi:F\to\mathbb C$ be a primitive additive character. For every word $v\in F^\iota$ ,

\sum_{c\in C}\psi\!\left(\sum_{i\in\iota}c_i v_i\right) = \begin{cases} |C|,&v\in C^\perp,\\ 0,&v\notin C^\perp. \end{cases}

This is character orthogonality over a linear code. It is a reusable finite-field form of the binary code/dual character identity stated in Chapter 5, Problem 13, and of the character relation underlying Lemma 11.

Preamble

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

Formal statement

namespace CodingTheory

open scoped BigOperators

/-- Character orthogonality over a linear code and its dual. -/
theorem codeCharacterSum
    (F ι : Type*) [Field F] [Fintype F] [DecidableEq F]
    [Fintype ι] [DecidableEq ι]
    (ψ : AddChar F ℂ) (hψ : ψ.IsPrimitive)
    (C : LinearCode F ι) (v : Word F ι) :
    letI := Fintype.ofFinite C
    (v ∈ dualCode F ι C →
        (∑ c : C, ψ ((dotForm F ι) (c : Word F ι) v)) = (Nat.card C : ℂ)) ∧
      (v ∉ dualCode F ι C →
        (∑ c : C, ψ ((dotForm F ι) (c : Word F ι) v)) = 0) := by sorry

end CodingTheory

Source

F. J. MacWilliams and N. J. A. Sloane, The Theory of Error-Correcting Codes, Chapter 5, Problem 13, p. 134 (binary form), Lemma 9, p. 143, and Lemma 11, pp. 144–145 (finite-field character/Fourier form), https://books.google.com/books?id=nv6WCJgcjxcC, chapter DOI: 10.1016/S0924-6509(08)70530-0; Violetta Weger, Coding Theory, Lemma 11.8, pp. 155–156, 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 finite field $F$ equipped with decidable equality, every finite coordinate type $\iota$ equipped with decidable equality, every additive character $\psi:F\to\mathbb C$ satisfying $\psi(0)=1$ and $\psi(x+y)=\psi(x)\psi(y)$ , and a proof that $\psi$ is primitive—meaning that for every nonzero $a\in F$ , the additive character $x\mapsto\psi(ax)$ is not identically $1$ —let $C$ be any $F$ -linear subspace of the word space $F^\iota=\{x:\iota\to F\}$ , and let $v\in F^\iota$ . Define $\langle x,y\rangle=\sum_{i\in\iota}x(i)y(i)$ , define the dual code by $C^\perp=\{w\in F^\iota:\langle c,w\rangle=0\text{ for every }c\in C\}$ , and define $S_C(v)=\sum_{c\in C}\psi(\langle c,v\rangle)$ , where the summation is over the subtype of codewords $c$ together with their membership proofs and each such $c$ is coerced to its underlying word. The declaration asserts precisely the conjunction

\bigl(v\in C^\perp\Longrightarrow S_C(v)=(|C|:\mathbb C)\bigr) \land \bigl(v\notin C^\perp\Longrightarrow S_C(v)=0\bigr),

where $|C|=\operatorname{Nat.card}(C)$ is the finite natural-number cardinality of $C$ , cast into $\mathbb C$ , and the $0$ on the right is complex zero. The local finite-type structure on $C$ is obtained from its finiteness, so no enumeration of $C$ is an additional hypothesis. Both implications are asserted simultaneously: for any particular $v$ , one premise holds and the other implication is vacuous; no converse is literally stated. The coordinate type $\iota$ may be empty, and $C$ may be the zero code or the whole word space, although $C$ itself is never an empty set because every submodule contains the zero word. In the empty-coordinate case the word space and $C$ each have one element, every word lies in $C^\perp$ , the first equality reads $\psi(0)=1$ , and the second implication is vacuous.

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