Information Theory

Motivation

An exact linear observation $\langle x, S\rangle$ of a real signal can carry arbitrarily many bits. A finite message computed from a block of such observations cannot, but its information content is not controlled by the number of observations alone: if earlier messages have already concentrated the signal in a small region, the next block can exploit that concentration. Bounds of this kind are the engine of memory–sample lower bounds for noiseless Gaussian regression, where a learner with $M$ bits of memory must recover a unit vector to angular accuracy $\epsilon$ from a stream of exact Gaussian measurements.

This preprint asks how to restore a geometric spread condition on the posterior while paying for the information revealed in doing so, and proves that, for a cube-shaped prior on a spherical patch, $t$ blocks of $\Theta(d)$ exact measurements with messages of at most $\exp(Ad^2)$ values reveal only $O_A(dt)$ nats.

Background

• 2015. Steinhardt and Duchi prove memory–sample trade-offs for noisy sparse regression.
• 2016. Steinhardt, Valiant and Wager formulate a memory/sample conjecture for parity learning; Raz proves a quadratic-memory versus exponential-sample separation for parities, extended to a broad class of finite problems in 2017.
• 2019. Sharan, Sidford and Valiant prove an $\Omega(d\log r)$ sample lower bound for Gaussian regression with small additive noise, memory at most $d^2/4$ bits and Euclidean accuracy $d^{-r}$; their Section 7 expands projection moments into independent signal copies. Dagan, Kur and Shamir prove quadratic-memory lower bounds for approximately solving a consistent linear system in random order.
• 2026. OpenAI preprints on exact observations: Posterior replicas and conditional information in Gaussian regression, Replacing Gaussian observations in memory-constrained inference, and the present Localization costs and information growth for exact Gaussian observations (dated September 27, 2026), which supplies several localization routes to the $\Omega(d\log(1/\epsilon))$ lower bound for $o(d^2)$ memory. None of these preprints is peer reviewed; the Lean goal is open on this platform.

Setting

Let $d$ be large, $n = d - 1$, $k = \lfloor n/16\rfloor$, $m = \lfloor n/8\rfloor$. The cube prior is normalized Lebesgue measure $\mu_0$ on the half-open cube $Q_0 = [-1/(2\sqrt n), 1/(2\sqrt n))^n$, and the chart $\phi(z) = (z, \sqrt{1 - \|z\|^2})$ maps it into $S^{d-1}$. Dyadic cells of level $J$ subdivide $Q_0$ into $2^{nJ}$ half-open subcubes of side $2^{-J}/\sqrt n$.

Draw $Z \sim \mu_0$. In block $i = 1, \dots, t$ an independent standard Gaussian $k \times d$ matrix $X_i$ is drawn, and $(X_i, X_i\phi(Z))$ is observed exactly. A message $W_i \in \{1, \dots, N\}$ is drawn from a Borel probability kernel of the block data, whose choice may depend on the preceding messages $W_1, \dots, W_{i-1}$. Information is measured in nats by mutual information $I(\cdot\,;\cdot)$, defined as a relative entropy.

In Lean (OAI.RepeatedLocalization), Coordinate n = Fin n → ℝ, cubePrior n is Lebesgue measure conditioned on initialCube n, chart is $\phi$, a Cell n is a level $J$ with a multi-index in Fin (2^J), a BlockRule n N is a measurable probability vector on Fin N indexed by block data, Rules n N t chooses a rule for each block from the past history, and experimentLaw rules is the joint law of $(Z, W_1, \dots, W_t)$.

Formalization targets

Goal: Theorem 3.2 (Repeated localization), repeated_localization

There is an absolute $c > 0$ such that for every $C_0 > 0$ there is $C$ with the following property, for $d$ large. If

$$\big(2/m + e^{-ck}\big)\log N \le C_0 d,$$

