Information Theory

Motivation: how much randomness fits under prescribed edge probabilities?

Prescribing the probability $x_e$ that each edge belongs to a random perfect matching does not determine the distribution of the whole matching. The largest entropy compatible with those edge probabilities, $H(x)$, measures how many matching choices can coexist with them, and it links three topics: lower bounds on the number of perfect matchings, convex-optimization approaches to approximate counting, and the facial geometry of the perfect-matching polytope. For bipartite graphs, Schrijver's permanent inequality (Schrijver 1998) and Gurvits' weighted Bethe inequality (Gurvits 2011) give the clean comparison $H\ge F-B$ between $H$ and sums of one-coordinate entropies. For general graphs, odd cuts make such comparisons harder, and Anari, Oveis Gharan and Vinzant (2018) asked (FOCS version, Conjecture 6) whether the maximum binary-coordinate entropy over the polytope exceeds $\log N(G)$ by only a linear function of the number of vertices.

Timeline

• 1965 — Edmonds describes the perfect-matching polytope by degree equations, nonnegativity and odd-cut inequalities (Edmonds 1965).
• 1982 — Naddef (Math. Program. 1982) and Edmonds, Pulleyblank and Lovász (Combinatorica 1982) determine the dimension of the perfect-matching polytope.
• 1986 — Chung, Graham, Frankl and Shearer: Shearer's entropy inequality (JCTA 1986), which gives $H\le F$.
• 1998–2011 — Schrijver's lower bound for regular bipartite graphs and Gurvits' Bethe-approximation form give $H\ge F-B$ in the bipartite case.
• 2011 — Esperet, Kardoš, King, Král' and Norine: exponentially many perfect matchings in bridgeless cubic graphs (Adv. Math. 2011).
• 2018 — Anari, Oveis Gharan and Vinzant propose the entropy framework and the linear-error question (FOCS 2018).
• 2022 — Ebrahimnejad, Nagda and Oveis Gharan count perfect matchings in regular expanding nonbipartite graphs (ITCS 2022).
• 2026 — Abdi, Cornuéjols, Dadush and Dalirrooyfard bound the rank of tight odd cuts by $3m-1$ and give exponential lower counts for regular graphs of degree at least four with an odd-cut condition (Proc. LMS 2026). An OpenAI preprint, Entropy and Face Dimension of the Perfect-Matching Polytope (OpenAI Math Release, September 23, 2026), claims the pointwise bound $F-(2-2/m)B\le H\le F$ and a positive answer to the Anari–Oveis Gharan–Vinzant question. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

Let $G$ be a finite loopless multigraph with vertex set $V$, $|V|=2m\ge2$, and edge set $E$ (parallel edges are distinct coordinates). A perfect matching is a set of edges covering each vertex exactly once; $\mathcal M(G)$ is the set of them and $N(G)=|\mathcal M(G)|$. The perfect-matching polytope is

$$P(G)=\operatorname{conv}\{\mathbf 1_M: M\in\mathcal M(G)\}\subseteq\mathbb R^E .$$

For $x\in P(G)$ put, with natural logarithms and $0\log 0=0$,

$$H(x)=\max\Big\{-\sum_M p_M\log p_M:\ p\text{ a probability law on }\mathcal M(G),\ \sum_M p_M\mathbf 1_M=x\Big\},$$ $$F(x)=-\sum_{e}x_e\log x_e,\qquad B(x)=-\sum_e(1-x_e)\log(1-x_e).$$

Formalization targets

The milestones are listed in attack order: the face of a triangle expansion (Lemma 5.1), the coefficient-eight nonlinear bound (Theorem B.1), deterministic approximate counting (Theorem 1.2) and its singleton-loop variant (Proposition C.1).

Goal: Theorem 1.1 (pointwise entropy bounds)

If $G$ has at least one perfect matching, then for every $x\in P(G)$

$$F(x)-\Big(2-\frac 2m\Big)B(x)\;\le\;H(x)\;\le\;F(x).$$

The bound holds on the whole polytope, boundary included. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The upper bound is Shearer's inequality; the content is the lower comparison with coefficient $2-2/m$, valid in nonbipartite graphs where the bipartite coefficient $1$ fails (the source gives an eight-vertex counterexample, and Corollary 5.3 shows any universal coefficient is at least $\ln3/(2\ln(3/2))$). Optimizing over $x$ gives $\log N(G)\le\max_{P(G)}(F+B)\le\log N(G)+3m-2$, answering the Anari–Oveis Gharan–Vinzant question. Plugging in uniform marginals gives $N(G)\ge e^{-2(m-1)}k^m$ for graphs with $k$ edge-disjoint perfect matchings, and for $k$-regular graphs whose odd cuts all have at least $k$ edges. The same entropy framework yields a deterministic polynomial-time algorithm approximating $N(G)$ within a factor $512^n$ for graphs with binary edge multiplicities (Theorem 1.2).

Formalizing it. The goal is a finite-dimensional inequality about polytopes and entropies, accessible to Mathlib's convexity and analysis libraries. The milestones extend the mission to a certified polynomial-time counting algorithm in Mathlib's Turing-machine model, a rare example of a formally specified approximation algorithm for a #P-hard quantity.

Difficulty

Shearer's inequality gives the upper bound in one line, and in bipartite graphs the lower bound follows from permanent inequalities that have no analogue for general graphs. A direct convexity argument fails because $H$ is not differentiable across faces of $P(G)$: at a boundary mean the maximum-entropy law lives on a lower-dimensional face, and its covariance is singular in the ambient edge space. The lower bound must therefore be proved face by face, and it needs the sharp geometric estimate $|\operatorname{supp}x|-\dim F_x\le 3m-2$ for the minimal face $F_x$ containing $x$; the earlier rank bound $3m-1$ would not give the coefficient $2-2/m$.

Formalization scope

• Graphs are LooplessGraph V E: endpoint maps left right : E → V with left e ≠ right e, on finite types with decidable equality, so parallel edges are distinct elements of E. A perfect matching is a Finset E with exactly one edge at each vertex.
• polytope G is the convex hull of matching indicator vectors in E → ℝ; maxMatchingEntropy G x is sSup of the entropies of probability vectors on matchings with mean x. On the polytope this set is nonempty, compact and bounded, so the sSup is the attained maximum; off the polytope it would be junk, which is why the hypothesis x ∈ G.polytope is required.
• entropy uses Real.negMulLog, so $0\log0=0$; complementEntropy x is $B(x)$.
• Hypotheses: 0 < m, Fintype.card V = 2 * m, and a perfect matching exists. The coefficient is the real number 2 - 2 / m.
• The counting milestones use Turing.TM2ComputableInPolyTime with finite alphabets, binary encodings of the vertex count and of positive multiplicity records, and require polynomially bounded output length.
• Infrastructure needed: Edmonds' polytope description, faces and minimal faces of polytopes, exponential families and covariance, and polynomial-time computability of rational arithmetic in TM2. The polytope and entropy definitions are reusable for other counting missions.

