Generalized Hamming bound: $k \le n - \log_q \sum_{i \le \lfloor (d-1)/2 \rfloor} \binom{n}{i}(q-1)^i$

Proved

EssentialCodingTheory.generalized_hamming_bound

by chaikon · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

coding-theorycombinatoricsinformation-theory

Let $\alpha$ be a finite alphabet with $q = |\alpha|$ symbols, let $n, d \ge 0$ , and let $C \subseteq \alpha^n$ be a code in which any two distinct codewords differ in at least $d$ coordinates. Then the dimension $k = \log_q |C|$ of $C$ satisfies

k \;\le\; n - \log_q \Bigl( \sum_{i=0}^{\lfloor (d-1)/2 \rfloor} \binom{n}{i} (q-1)^i \Bigr).

In particular this holds for every $(n, k, d)_q$ code, i.e. every code of minimum distance exactly $d$ . Logarithms are real; the statement imposes no hypothesis $q \ge 2$ or $C \ne \emptyset$ , and with the convention $\log_q x = 0$ for $q \le 1$ or $x = 0$ it remains true in those degenerate cases.

Preamble

import Mathlib.InformationTheory.Hamming
import Mathlib.Analysis.SpecialFunctions.Log.Base
open Finset

Formal statement

namespace EssentialCodingTheory
theorem generalized_hamming_bound {α : Type*} [Fintype α] [DecidableEq α] {n d : ℕ}
    (C : Finset (Fin n → α))
    (hC : ∀ c₁ ∈ C, ∀ c₂ ∈ C, c₁ ≠ c₂ → d ≤ hammingDist c₁ c₂) :
    Real.logb (Fintype.card α) C.card ≤
      n - Real.logb (Fintype.card α)
        ((∑ i ∈ range ((d - 1) / 2 + 1), n.choose i * (Fintype.card α - 1) ^ i : ℕ) : ℝ) := by
  sorry
end EssentialCodingTheory

Source

V. Guruswami, A. Rudra, M. Sudan, Essential Coding Theory (web draft), https://cse.buffalo.edu/faculty/atri/courses/coding-theory/book/web-coding-book.pdf, §1.7, p. 21, Theorem 1.7.2 (Hamming Bound for any d); definitions: code 1.2.1 (p. 5), dimension 1.2.3 (p. 6), Hamming distance 1.3.3 (p. 8), minimum distance 1.4.1 (p. 12), (n,k,d)_q code 1.7.1 (p. 20).

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

The statement concerns a finite alphabet $\alpha$ , with no further structure assumed beyond being finite and having decidable equality. Write $q = |\alpha|$ for its size. Note that $q$ may be $0$ or $1$ . The other inputs are:

natural numbers $n$ and $d$ , with no restrictions: $d = 0$ , $n = 0$ and $d > n$ are all allowed;
a finite set $C$ of words of length $n$ over $\alpha$ , that is, $C \subseteq \alpha^n$ .

The single hypothesis is that any two distinct words $c_1 \neq c_2$ in $C$ have Hamming distance $d_H(c_1, c_2) \ge d$ . Here $d_H(c_1, c_2)$ is the number of coordinates $1 \le j \le n$ where $c_1$ and $c_2$ differ. If $d \le 1$ this hypothesis holds for every $C$ . If $C$ has at most one element it holds for every $d$ .

Set $t = \lfloor (d \mathbin{\dot-} 1)/2 \rfloor$ , where $\dot-$ is truncated natural-number subtraction, so $t = 0$ when $d = 0$ or $d = 1$ . Define the natural number

V \;=\; \sum_{i=0}^{t} \binom{n}{i}\,(q \mathbin{\dot-} 1)^i .

In this sum, $q \mathbin{\dot-} 1 = 0$ when $q = 0$ , and $0^0 = 1$ . Terms with $i > n$ are $0$ because $\binom{n}{i} = 0$ for them. Since the $i = 0$ term is $1$ , $V \ge 1$ .

The theorem states the real-number inequality

\log_q |C| \;\le\; n - \log_q V, \qquad\text{where } \log_q x := \frac{\ln x}{\ln q}.

This logarithm follows total-function conventions:

$\ln 0 = 0$ , so if $C = \emptyset$ the left side is $0$ and the claim becomes $\log_q V \le n$ .
When $q \in \{0, 1\}$ , $\ln q = 0$ and division by zero gives $0$ . Every $\log_q$ term is then $0$ , and the claim reduces to $0 \le n$ .
When $q \ge 2$ and $C \neq \emptyset$ , the inequality is equivalent to $|C| \cdot V \le q^n$ .

Human review

Endorsed by marwahaha · Oct 14, 2026
Endorsed by chaikon · Oct 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Generalized Hamming bound: k≤n−log⁡q∑i≤⌊(d−1)/2⌋(ni)(q−1)ik \le n - \log_q \sum_{i \le \lfloor (d-1)/2 \rfloor} \binom{n}{i}(q-1)^ik≤n−logq​∑i≤⌊(d−1)/2⌋​(in​)(q−1)i

Generalized Hamming bound: $k \le n - \log_q \sum_{i \le \lfloor (d-1)/2 \rfloor} \binom{n}{i}(q-1)^i$