then one can reveal nested dyadic cells $Q_0 \supset Q_1 \supset \cdots \supset Q_t$ containing $Z$, with $Q_i$ a finite-valued measurable function of $Z$ and $W_1, \dots, W_i$, such that the augmented transcript $\Pi_t = (W_1, Q_1, \dots, W_t, Q_t)$ satisfies

$$I(Z; \Pi_t) \le C d t, \qquad \mathbb{E}\, J_t \le C t,$$

where $J_t$ is the level of $Q_t$. An alphabet of size $N \le \exp(Ad^2)$ satisfies the hypothesis with $C_0$ depending only on $A$.

Milestones (results from the paper's other routes)

• Lemma 5.2 (finite expected regularization of a finite-relative-entropy posterior by a terminating dyadic search).
• Lemma 12.1 (convexity and coercivity of the kernel potential $\Phi(\nu) = D(\nu\|\sigma) - \int \log J_\nu\, d\nu$).
• Proposition 12.6 (the potential grows by at most $Cd$ per block).
• Lemma 13.2 (inverse simplex-volume moment under a ball bound, with no support restriction).

Significance

The result. Theorem 3.2 is the first information estimate in the paper and the model for its later routes: it shows that revealing a nested dyadic cell after each block, which restores the spread condition needed by the projection estimate, costs only $O(d)$ nats per block. Since the original message history is a function of $\Pi_t$, the bound also controls the information in the messages alone. Combined with the paper's endpoint arguments this yields the lower bound $T \ge c\,d\log(1/\epsilon)$ for learners with $o(d^2)$ bits.

Formalizing it. These results are proved only in an unrefereed preprint; no machine-checked proofs exist. The milestones are independent analytic statements (an entropy regularization, a convex potential and its drift, an inverse-volume moment) that are reusable in the companion missions on exact Gaussian observations.

Difficulty

The information a block reveals depends on how concentrated the current posterior is, and earlier messages can make it arbitrarily concentrated. Simply conditioning on messages gives no control. Revealing a localizing cell restores spread, but naming a cell itself costs information, and the count of candidate cells at depth $j$ grows like $2^{nj/2}$; the argument must show that confinement to a depth-$j$ cell (worth $nj$ bits relative to the prior) pays for this, uniformly over all message rules.

Formalization scope

• The prior is the image of cube volume under $\phi$, not surface measure; coordinates are Fin n → ℝ, and $d$ appears as n + 1.
• Row counts and parameters are natural-number floors n / 16, n / 8. Gaussian entries are gaussianReal 0 1.
• A disclosure Q : Disclosure n N t is valid when each cell map is measurable with finite range, contains $Z$, lies in $Q_0$, and the cells are nested. The goal asserts existence of a valid disclosure with mutualInformation (augmentedLaw rules Q) ≤ C (n+1) t and expected final level at most $Ct$.
• Mutual information is klDiv of the joint law against the product of marginals, valued in ℝ≥0∞.

The goal is not trivial: the trivial disclosure (always $Q_0$) does not bound the information in arbitrary messages, and the quantifier order (absolute $c$, then $C_0$, then $C$) matches the source.

Needed infrastructure: Gaussian projections of measures on cells, $L^m$ density bounds, dyadic cell combinatorics, and relative-entropy chain rules. Contributions toward any milestone are welcome.

Selected references

• OpenAI, Localization costs and information growth for exact Gaussian observations, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Localization-costs-and-information-growth-for-exact-Gaussian-observations-September-27-2026/paper.pdf
• OpenAI, Posterior replicas and conditional information in Gaussian regression, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/main/preprints/Posterior-replicas-and-conditional-information-in-Gaussian-regression-September-27-2026/paper.pdf
• V. Sharan, A. Sidford, G. Valiant, Memory-Sample Tradeoffs for Linear Regression with Small Error, STOC 2019. https://doi.org/10.1145/3313276.3316403
• R. Raz, Fast Learning Requires Good Memory, 2016. https://arxiv.org/abs/1602.05161
• R. Raz, A Time-Space Lower Bound for a Large Class of Learning Problems, FOCS 2017. https://doi.org/10.1109/FOCS.2017.73
• J. Steinhardt, G. Valiant, S. Wager, Memory, Communication, and Statistical Queries, COLT 2016. https://proceedings.mlr.press/v49/steinhardt16.html
• J. Steinhardt, J. Duchi, Minimax Rates for Memory-Bounded Sparse Linear Regression, COLT 2015. https://proceedings.mlr.press/v40/Steinhardt15.html
• Y. Dagan, G. Kur, O. Shamir, Space Lower Bounds for Linear Prediction in the Streaming Model, COLT 2019. https://proceedings.mlr.press/v99/dagan19b.html
• T. Austin, Multi-variate correlation and mixtures of product measures, Kybernetika, 2020.

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.

Binary and spherical codes, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

For every real $\delta$ with $0<\delta<1/2$, the following strict inequality holds. Write $h(x)=-x\log_2x-(1-x)\log_2(1-x)$, with the total-real logarithm convention $\log_2 0=0$. Let $A(n,k)$ be the maximum cardinality of a finite subset of $\{0,1\}^n$ in which every two distinct words differ in at least $k$ coordinates, and put $R(\delta)=\limsup_{n\to\infty}\log_2 A(n,\lceil\delta n\rceil)/n$. Empty codes are permitted in the maximum; the $n=0$ sequence term is zero by total real division. Define $g(v)=h((1-\sqrt{1-v})/2)$ and $M(\delta)=\inf_{0\leq t\leq1-2\delta}\{1+g(t^2)-g(t^2+2\delta t+2\delta)\}$, a real infimum. Then $R(\delta)<M(\delta)$.

Additional targets:

• Binary-code rate is strictly below the classical entropy expression.
• Positive gap below the classical binary-code rate expression.
• Binary-code rate is bounded by the combined variational infimum.
• The combined variational rate is strictly below the defined MRRW rate.
• Positive gap below the defined MRRW binary-code rate.
• Binary-code rate bound and strict improvement of the MRRW rate.
• Finite spherical-code bounds and the closed hierarchy rate bound.
• Strict descent of spherical-code hierarchy rates and localized rates.
• Eventual kissing-number bound with exponent 0.39661.

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, B_BinaryCodes.json, B_SphericalCodes.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

Motivation

A Costas array is a permutation matrix in which the difference vectors between distinct dots are pairwise distinct; such arrays are frequency-hopping patterns for sonar and radar (Costas, 1984). Rubio and Torres ask whether their $m$-dimensional version can stay Costas in every window of its periodic extension, and conjecture that this happens only in the smallest order.

Timeline. 1984: Taylor proves that 2D periodic Costas arrays have order $\le 2$. 2023: Rubio–Torres prove the odd-order and 3D cases, give $2\times2\times4$ examples, and state Conjecture 1.

Setting

Let $[n]=\{1,\dots,n\}$, $X=[a_1]\times\cdots\times[a_k]$, $Y=[b_1]\times\cdots\times[b_l]$ with all sides $\ge2$, and $\varphi:X\to Y$ a bijection; the dots are $(x,\varphi(x))\in\mathbb Z^{k+l}$. The array is Costas if the difference vectors between distinct dots are distinct, and periodic Costas if moreover, after repeating the dots periodically over $\mathbb Z^{k+l}$, the dots inside every translate $t+X\times Y$ have distinct difference vectors.

Formalization target

Conjecture 1: if $k\ge l\ge1$ and $\varphi$ defines a periodic Costas array, then

$$\prod_{i=1}^k a_i=2^k,$$

equivalently every $a_i=2$. The condition $k\ge l$ is a normalization ($\varphi^{-1}$ swaps the boxes).

Significance

A proof would give the multidimensional analogue of Taylor's theorem; a counterexample would give periodic distinct-difference patterns of non-power-of-two order.

Difficulty

The Rubio–Torres counting argument needs a bound that is available only when $Y$ is one-dimensional, which is why it stops at $m=3$. Computational evidence: an exhaustive window check reports that the $2\times3\times2\times3$ array with dots $(1,1,1,1),(1,2,1,2),(1,3,2,1),(2,1,1,3),(2,2,2,3),(2,3,2,2)$ is periodic Costas, which would disprove the conjecture.

Formalization scope

A point of $\mathbb Z^{k+l}$ is a pair $(x,y)$; boxes are 1-based; $\varphi$ is a total function $\mathbb Z^k\to\mathbb Z^l$ whose values off $X$ are unused. Differences are plain integer vectors (not reduced modulo the sides), windows range over all $t\in\mathbb Z^{k+l}$, and $k,l\ge1$ and sides $\ge2$ are part of the definition, so no degenerate case holds vacuously.

Selected references

• I. Rubio, J. Torres, Multidimensional Costas Arrays and Their Periodicity, IEEE Trans. Inf. Theory 69(8), 2023, 5032–5040. arXiv:2208.02378, DOI
• J. P. Costas, A study of a class of detection waveforms having nearly ideal range-Doppler ambiguity properties, Proc. IEEE 72(8), 1984, 996–1009.
• S. W. Golomb, H. Taylor, Constructions and properties of Costas arrays, Proc. IEEE 72(9), 1984, 1143–1163.

Motivation

The free energy principle (FEP) proposes that a self-organizing system — a brain, an organism, an agent — persists by minimizing one quantity: the variational free energy of its sensory states under an internal generative model. Introduced by Karl Friston as a principle of brain function [Friston 2006] and stated in its unified form [Friston 2010], the principle makes a precise mathematical claim at its core: whatever internal state estimate the system holds, the free energy of incoming data is never below the data's surprisal (negative log marginal likelihood), and the excess is exactly the Kullback–Leibler divergence between the system's recognition density and the Bayesian posterior implied by the model. Active inference extends the same functional from perception to action and planning [Friston et al. 2017], and the same bound is known in machine learning as the evidence lower bound (ELBO) of variational inference [Parr et al. 2022].

Timeline of the mathematical content this mission formalizes:

• 2006 — Friston, A free energy principle for the brain (J. Physiol. Paris 100): the bound stated for perception as variational inference on a generative model.
• 2010 — Friston, The free-energy principle: a unified brain theory? (Nat. Rev. Neurosci. 11, 127–138): free energy as an upper bound on surprisal, presented as the core of a unified account.
• 2017 — Friston, FitzGerald, Rigoli, Schwartenbeck, Pezzulo, Active inference: a process theory (Neural Comput. 29(1), 1–49): the same functional drives policy selection through expected free energy.
• 2022 — Parr, Pezzulo, Friston, Active Inference (MIT Press): textbook treatment; the posterior-form identity $F = D_{\mathrm{KL}}(Q\,\|\,P(s|o)) - \log P(o)$ as the central equation.
• 2026 — fep_formal (Active Inference Institute): a machine-checked Lean 4 catalogue of 155 Free Energy Principle topics, compiled with zero proof holes against a pinned Mathlib. This mission transcribes the catalogue's core-free-energy chain — topic fep-002 and the foundation module active_inference — onto the platform, turning the first link of the FEP development into solvable community infrastructure.

Setting

Everything is finite, and laws are normalized real mass functions.

A finite law on a finite type $\alpha$ is a function $p : \alpha \to \mathbb{R}$ with $p(x) \ge 0$ for every $x$ and $\sum_x p(x) = 1$. A finite kernel from $\alpha$ to $\beta$ assigns to each $x \in \alpha$ a normalized row over $\beta$. The mission's definitions Def_fep_finite_laws and Def_fep_finite_information package these carriers with entropy, cross-entropy, and the KL divergence

$$D_{\mathrm{KL}}(p\,\|\,q) \;=\; \sum_{x} q(x)\cdot \mathrm{klFun}\!\left(\frac{p(x)}{q(x)}\right), \qquad \mathrm{klFun}(x) = x\log x + 1 - x,$$

a totalized real-valued divergence that is finite even at zero-mass atoms (the convention $0 \cdot \log 0 = 0$ via Real.negMulLog) and nonnegative on normalized laws.

A finite generative model for active inference (definition Def_fep_generative_model) over finite types $\mathsf{Policy}, \mathsf{State}, \mathsf{Outcome}$ consists of: an initial state law $P(s)$; a policy-conditioned transition kernel; a state-to-outcome likelihood kernel; a preference law over outcomes; and a policy prior. Under a policy $\pi$ the model predicts the state law $P(s \mid \pi)$ and the outcome law $P(o \mid \pi)$. A recognition density is any finite law $Q$ over states — the system's internal estimate. At an outcome $o$ with positive predicted mass, the Bayesian posterior $P(\cdot \mid o, \pi)$ is the exact finite Bayes rule. The outcome surprisal is $-\log P(o \mid \pi)$, and the posterior-form variational free energy of a recognition density $Q$ is

$$F[Q, o, \pi] \;=\; D_{\mathrm{KL}}\big(Q \,\|\, P(\cdot \mid o, \pi)\big) \;-\; \log P(o \mid \pi).$$

Formalization targets

Goal: the variational free-energy bound

For every generative model, every policy $\pi$, every outcome $o$ with $P(o\mid\pi) > 0$, and every recognition density $Q$:

$$-\log P(o \mid \pi) \;\le\; F[Q, o, \pi].$$

The recognition density $Q$ is universally quantified — the bound holds for whatever state estimate the system happens to carry.

Exactness, uniqueness, and the ELBO form

Three companions pin down the equality case, ordered weakest to strongest alongside the milestone list:

• Exactness — the Bayesian posterior attains the bound:

$$F\big[P(\cdot \mid o, \pi),\, o,\, \pi\big] = -\log P(o \mid \pi).$$

• Uniqueness — equality characterizes the posterior, with no full-support assumption:

$$F[Q, o, \pi] = -\log P(o \mid \pi) \iff Q = P(\cdot \mid o, \pi).$$

• ELBO form — negating both sides:

$$-F[Q, o, \pi] \;\le\; \log P(o \mid \pi).$$

Measure-theoretic core

Independently of the finite model, in Mathlib's nonnegative extended reals $\mathbb{R}_{\ge0} \cup \{\infty\}$, with $q$, $p$ measures on any measurable space and $s \in \mathbb{R}_{\ge0} \cup \{\infty\}$:

$$s \;\le\; s + D_{\mathrm{KL}}(q \,\|\, p),$$

the unconditional shape of the bound (topic fep-002 of the source catalogue), with the divergence taken as $\infty$ when the log-likelihood ratio is not integrable.

Significance

The result itself. This inequality is the load-bearing step of the FEP: it converts "minimize free energy" into "move recognition toward the posterior," and it is the exact statement whose continuous, dynamic, and policy-selecting extensions (expected free energy, Markov blankets, non-equilibrium thermodynamics) form the rest of the FEP literature. Without it, the principle's variational step has no mathematical content.

Formalizing it. The mathematics here is classical — Gibbs' inequality — and the source development already proves every row with no proof holes. What the mission adds is faithful, reusable infrastructure: the definitions are published as platform nodes in the shared namespace FreeEnergyPrinciple, so later missions in this programme (expected free energy and policy selection, Markov blankets, Gaussian and continuous-time variants, already proved in the source repository) can import them instead of re-deriving the substrate. Status honesty: all eight items below are formalized and machine-checked locally against the platform environment; each is an open problem on the platform only in the sense that no proof has yet been submitted to it.

Difficulty

The bound itself is a one-line consequence of KL nonnegativity — the naive idea "prove it by simp on the KL sum" is essentially right, and the source proofs are correspondingly short. The actual difficulty is boundary precision, where plausible renderings go silently wrong:

• The positivity premise $P(o \mid \pi) > 0$ is not decoration: the Bayesian posterior is defined only where the evidence has positive mass, and hiding that in a totalized division would change the statement.
• The uniqueness characterization is not a formality: at zero-mass reference atoms the logarithmic cross-entropy identity degenerates, and the proof needs the normalization lemma $D_{\mathrm{KL}}(p\,\|\,q) = 0 \leftrightarrow p = q$, which forces the recognition law's mass to zero wherever the posterior's is zero. A solver who proves the bound but states equality with a full-support hypothesis has proved something different from the source.
• The measure-theoretic core is deliberately unconditional; adding finiteness side conditions to it would weaken the source's point that $\mathbb{R}_{\ge0} \cup \{\infty\}$ absorbs the degenerate cases.

A vacuous formalization — quantifying over a single distinguished recognition law, or taking "posterior" as an arbitrary variable — would trivialize the goal; the targets below rule this out by fixing the exact finite Bayes rule and universally quantifying $Q$.

Formalization scope

Committed conventions of this mission's Lean development:

• All model carriers are finite types (Fintype); laws are $\mathbb{R}$-valued normalized mass functions; kernels are normalized rows. No measure-theoretic machinery below the finite substrate except for the measure-theoretic core milestone.
• KL is the totalized real-valued finite divergence $D_{\mathrm{KL}}(p\,\|\,q) = \sum_x q(x)\cdot \mathrm{klFun}(p(x)/q(x))$; entropy uses Real.negMulLog, so $0 \cdot \log 0 = 0$ exactly, not by exception-handling.
• The posterior is the exact finite Bayes rule FiniteKernel.posterior, taken at the explicit hypothesis $0 < P(o \mid \pi)$.
• One mission-wide namespace FreeEnergyPrinciple; definitions live in the published definition files Def_fep_finite_laws, Def_fep_finite_information, Def_fep_generative_model, and every theorem item imports them. A Free Energy Principle II mission (expected free energy) is expected to reuse the same namespace and definitions.
• The measure-theoretic core uses Mathlib's InformationTheory.klDiv in ℝ≥0∞ with no finiteness hypotheses.
• Contributions welcome: alternative measure-theoretic renderings of the core bound, the Gaussian instantiation of the same identity, and ports of the source repository's subsequent rows (Bayesian model reduction, expected free energy) onto these definitions.

Selected references

• K. Friston, A free energy principle for the brain, Journal of Physiology (Paris) 100 (2006) 70–87. https://doi.org/10.1016/j.jphysparis.2006.10.001
• K. Friston, The free-energy principle: a unified brain theory?, Nature Reviews Neuroscience 11 (2010) 127–138. https://doi.org/10.1038/nrn2787
• K. Friston, T. FitzGerald, F. Rigoli, P. Schwartenbeck, G. Pezzulo, Active inference: a process theory, Neural Computation 29 (2017) 1–49. https://doi.org/10.1162/neco_a_00912
• T. Parr, G. Pezzulo, K. J. Friston, Active Inference: The Free Energy Principle in Mind, Brain, and Behavior, MIT Press (2022). https://mitpress.mit.edu/9780262045354/active-inference/
• D. A. Friedman, fep_formal: Towards Lean 4 Formalization of the Free Energy Principle (v1.2.0), Active Inference Institute (2026), the formal source of truth for this mission. https://github.com/ActiveInferenceInstitute/fep_formal
• D. A. Friedman, Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, Active Inference Journal (2026). https://doi.org/10.5281/zenodo.19699233