Selected references

• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards B 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
• L. G. Valiant, The complexity of computing the permanent, Theoret. Comput. Sci. 8 (1979), 189–201. https://doi.org/10.1016/0304-3975(79)90044-6
• D. Naddef, Rank of maximum matchings in a graph, Math. Program. 22 (1982), 52–70. https://doi.org/10.1007/BF01581025
• J. Edmonds, W. R. Pulleyblank, L. Lovász, Brick decompositions and the matching rank of graphs, Combinatorica 2 (1982), 247–274. https://doi.org/10.1007/BF02579233
• F. R. K. Chung, R. L. Graham, P. Frankl, J. B. Shearer, Some intersection theorems for ordered sets and graphs, J. Combin. Theory Ser. A 43 (1986), 23–37. https://doi.org/10.1016/0097-3165(86)90019-1
• A. Schrijver, Counting 1-factors in regular bipartite graphs, J. Combin. Theory Ser. B 72 (1998), 122–135. https://doi.org/10.1006/jctb.1997.1798
• N. Linial, A. Samorodnitsky, A. Wigderson, A deterministic strongly polynomial algorithm for matrix scaling and approximate permanents, Combinatorica 20 (2000), 545–568. https://doi.org/10.1007/s004930070007
• M. Jerrum, A. Sinclair, E. Vigoda, A polynomial-time approximation algorithm for the permanent of a matrix with nonnegative entries, J. ACM 51 (2004), 671–697. https://doi.org/10.1145/1008731.1008738
• L. Esperet, F. Kardoš, A. D. King, D. Král', S. Norine, Exponentially many perfect matchings in cubic graphs, Adv. Math. 227 (2011), 1646–1664. https://doi.org/10.1016/j.aim.2011.03.015
• L. Gurvits, Unleashing the power of Schrijver's permanental inequality with the help of the Bethe approximation (2011). https://arxiv.org/abs/1106.2844v11
• M. Cygan, M. Pilipczuk, R. Škrekovski, A bound on the number of perfect matchings in Klee-graphs, Discrete Math. Theor. Comput. Sci. 15 (2013), 37–52. https://doi.org/10.46298/dmtcs.633
• A. Barvinok, Approximating permanents and hafnians, Discrete Analysis (2017). https://doi.org/10.19086/da.1244
• N. Anari, S. Oveis Gharan, C. Vinzant, Log-concave polynomials, entropy, and a deterministic approximation algorithm for counting bases of matroids, FOCS 2018, 35–46. https://doi.org/10.1109/FOCS.2018.00013
• F. Ebrahimnejad, A. Nagda, S. Oveis Gharan, Counting and sampling perfect matchings in regular expanding non-bipartite graphs, ITCS 2022, 61:1–61:12. https://doi.org/10.4230/LIPIcs.ITCS.2022.61
• A. Abdi, G. Cornuéjols, D. Dadush, M. Dalirrooyfard, Lower bounds for cube-ideal set-systems, Proc. London Math. Soc. 133 (2026), e70199. https://doi.org/10.1112/plms.70199
• OpenAI, Entropy and Face Dimension of the Perfect-Matching Polytope, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Entropy-and-Face-Dimension-of-the-Perfect-Matching-Polytope-September-23-2026/main.pdf

Motivation

A binary error-correcting code is a set of $n$-bit words chosen so that the words stay distinguishable after a few bits have been corrupted in transmission. A code can correct any $r$ errors exactly when every two of its words differ in at least $2r+1$ positions. The more words the code has, the more information each transmitted block carries. So the central quantitative question of coding theory is how large a code of given length and minimum distance can be. Codes are used in every technology that transmits or stores data, from disks and phones to deep-space probes.

In 1973 Philippe Delsarte showed that an upper bound on this maximum size is the optimum value of an explicit linear program (Delsarte, An algebraic approach to the association schemes of coding theory, Philips Res. Repts. Suppl. 10, 1973). The bound was far stronger than the classical volume argument and remains a standard tool. This mission formalizes the self-contained proof of the bound in §8.4 of Matoušek and Gärtner's textbook (Springer 2007). That proof follows Best, Brouwer, MacWilliams, Odlyzko and Sloane (IEEE Trans. Inform. Theory 24, 1978). The mission also covers the step of Delsarte's original argument that the book isolates as a lemma.

Timeline.

• 1950: Hamming introduces single-error-correcting codes and the sphere-packing bound.
• 1973: Delsarte proves the linear programming bound using association schemes.
• 1978: Best et al. give the elementary parity proof and small improvements, among them $A(17,3) \le 6552$.
• 2005: Schrijver replaces the linear program by a semidefinite program and improves many entries of the code tables (IEEE Trans. Inform. Theory 51).

Setting

A word is $\mathbf w = (w_1,\dots,w_n) \in \{0,1\}^n$, and a code is any set $C \subseteq \{0,1\}^n$. The Hamming distance $d_H(\mathbf w,\mathbf w')$ is the number of positions $j$ with $w_j \ne w'_j$. The weight $|\mathbf w|$ is the number of ones in $\mathbf w$. The word $\mathbf w \oplus \mathbf w'$ is the entrywise sum modulo 2. For $I \subseteq \{1,\dots,n\}$, the restricted distance $d^I_H(\mathbf w,\mathbf w')$ counts only the differing positions that lie in $I$.

A code has distance $d$ if $d_H(\mathbf w,\mathbf w') \ge d$ for all distinct $\mathbf w,\mathbf w' \in C$ (Definition 8.4.1). The quantity $A(n,d)$ is the maximum of $|C|$ over all codes $C \subseteq \{0,1\}^n$ with distance $d$.

For $0 \le i,t \le n$ the Krawtchouk numbers are

$$K_t(n,i) = \sum_{j=0}^{\min(i,t)} (-1)^j \binom ij \binom{n-i}{t-j}.$$

The distance distribution of a code $C$ is

$$\tilde x_i(C) = \frac{1}{|C|}\,\bigl|\{(\mathbf w,\mathbf w')\in C^2 : d_H(\mathbf w,\mathbf w') = i\}\bigr|, \qquad i=0,\dots,n.$$

The Delsarte linear program has variables $x_0,\dots,x_n$. It maximizes $x_0+\dots+x_n$ subject to:

• $x_0 = 1$;
• $x_i = 0$ for $1 \le i \le d-1$;
• $\sum_{i=0}^n K_t(n,i)\,x_i \ge 0$ for $1 \le t \le n$;
• $x \ge 0$.

For Delsarte's original argument, $M_i$ is the $2^n\times 2^n$ matrix whose $(\mathbf v,\mathbf w)$ entry is $1$ when $d_H(\mathbf v,\mathbf w) = i$ and $0$ otherwise. The weights are $\tilde y_i = |\{(\mathbf w,\mathbf w')\in C^2 : d_H = i\}| / (2^n\binom ni)$.

Formalization targets

Goal: Theorem 8.4.3 (the Delsarte bound)

$$A(n,d) \;\le\; \max\Bigl\{\textstyle\sum_{i=0}^n x_i \;:\; x \text{ feasible for the Delsarte program}\Bigr\}\quad\text{for all } n, d.$$

The goal is stated against every upper bound $v$ of the objective on the feasible set. No particular optimum value is fixed, so the statement covers every $n$ and $d$ at once.

Milestones, in attack order

1. Lemma 8.4.5. For every $I$ and $C$, the pairs in $C^2$ with even $d^I_H$ are at least as many as the pairs with odd $d^I_H$.
2. Corollary 8.4.6. $\sum_{(\mathbf w,\mathbf w')\in C^2}(-1)^{(\mathbf w\oplus\mathbf w')^T\mathbf v}\ge 0$ for every $\mathbf v$.
3. Proposition 8.4.4. $\sum_{i=0}^n K_t(n,i)\,\tilde x_i(C) \ge 0$ for every $C$ and every $t = 1,\dots,n$.
4. §8.4, p. 160. The values $\tilde x_i(C)$ sum to $|C|$. For a nonempty code with distance $d$, the vector $\tilde x(C)$ is feasible for the program.
5. Lemma 8.4.2 (sphere-packing bound). $A(n,2r+1) \le \lfloor 2^n / \sum_{i=0}^r\binom ni\rfloor$.
6. Lemma 8.4.7. $\tilde M = \sum_{i=0}^n \tilde y_i M_i$ is positive semidefinite.

Significance

The Delsarte bound turns an extremal problem over the $2^{2^n}$ subsets of the cube into a linear program with $n+1$ variables. For $A(17,3)$ it gives $6553$, while the sphere-packing bound gives $7281$. Many entries of the standard code tables rest on this bound or its refinements. The positive semidefiniteness in Lemma 8.4.7 is the starting point of the semidefinite programming bounds of Schrijver and of later work. The same framework also underlies the linear programming bounds for spherical codes and sphere packings.

The theorem is classical and fully proved in the literature. Neither Mathlib nor this platform has a formal statement or proof of it. Mathlib has Hamming distance and binomial coefficients, but it has no $A(n,d)$, no Krawtchouk numbers and no LP bound for codes. This mission would produce the first formal statement and proof. It would also produce reusable identities on Krawtchouk sums and character sums over $\{0,1\}^n$.

Difficulty

Two of the program's constraints are immediate once $\tilde x_i$ is defined: $\tilde x_0 = 1$, and $\tilde x_i = 0$ for $i < d$. The difficulty lies in the Krawtchouk constraints. They do not follow from counting pairs at a single distance. They require a sign-weighted count over all words of weight $t$, and the sum must then be regrouped by the distance of each pair. That regrouping identifies a count of words, split by how many ones they share with a fixed word, with the Krawtchouk number. Formally this is an exchange of finite sums together with a binomial counting identity, and the index bookkeeping, including the range $j \le \min(i,t)$, has to be exact.

The obvious attempt proves the inequality one distance class at a time. It fails because the individual terms $K_t(n,i)\,\tilde x_i$ have no sign. Only the whole sum is nonnegative.

Formalization scope

• Words and codes. Words are Fin n → Bool, with bit $1$ as true. The book's positions $1,\dots,n$ become 0, …, n-1. Codes are Finsets of words, and $d_H$ is Mathlib's hammingDist.
• The maximum $A(n,d)$. $A(n,d)$ is a Finset.sup over the finite family of codes with distance $d$. This family contains the empty code, so the maximum is attained.
• Krawtchouk numbers. $K_t(n,i)$ is an integer, and its natural-number subtractions are honest for $i \le n$ and $j \le t$.
• LP variables and the $x_i = 0$ constraints. The LP variables are indexed by Fin (n+1) with no index shift. The constraints $x_i = 0$ are imposed for $1 \le i < d$, so they are vacuous for $d \le 1$.
• The empty code. Lean's convention $1/0 = 0$ gives $\tilde x(\emptyset) = 0$. Proposition 8.4.4 then holds trivially, and the feasibility milestone carries the hypothesis $C \ne \emptyset$ that the book's division presupposes.
• The sphere-packing floor. The floor in the sphere-packing bound is natural-number division by a denominator that is at least $1$.
• Positive semidefiniteness. This is Mathlib's Matrix.PosSemidef over $\mathbb R$.

No trivialization. The goal is not stated as "$A(n,d) \le \sup$" with a real supremum, which Lean would evaluate to $0$ on an empty or unbounded set. Its hypothesis ranges over upper bounds of a feasible program: $(1,0,\dots,0)$ is always feasible, so the hypothesis is never vacuous.

Contributions welcome. Useful lemmas include:

• Krawtchouk identities, for example $\sum_{t}K_t(n,i) = 2^n[i=0]$ and $K_i(n,t)\binom ni = K_t(n,i)\binom nt$;
• counting words of weight $t$ that meet a fixed support in exactly $j$ positions;
• general facts on character sums $\sum_{\mathbf w\in C}(-1)^{\mathbf w^T\mathbf v}$.

These are reusable for other LP and SDP bounds in coding theory.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.4. https://doi.org/10.1007/978-3-540-30717-4
• P. Delsarte, An algebraic approach to the association schemes of coding theory, Philips Research Reports Supplements 10, 1973.
• M. R. Best, A. E. Brouwer, F. J. MacWilliams, A. M. Odlyzko, N. J. A. Sloane, Bounds for binary codes of length less than 25, IEEE Trans. Inform. Theory 24 (1978), 81–93. https://doi.org/10.1109/TIT.1978.1055827
• A. Schrijver, New code upper bounds from the Terwilliger algebra and semidefinite programming, IEEE Trans. Inform. Theory 51 (2005), 2859–2866. https://doi.org/10.1109/TIT.2005.851748

Motivation

Consider the classical error-correcting problem. An input vector $f \in \mathbb{R}^n$ (the plaintext) is encoded as $Af \in \mathbb{R}^m$ by a coding matrix $A$ with $m > n$, and an unknown, arbitrary vector of errors $e$ corrupts the result, so that only $y = Af + e$ is observed. Can $f$ be recovered exactly, and by an algorithm whose running time is polynomial in $m$? Candès and Tao (2005) answer both questions at once: if a matrix $F$ annihilating $A$ satisfies a restricted orthonormality condition, then $f$ is the unique solution of the convex program $\min_g \|y - Ag\|_{\ell^1}$, which is a linear program, whenever at most $S$ entries of $y$ are corrupted, whatever their positions and values. Read for the matrix $F$ alone, the same theorem says that $\ell^1$ minimization (basis pursuit) returns the sparsest solution of an underdetermined linear system. That statement is the mathematical core of compressed sensing, and the restricted isometry constants introduced in this paper became the standard tool of the field.

Timeline. Donoho and Huo (2001), followed by Elad–Bruckstein, Donoho–Elad and Gribonval–Nielsen, proved the equivalence of $\ell^0$ and $\ell^1$ minimization for matrices formed by concatenating two orthonormal bases, for sparsity of order $\sqrt{m}$, through incoherence. Candès, Romberg and Tao (2004) and Candès and Tao (2004) obtained recovery with overwhelming probability for random matrices at sparsity of order $m/\log m$. Donoho (2004) showed for Gaussian matrices that a constant, unspecified fraction $\rho m$ of nonzero entries can be tolerated. The present paper (December 2004, published 2005) gives a deterministic sufficient condition, $\delta_S + \theta_{S,S} + \theta_{S,2S} < 1$, valid for every matrix, and specializes it to Gaussian matrices with explicit numerical values of the tolerable fraction. Later work, for instance Candès (2008) with the condition $\delta_{2S} < \sqrt{2} - 1$, sharpened the sufficient condition; those later results are not part of this mission.

Setting

Let $F$ be a real $p \times m$ matrix with columns $v_1, \dots, v_m \in \mathbb{R}^p$, and let $H$ be the linear span of these columns. For an index set $T \subseteq \{1,\dots,m\}$ and real coefficients $c = (c_j)_{j \in T}$, write $F_T c = \sum_{j \in T} c_j v_j$. A vector $c \in \mathbb{R}^m$ is supported on $T$ when $c_j = 0$ for all $j \notin T$; with this convention $F_T c$ is just the product $Fc$. Norms are the Euclidean norm $\|c\| = (\sum_j c_j^2)^{1/2}$ and the $\ell^1$ norm $\|c\|_{\ell^1} = \sum_j |c_j|$.

Definition 1.1. For an integer $S$, the $S$-restricted isometry constant $\delta_S$ is the smallest quantity such that

$$(1 - \delta_S)\|c\|^2 \le \|F_T c\|^2 \le (1 + \delta_S)\|c\|^2$$

for all $T$ of cardinality at most $S$ and all real coefficients $(c_j)_{j \in T}$. The $S, S'$-restricted orthogonality constant $\theta_{S,S'}$ is the smallest quantity such that

$$|\langle F_T c, F_{T'} c' \rangle| \le \theta_{S,S'} \, \|c\| \, \|c'\|$$

for all disjoint $T, T'$ with $|T| \le S$ and $|T'| \le S'$. The paper writes $\theta_S$ for $\theta_{S,S}$. These numbers measure how far the columns of $F$ are from an orthonormal system when only linear combinations of at most $S$ columns are considered.

The two optimization problems are

$$(P_1)\quad \min_{d \in \mathbb{R}^m} \|d\|_{\ell^1} \ \text{ subject to } \ Fd = f, \qquad\qquad (P_1')\quad \min_{g \in \mathbb{R}^n} \|y - Ag\|_{\ell^1}.$$

A vector is the unique minimizer of one of these problems when it is feasible and every other feasible vector has a strictly larger objective value.

Formalization targets

Goal: Theorem 1.5 (decoding by linear programming)

Let $A$ be a real $m \times n$ matrix of full rank with $m > n$, and $F$ a real $p \times m$ matrix with $FA = 0$. Let $S \ge 1$ satisfy

$$\delta_S(F) + \theta_{S,S}(F) + \theta_{S,2S}(F) < 1 . \tag{1.10}$$

If $y = Af + e$ where $e$ is supported on a set of size at most $S$, then $f$ is the unique minimizer of $(P_1')$.

Core: Theorem 1.4 (exact recovery by $\ell^1$ minimization)

Let $S \ge 1$ satisfy (1.10) for $F$, and let $c$ be supported on a set $T$ with $|T| \le S$. Then $c$ is the unique minimizer of $(P_1)$ with $f := Fc$.

Theorem 1.5 is the companion of Theorem 1.4 for the decoding problem, and the mission's milestones are the four lemmas the paper proves on the way: Lemma 1.2 (the $\delta$ numbers control the $\theta$ numbers), Lemma 1.3 (uniqueness of sparse representations under $\delta_{2S} < 1$), and the two dual sparse reconstruction properties, Lemma 2.1 ($\ell^2$ version) and Lemma 2.2 ($\ell^\infty$ version).

Significance

The result. The guarantee is deterministic and uniform: one condition on $F$, checkable in principle from the matrix alone, ensures that a single linear program recovers every sufficiently sparse vector, with no probability of failure. In the decoding reading, a fixed fraction of the ciphertext can be corrupted arbitrarily and the plaintext is still recovered exactly by convex optimization. The paper shows in its Section 3 that Gaussian matrices satisfy (1.10) with overwhelming probability at explicit values of $S/m$, and in Section 5 that the same hypothesis yields near-optimal recovery of compressible signals from few measurements; both are consequences of the deterministic core formalized here.

Formalizing it. The theorems are proved in the paper, and no machine-checked proof of them exists. Prove2Me holds a formalization of a different restricted-isometry sufficient condition taken from a textbook (HighDimProb.SparseRecovery.rip_implies_exact_recovery); it uses a different definition of the isometry constant and a different hypothesis, so nothing there can be reused as is. This mission produces the definitions of $\delta_S$ and $\theta_{S,S'}$ exactly as in Definition 1.1, the dual-certificate lemmas, and the two theorems, in a form that later missions on compressed sensing can import. The probabilistic Theorem 1.6, Lemma 3.1 and Corollary 1.7, and the compressible-signal Theorem 5.1, are not targets: see the scope section for why.

Difficulty

The whole proof rests on a dual certificate: a vector $w \in H$ with $\langle w, v_j \rangle = \operatorname{sgn}(c_j)$ for $j \in T$ and $|\langle w, v_j \rangle| < 1$ for $j \notin T$. Given such a $w$, the argument of Section 2.2 is a short chain of inequalities. The first idea every newcomer has is $w = F_T (F_T^* F_T)^{-1} \operatorname{sgn}(c)$; this interpolates the signs on $T$ and, by restricted orthogonality, its inner products off $T$ are small in an $\ell^2$ sense, but not in the $\ell^\infty$ sense required. That is exactly Lemma 2.1: the $\ell^\infty$ bound holds only outside an exceptional set of at most $S'$ indices. Lemma 2.2 removes the exceptional set by an infinite alternating iteration, prescribing values on the previous exceptional set while keeping the values on $T$ fixed, and summing a geometrically convergent series.

Two points deserve attention from solvers. First, the paper's proof of Lemma 2.2 prescribes values on sets of size up to $2S$ ($T_0 \cup T_n$) at each step, while the per-step factors it quotes, $\theta_{S,2S}/(1-\delta_S)$, are what Lemma 2.1 gives for a set of size $S$; a proof of the printed constant in (2.4) has to account for this, and the hypothesis of Theorem 1.4 leaves room for a proof with slightly worse per-step factors. Second, Lemma 2.1 is printed with $\theta_S$ in its $\ell^2$ bound on the exceptional set, while the inequality (2.3) its proof establishes gives $\theta_{S,S'}$; the mission states the lemma with $\theta_{S,S'}$, which coincides with the printed form in the case $S' = S$ used by Lemma 2.2.

Formalization scope

Matrices are Matrix (Fin p) (Fin m) ℝ; a coefficient vector on $T$ is a vector in Fin m → ℝ supported on the finite set $T$, and $F_T c$ is F.mulVec c. The Euclidean and $\ell^1$ norms and the inner product are explicit finite sums, so every statement can be checked by hand against the paper. $H$ is the span of the columns.

The constants $\delta_S$ and $\theta_{S,S'}$ are the infimum of the set of nonnegative $\delta$ (resp. $\theta$) satisfying the defining inequalities for all admissible sets and coefficients. This set is nonempty, closed and bounded below, so the infimum is attained and is the paper's smallest quantity; on the paper's domain the smallest such quantity is nonnegative, so the extra clause only fixes a harmless value in degenerate cases such as $S = 0$. The definitions are total in $S, S'$, and each theorem carries the paper's domain conditions ($S \ge 1$, and $2S \le m$, $3S \le m$ or $S + S' \le m$ as needed) as explicit hypotheses. The hypotheses are satisfiable, since a matrix with orthonormal columns has $\delta_S = \theta_{S,S'} = 0$, so none of the statements is vacuous.

"Unique minimizer" is a strict inequality against every competitor. "Full rank" for the $m \times n$ matrix $A$ with $m > n$ is injectivity of $g \mapsto Ag$; both are standing assumptions of the paper's Section 1.1 and appear as hypotheses of Theorem 1.5. In Lemma 2.1, "a constant $K > 0$ depending only on $\delta_S$" is a positive function of the real number $\delta_S$, quantified before all other data.

Out of scope, with the reason for each: Theorem 1.6 refers to a threshold $r^*(p,m)$ "given in Section 3.5", which the paper does not contain, and to "overwhelming probability" with unspecified constants; Lemma 3.1 is proved only for $m$ and $p$ "large enough", with an unspecified threshold and an $o(1)$ term quoted from the literature; Corollary 1.7 rests on Theorem 1.6; Theorem 5.1 has an unspecified constant $C$ and is explicitly not proved in the paper. A future mission can add these once precise statements are fixed.

Contributions that are welcome: proofs of the four milestone lemmas and of the two theorems; reusable lemmas on the attainment and monotonicity of the constants, on the Gram matrix $F_T^* F_T$ and its inverse under $\delta_S < 1$, and on the duality inequality of Section 2.2. Statements that weaken the hypotheses (for instance to $\delta_{2S} < \sqrt{2} - 1$) belong to a separate mission.

Selected references

• E. J. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51 (12), 2005, 4203–4215. https://doi.org/10.1109/TIT.2005.858979 (arXiv: https://arxiv.org/abs/math/0502327)
• E. J. Candès, J. Romberg and T. Tao, Robust uncertainty principles: exact signal reconstruction from highly incomplete frequency information, IEEE Trans. Inform. Theory 52 (2), 2006. https://arxiv.org/abs/math/0409186
• E. J. Candès and T. Tao, Near optimal signal recovery from random projections: universal encoding strategies?, IEEE Trans. Inform. Theory 52 (12), 2006. https://arxiv.org/abs/math/0410542
• D. L. Donoho and X. Huo, Uncertainty principles and ideal atomic decomposition, IEEE Trans. Inform. Theory 47, 2001, 2845–2862. https://doi.org/10.1109/18.959265
• S. S. Chen, D. L. Donoho and M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20, 1999, 33–61. https://doi.org/10.1137/S1064827596304010
• E. J. Candès, The restricted isometry property and its implications for compressed sensing, C. R. Acad. Sci. Paris, Ser. I 346, 2008, 589–592. https://doi.org/10.1016/j.crma.2008.03.014

One bit of a noisy string

Send a uniformly random string $X \in \{0,1\}^n$ through a memoryless binary symmetric channel with crossover probability $p$: each coordinate is flipped independently with probability $p$, producing $Y \in \{0,1\}^n$. An observer sees $Y$ and wants to learn about $X$ — but the summary of $X$ they are allowed to keep is a single bit $f(X)$, computed by a Boolean function $f$ chosen in advance. Which choice of $f$ makes that one bit most informative about the noisy observation, in Shannon's sense?

The natural candidate is a dictator, $f(x) = x_i$: keep one coordinate and forget the rest. It achieves $I(f(X); Y) = I(X_i; Y_i) = 1 - H(p)$, where $H$ is the binary entropy function in bits. Majority, parity, and every other symmetric or balanced construction does worse. Courtade and Kumar conjectured in 2014 that nothing does better: no Boolean function of $n$ noisy-channel inputs, however many coordinates it reads and however it combines them, beats a single coordinate.

Setting

Fix $n \in \mathbb{N}$, a crossover probability $p \in [0,1]$, and a Boolean function $f : \{0,1\}^n \to \{0,1\}$. With $X$ uniform on the cube and $Y$ its image under the channel, all the relevant quantities are finite sums: the joint mass of $(f(X), Y)$ is

$$\Pr[f(X) = b,\, Y = y] \;=\; 2^{-n}\sum_{x \in \{0,1\}^n} \mathbf{1}[f(x) = b] \prod_{i=1}^{n} \bigl( (1-p)^{\mathbf{1}[x_i = y_i]} p^{\mathbf{1}[x_i \neq y_i]} \bigr),$$

and mutual information is $I(f(X); Y) = H(f(X)) + H(Y) - H(f(X), Y)$, all entropies in bits. No measure theory is required, and the endpoints $p \in \{0, 1/2, 1\}$ are included by the conventions $0 \log 0 = 0$ and $\log 0 = 0$.

Formalization targets

Goal — the general inequality

$$\forall\, n \in \mathbb{N},\ \forall f : \{0,1\}^n \to \{0,1\},\ \forall p \in [0,1]: \qquad I\bigl(f(X); Y\bigr) \;\le\; 1 - H(p).$$

The goal quantifies over every dimension, including $n = 0$, every Boolean function — balanced or not, monotone or not — and every crossover probability including the three endpoints. Nothing is assumed about $f$: no balance condition, no bound on the number of influential coordinates, no restriction to a range of $p$. The bound is tight, attained by any dictator, so the statement is exactly the assertion that dictators are the most informative Boolean functions.

Why the bound matters

The inequality is the sharp, one-bit case of a general question in information theory: how much can a lossy summary of a source tell you about a noisy observation of that source? It is the Boolean-function analogue of a hypercontractivity or "small-set expansion" statement — quantities of the form $I(f(X); Y)$ under a noise operator are precisely what appear in the analysis of Boolean functions, in hardness-of-approximation reductions built on noise stability, and in distributed source-coding and common-information problems, where the bound limits what a single bit of a compressed description can carry. Special cases were known and repeatedly used: balanced functions, functions of few coordinates, and asymptotic or high-noise regimes. The general statement resisted those methods, because the extremal structure is a single coordinate while the space of competitors grows doubly exponentially in $n$.

Why it is hard

Mutual information is neither convex nor concave in $f$, and the obvious relaxations are false: the corresponding bound for real-valued or non-Boolean summaries fails, so any argument must use Booleanness. Fourier-analytic approaches control noise stability but lose the constant needed for tightness, and the tightness is the whole content — the inequality is an equality for dictators, leaving no slack to absorb approximation. Induction on $n$ requires a statement strong enough to survive restriction, and the known strengthenings become false at the endpoints. The regimes also split: near $p = 1/2$ the problem becomes a perturbative curvature computation around the dictator, while for moderate $p$ the extremal analysis is a global optimization over a two-parameter family, and the two arguments meet only if their boundaries are matched exactly.

Formalization scope

The goal is stated with the entropy and mutual-information definitions of this mission's definition module: binary entropy via Mathlib's Real.binEntropy divided by $\log 2$ (so entropies are in bits), the channel as an explicit product kernel, and the joint and marginal masses as explicit finite sums over the cube. The proposition is a single closed statement — no hypotheses beyond $0 \le p \le 1$ — so a solution must establish it for all dimensions uniformly.

A complete machine-checked proof of this statement exists in Lean 4 (Chen–Gohari–Javanmard–Lin–Mirrokni–Nair–Woodruff, 2026): axioms $\{$propext, Classical.choice, Quot.sound$\}$, no sorry and no native_decide, but 45,500 modules and roughly 50 million lines, most of it kernel-checked numerical certificate data. It is therefore not submittable as a single solution, and the mission's supporting structure — the manuscript route's regional statements and its leaf certificate families — will be added as separate theorems as they are transplanted onto the platform.

Selected references

• T. A. Courtade, G. R. Kumar. Which Boolean functions maximize mutual information on noisy inputs? IEEE Transactions on Information Theory 60(8):4515–4525, 2014. (The conjecture.)
• Z. Chen, A. Gohari, A. Javanmard, H. Lin, V. Mirrokni, C. Nair, D. P. Woodruff. A Proof of the Most Informative Boolean Function Conjecture. arXiv:2609.24931, 2026.
• Lean 4 formalization of the above: https://github.com/dpwoodru/general-courtade-kumar-lean
• R. O'Donnell. Analysis of Boolean Functions. Cambridge University Press, 2014, Chapters 2 and 9 (noise operators, hypercontractivity).

Motivation

Cryptography before 1949 was a catalogue of ciphers and of the tricks that broke them. C. E. Shannon's Communication Theory of Secrecy Systems (Bell System Technical Journal 28(4):656–715, 1949) replaced the catalogue with a probabilistic model: a cipher is a family of invertible maps from messages to cryptograms, indexed by a key drawn from a known distribution, and the cryptanalyst's state of knowledge after an interception is the a posteriori distribution over messages. Part II of that paper asks when interception conveys nothing at all. The answer — perfect secrecy — is the origin of the one-time pad's security proof and of the modern habit of defining security as the indistinguishability of a posteriori from a priori beliefs.

This mission formalizes §10, Perfect Secrecy: the definition, the necessary and sufficient condition (Shannon's Theorem 6), the counting bound that the key set be at least as large as the message set, the cyclic system that attains the bound, the Latin-square description of the systems that attain it, and the entropy form of the constraint.

Setting

A finite secrecy system consists of three finite sets — the messages $M$, the keys $K$, the cryptograms $E$ — together with an enciphering map $T_k : M \to E$ for each key $k$. Each $T_k$ is non-singular, i.e. injective, so a receiver who knows the key deciphers unambiguously. The key is drawn from an a priori distribution $P(k) \ge 0$, $\sum_k P(k) = 1$, and the message from an a priori distribution $P(M) \ge 0$, $\sum_M P(M) = 1$, independently of the key.

Three derived quantities carry the theory. The key weight

$$P_M(E) \;=\; \sum_{k \,:\, T_k M = E} P(k)$$

is the probability that the cryptogram is $E$ given that the message is $M$. The cryptogram probability is $P(E) = \sum_M P(M) P_M(E)$, the probability of obtaining $E$ from any cause. The a posteriori probability of the message after interception is $P_E(M) = P(M) P_M(E) / P(E)$, defined for cryptograms with $P(E) \neq 0$.

A system has perfect secrecy when, for every a priori message distribution and every cryptogram that can occur, $P_E(M) = P(M)$ for all $M$: interception leaves the cryptanalyst's probabilities unchanged. Quantifying over all a priori message distributions is Shannon's requirement that the equality hold "independently of the values of $P(M)$".

Finally, $H(M) = -\sum_M P(M)\log P(M)$ and $H(K) = -\sum_K P(K)\log P(K)$ are the entropies of the message and key choices.

Formalization targets

Goal — Theorem 6

$$\text{perfect secrecy} \iff P_M(E) = P(E) \quad \text{for all } M, E .$$

Equivalently, $P_M(E)$ does not depend on $M$: the total probability of the keys carrying $M_i$ to a given $E$ is the same as that of the keys carrying $M_j$ to the same $E$. The goal fixes nothing about the sizes of the three sets, and no structure on the key distribution beyond normalization.

Milestone — the Bayes relation (p. 680)

$$P(E) = \sum_M P(M)P_M(E), \qquad P_E(M) = \frac{P(M)P_M(E)}{P(E)} .$$

Milestone — the key-counting bound (p. 681)

$$\text{perfect secrecy} \implies \#M \le \#K .$$

Milestone — attainability, the cyclic system of Fig. 5 (p. 681)

$$T_i M_j = E_s, \quad s = i + j \bmod n, \quad P(k) = \tfrac1n \;\Longrightarrow\; \text{perfect secrecy}.$$

Milestone — Latin-square characterization (p. 681)

$$\text{perfect secrecy} \ \wedge\ \#M = \#K = \#E \implies \big(\forall M, E\ \exists! k,\ T_k M = E\big) \ \wedge\ P \text{ is uniform}.$$

Milestone — the entropy constraint (p. 682)

$$\text{perfect secrecy} \implies H(M) \le H(K) .$$

Significance

Theorem 6 is the structural fact behind every later statement in the section: the counting bound, the Latin-square description, and the entropy constraint are all read off from the independence of $P_M(E)$ from $M$. The counting bound and the entropy constraint are the precise sense in which unconditional secrecy is expensive — the key must be at least as uncertain as the message — and they are the reason practical cryptography moved to computational assumptions. The cyclic system supplies the matching construction, so the bound is sharp.

These results are classical and have textbook proofs; what this mission produces is a machine-checked development of them from a single explicit model of a finite secrecy system, including the model itself. Mathlib has extensive measure-theoretic probability and some information theory, but no formalization of Shannon's secrecy systems, of perfect secrecy, or of the results of §10. The shared definition layer — ciphers with injective enciphering maps, key weights, a posteriori probabilities, the perfect-secrecy predicate, finite entropy — is reusable for the rest of the paper: the equivocation results of §11–§13, unicity distance, and the ideal-system theorems of §16 all rest on the same objects.

Difficulty

The two directions of Theorem 6 are not symmetric. Sufficiency is a computation. Necessity has to extract, from a statement about a posteriori probabilities that only constrains cryptograms of positive probability and only for one distribution at a time, a statement about key weights alone; the useful instantiation is a distribution giving every message positive mass, and the cryptograms of probability zero must be handled separately rather than ignored.

The counting and Latin-square milestones are finite combinatorics, but the obvious argument — "for each message and cryptogram pick the key joining them" — needs the keys picked to have positive probability, and the model permits keys of probability zero; this is exactly where an argument that looks complete on paper leaves a gap in Lean. The entropy milestone is the hardest of the five: $H(M) \le H(K)$ passes through the conditional entropies $H(M \mid E) \le H(K \mid E)$, and Mathlib's information-theoretic API is stated for measures rather than for finite weighted sums, so either a bridge or a self-contained development of finite conditional entropy is required.

Formalization scope

Messages, keys and cryptograms are arbitrary finite types with decidable equality on cryptograms; probabilities are real-valued functions with explicit non-negativity and normalization hypotheses rather than PMF, so that all sums are finite sums. A cipher bundles the enciphering maps, their injectivity, and the key distribution. The a posteriori probability is a real quotient, so it evaluates to zero when the cryptogram has probability zero; every statement that mentions it carries the hypothesis that the cryptogram has positive probability. Entropy uses the natural logarithm, with $x \mapsto -x\ln x$ vanishing at $0$; all inequalities are therefore in nats and are unaffected by the choice of base.

One trivializing formalization is ruled out explicitly: perfect secrecy is quantified over all a priori message distributions, not over one fixed distribution, and it is not vacuous — the cyclic milestone exhibits a family of ciphers satisfying it for every $n \ge 1$.

Contributions welcome beyond the milestones: finite conditional entropy and its chain rule as reusable lemmas, the equivalence of the present perfect-secrecy predicate with the statistical-independence formulation of message and cryptogram, and the extension of the model towards §11's equivocation $H_E(M)$, which is the next result of the paper to formalize.

Selected references

• C. E. Shannon, Communication Theory of Secrecy Systems, Bell System Technical Journal 28(4):656–715, 1949. https://doi.org/10.1002/j.1538-7305.1949.tb00928.x
• C. E. Shannon, A Mathematical Theory of Communication, Bell System Technical Journal 27(3):379–423, 1948. https://doi.org/10.1002/j.1538-7305.1948.tb01338.x

Motivation

Error-correcting codes protect information against corruption by adding controlled redundancy. For a code, the distribution of Hamming weights records how its words are spread across possible distances from the zero word and determines basic quantities such as its minimum distance. Linear codes also carry an algebraic duality: every linear code $C$ over a finite field has a dual code $C^\perp$ consisting of the words orthogonal to all words of $C$ under the standard coordinatewise bilinear form.

The MacWilliams identity states that the full Hamming-weight distribution of $C^\perp$ is determined by that of $C$ through one linear change of variables. It is the principal result of Chapter 5 of F. J. MacWilliams and N. J. A. Sloane's The Theory of Error-Correcting Codes. The binary identity appears there as Theorem 1, while the arbitrary-finite-field Hamming-weight-enumerator identity formalized here is Theorem 13 on p. 146. The surrounding chapter develops related transformations for complete, Lee, exact, joint, and split weight enumerators, nonlinear-code distance distributions, orthogonal arrays, and Krawtchouk polynomials.

This development isolates the arbitrary-$q$ Hamming identity as a first reusable result. Its declarations are designed to support later formalizations drawn from the same chapter and, more broadly, from the book, without enlarging the present target beyond the MacWilliams identity.

Setting

Let $F$ be a finite field of cardinality $q$, let $\iota$ be a finite coordinate type, and let a word be a function $c:\iota\to F$. A linear code $C$ is an $F$-linear subspace of the word space. The standard bilinear form is

$$\langle c,v\rangle=\sum_{i\in\iota}c_i v_i,$$

and the dual code is

$$C^\perp=\{v:\iota\to F:\langle c,v\rangle=0\text{ for every }c\in C\}.$$

The Hamming weight $\operatorname{wt}(c)$ is the number of coordinates at which $c$ is nonzero. Writing $n=|\iota|$, the homogeneous Hamming weight enumerator of $C$ is the integer-coefficient polynomial

$$W_C(X,Y)=\sum_{c\in C}X^{n-\operatorname{wt}(c)}Y^{\operatorname{wt}(c)}.$$

Thus the coefficient of $X^{n-j}Y^j$ is the number of codewords of weight $j$. The Lean development represents this object symbolically in MvPolynomial (Fin 2) ℤ; its complex-valued form is obtained by evaluation, so the symbolic and evaluated presentations share a single definition.

Formalization targets

Character orthogonality over a code

For a primitive complex additive character $\psi$ of $F$, define

$$S_C(v)=\sum_{c\in C}\psi(\langle c,v\rangle).$$

The first milestone states that $S_C(v)=|C|$ when $v\in C^\perp$ and $S_C(v)=0$ otherwise. The binary statement occurs as Problem 13 on p. 134 of MacWilliams--Sloane; Lemmas 9 and 11 on pp. 143--145 give the finite-field character and Fourier formulation.

Coordinatewise Hamming transform

For every word $c$ and all $X,Y\in\mathbb C$, the second milestone records the full character-weighted transform of the Hamming monomial:

$$\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)} (X-Y)^{\operatorname{wt}(c)}.$$

This is a separately reusable formulation of the coordinate calculation appearing in the proofs of Theorems 10 and 13 on pp. 144--146.

MacWilliams identity

The capstone is the following equality of integer polynomials:

$$|C|\,W_{C^\perp}(X,Y) = W_C\bigl(X+(q-1)Y,\,X-Y\bigr).$$

This is the denominator-free form of Chapter 5, Theorem 13. After evaluation over a characteristic-zero field it is equivalent to the normalized textbook formula

$$W_{C^\perp}(X,Y) = \frac{1}{|C|}W_C\bigl(X+(q-1)Y,\,X-Y\bigr).$$

Significance

The identity turns duality into an enumerative operation: knowing the weight enumerator of a linear code determines the weight enumerator of its dual. It supplies immediate consistency restrictions on possible weight distributions and is a basic input to the study of self-dual codes, Krawtchouk transforms, association schemes, invariant-theoretic properties of enumerators, and linear-programming bounds.

The formalization contributes a small common interface for finite-field words, linear codes, standard duals, and homogeneous Hamming weight enumerators. These declarations are absent from the selected Mathlib environment even though Mathlib already provides Hamming weight, finite-field algebra, additive characters, finite sums, bilinear-form orthogonals, and multivariate polynomials. Establishing the interface and its first central theorem makes those general libraries directly usable for subsequent coding-theory developments.

Difficulty

The paper statement is short, but its formal representations live in several different layers. Codes are submodules whose elements are subtypes; Hamming weight is a natural-number count; duality is expressed through a bilinear form; character identities take values in $\mathbb C$; and the final result is most reusable as an equality of symbolic polynomials over $\mathbb Z$. The central formalization burden is maintaining exact agreement while transporting the same enumerative data among these layers, including finite instances for codeword subtypes and the natural-number exponents of the homogeneous monomials.

The theorem must also retain the genuine finite-field statement. Replacing the code by an arbitrary finite set, hard-coding the binary field, defining the dual by its expected cardinality, or proving only equality at one chosen pair of evaluation points would not establish the target.

Formalization scope

The coordinate type is an arbitrary finite type rather than only Fin n; its cardinality plays the role of the code length. A word is CodingTheory.Word F ι := ι → F, and a linear code is a submodule of this common word space. This representation provides the linear structure and canonical orthogonal dual required here while leaving room for a future nonlinear-code type built from finite sets of the same words.

The polynomial CodingTheory.hammingWeightEnumeratorPolynomial has coefficients in $\mathbb Z$ and variables indexed by Fin 2. Variable $0$ records zero coordinates and variable $1$ records nonzero coordinates. Its name explicitly identifies the Hamming enumerator, leaving separate stable names available for future complete, Lee, exact, joint, and split weight enumerators. Those later enumerators should be added as new declarations and connected to this one by specialization theorems rather than replacing it.

The standard dual is bilinear, not Hermitian. The code alphabet may be any finite field. The zero code, full code, and empty coordinate type are included; in the empty-coordinate case there is one word of weight zero and the identity reduces to $1=1$. The present mission does not formalize nonlinear codes, complete or other generalized enumerators, orthogonal arrays, or Krawtchouk-polynomial theory. It establishes only the definitions and two character-sum milestones required for the Hamming MacWilliams identity, with a namespace and module boundary intended for reuse by later missions in the textbook series.

Selected references

• F. J. MacWilliams and N. J. A. Sloane, The Theory of Error-Correcting Codes, North-Holland, 1977, Chapter 5, pp. 125--154; especially Problem 13 (p. 134), Lemmas 9 and 11 (pp. 143--145), and Theorem 13 (p. 146). Publisher chapter record.
• Violetta Weger, Coding Theory, Technical University of Munich lecture notes, 2025, Theorem 11.2 and Lemma 11.8, pp. 154--159.
• F. J. MacWilliams, “A Theorem on the Distribution of Weights in a Systematic Code”, Bell System Technical Journal 42 (1963), 79--94.