Motivation

Distributionally robust optimization evaluates a decision against a set of plausible probability laws rather than against a single estimated law. A common way to specify that set is to choose a nominal law $P_0$ and allow every law $P$ whose discrepancy from $P_0$ is below a radius $\varepsilon$. Different discrepancies produce different ambiguity sets, so comparing them tells a modeler what one constraint guarantees about another. Rahimian and Mehrotra collect such constructions in their survey and state a chain of comparisons among variation, Hellinger, Kullback–Leibler, and J-divergences in Lemma 5.4 (arXiv:1908.05659v1, pp. 31, 34–35). The chain connects four common ways of controlling model error without requiring a finite outcome space or a common density chosen in advance.

The source is the 2019 arXiv v1 preprint of a survey. Its proof of Lemma 5.4 cites earlier work rather than giving a full derivation. The preprint also prints an additional J-to-$\chi^2$ comparison that is false; this mission isolates the part that holds for every pair of probability measures. The distinction matters when an ambiguity set is used to certify a bound under a different divergence: an inclusion based on the false link can certify laws that are outside the intended set.

Setting

Let $(\Xi,\mathcal F)$ be a measurable space, and let $\mathfrak M(\Xi,\mathcal F)$ be its probability measures. Given $P_1,P_2\in\mathfrak M(\Xi,\mathcal F)$, a $\phi$-divergence $\mathfrak D^\phi(P_1,P_2)$ compares their densities using a function $\phi:[0,\infty)\to[0,\infty]$ with $\phi(1)=0$. The paper assumes $\phi$ is convex. To account for measures that are not mutually absolutely continuous, take the common dominating measure $\nu=P_1+P_2$ and write $p=dP_1/d\nu$ and $q=dP_2/d\nu$. The integrand is $q\phi(p/q)$ when $q>0$ and $p\phi'(\infty)$ when $q=0$, where $\phi'(\infty)=\lim_{t\to\infty}\phi(t)/t$; a point with $p=q=0$ contributes zero (§5.1.2, p. 31).

Table 1 gives four generators used here:

$$\phi_v(t)=|t-1|,\qquad \phi_h(t)=(\sqrt t-1)^2,\qquad \phi_{\mathrm{kl}}(t)=t\log t-t+1,\qquad \phi_j(t)=(t-1)\log t.$$

The first two divergences are the full $L^1$ variation discrepancy and the unhalved squared Hellinger discrepancy. In particular, $\mathfrak D^{\phi_v}=2d_{\mathrm{TV}}$, where $d_{\mathrm{TV}}$ is the total variation distance defined later in the paper. The J generator has $\phi_j(0)=+\infty$, understood as its limit at zero; $\phi_{\mathrm{kl}}(0)=1$ under $0\log0=0$. The recession slopes of the four generators, in the displayed order, are $1,1,+\infty,+\infty$ (Table 1, p. 31; §5.1.3, p. 35).

For a nominal probability measure $P_0$ and a nonnegative radius $\varepsilon$, equation (5.9) defines the ambiguity ball

$$\mathcal P^\phi(P_0;\varepsilon) =\{P\in\mathfrak M(\Xi,\mathcal F):\mathfrak D^\phi(P,P_0)\le\varepsilon\}.$$

Formalization targets

The three milestone comparisons are the valid initial part of (5.10), for every $P,P_0\in\mathfrak M(\Xi,\mathcal F)$:

$$\frac14\bigl(\mathfrak D^{\phi_v}(P,P_0)\bigr)^2 \le\mathfrak D^{\phi_h}(P,P_0) \le\mathfrak D^{\phi_{\mathrm{kl}}}(P,P_0) \le\mathfrak D^{\phi_j}(P,P_0).$$

The middle comparison is also stated in footnote 18. The mission goal is the corrected Lemma 5.4: it joins these three comparisons to the resulting valid part of (5.11), for every nominal $P_0$ and radius $\varepsilon$:

$$\mathcal P^{\phi_j}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_{\mathrm{kl}}}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_h}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_v}(P_0;2\sqrt\varepsilon).$$

Each inclusion has the direction induced by the preceding divergence inequality: a stronger divergence constraint gives a smaller ball. The first comparison retains the paper's factor $1/4$, and the final ball retains its radius $2\sqrt\varepsilon$ (Lemma 5.4, p. 34).

Significance

The result allows a J-divergence or KL-divergence ambiguity model to carry a simultaneous bound in Hellinger and full variation divergence. A Hellinger radius $\varepsilon$ yields the explicit variation radius $2\sqrt\varepsilon$; this makes the scale change visible when comparing two models built with different discrepancies. Without a general-measure statement, a finite-outcome approximation does not itself cover continuous laws or pairs with a singular component.

The paper presents the inequalities as known and cites sources for them. A finite-alphabet TV–Hellinger–KL chain and a general-measure KL–affinity bound already have machine-checked results in the platform catalog. The work here is to formalize the four generators with one shared general-measure divergence, close the remaining inequalities in that representation, and connect them to the ambiguity-ball inclusions. This also provides reusable definitions for other distributionally robust models that use the same divergence convention.

Difficulty

Writing the density ratio only with respect to $P_0$ loses the part of $P$ singular to $P_0$. That would change both variation and Hellinger divergence and make the stated chain an unreliable comparison of the paper's objects. At the opposite boundary, $P$ can vanish on a set that $P_0$ charges. There the J generator must be infinite, although a direct use of a total real logarithm at zero can assign it an incorrect finite value. These two edge cases make an apparently routine pointwise comparison insufficient for the full measurable-space theorem.

Formalization scope

Lean represents $P$ and $P_0$ as ProbabilityMeasure Ξ on an arbitrary MeasurableSpace Ξ. It computes Radon–Nikodym densities relative to $P+P_0$, evaluates the divergence with an extended nonnegative Lebesgue integral, and represents both divergence values and radii in ENNReal. The generic definition computes the recession slope as a limsup; for the four Table 1 generators this is the limit in the paper. The formal ambiguity ball contains probability measures only. A top radius is allowed by the type; the finite nonnegative radii are the paper's intended model parameters. The generic operation does not take a convexity certificate, but the four named generators are the only ones used in the theorem.

The formalization must not turn a nondominated pair into divergence zero or assign $\phi_j(0)=0$: either choice changes the claimed chain. It must also retain the full variation divergence, without the half factor used for total variation distance. The definitions of the common-measure divergence, its four generators, and the ambiguity ball are intended for reuse. Contributions establishing properties of the recession slopes, comparison lemmas on arbitrary measurable spaces, and their ambiguity-set consequences are within scope.

The paper's final inequality in (5.10), $\mathfrak D^{\phi_j}\le\mathfrak D^{\phi_{\mathrm{ca}^2}}$, and the associated first inclusion in (5.11) are removed. They are false even on a two-point space: with $P_0=(1/2,1/2)$ and $P=(0,1)$, J-divergence is $+\infty$ while the order-two $\chi$-divergence is $1$. Thus $P$ lies in the latter ball of radius $1$ but outside the J ball of that radius. The source's footnote 18 separately notes an error in a cited Hellinger–KL comparison; the corrected Hellinger–KL inequality is retained (pp. 34–35).

Selected references

• H. Rahimian and S. Mehrotra, Distributionally Robust Optimization: A Review, arXiv preprint arXiv:1908.05659v1, 2019. Preprint.

Motivation

Quantum communication and computation often require a receiver to infer which preparation was sent after it has passed through a noisy quantum process. When possible preparations are mixed states, their overlap makes exact identification impossible. A measurement is then judged by its average probability of a correct label. The pretty good measurement gives a concrete measurement from the ensemble itself, without first solving the optimization over all measurements. Barnum and Knill related it to a general reversal operation for noisy dynamics and bounded its error through pairwise state fidelities in their preprint, §V–VI. The bound is useful when the overlaps are easier to estimate than the measurement's success probability.

The present mission addresses the preprint's second main result. The source is arXiv:quant-ph/0004088v2, not the later journal pagination. The preprint also strengthens its Theorem 3 relative to the published text, as its acknowledgment explains; this mission concerns Theorem 5 and the calculation around it.

Setting

An ensemble is a finite family of output density matrices $\hat\rho_j$ with probabilities $p_j\geq0$ satisfying $\sum_jp_j=1$. A density matrix is a positive semidefinite complex matrix with trace one. For each label $j$, fix an orthonormal eigenbasis $v_{ij}$ and nonnegative eigenvalues $\lambda_{ij}$ such that

$$\hat\rho_j=\sum_i\lambda_{ij}|v_{ij}\rangle\langle v_{ij}|, \qquad \sum_i\lambda_{ij}=1.$$

The eigenpair index $i$ runs over a finite output basis $O$; zero eigenvalues are allowed. The input labels form a finite basis $J$. A label distribution is represented by $\rho=\sum_jp_j|j\rangle\langle j|$.

The paper's classicizing channel $A$ has Kraus operators $A_{ij}=\sqrt{\lambda_{ij}}|v_{ij}\rangle\langle j|$. Acting on an input matrix $X$, its value is $A(X)=\sum_{i,j}A_{ij}X A_{ij}^{\dagger}$. In particular, its output on $\rho$ is $\rho_{\mathrm{out}}=\sum_jp_j\hat\rho_j$. The paper assumes $\rho_{\mathrm{out}}$ has full support when it writes its reversal operation. For a general Kraus family $A_a$, that operation has operators

$$(R_{A,\rho})_a=\rho^{1/2}A_a^\dagger A(\rho)^{-1/2}.$$

The inverse square root is spectral: invert nonzero eigenvalues and leave zero eigenvalues at zero. With full support, it is the usual inverse square root.

For an input label $j$, classical fidelity is the chance that the composite operation returns the same label. Averaging gives

$$F_{\mathrm{cl}}(\rho,K)= \sum_jp_j\langle j|K(|j\rangle\langle j|)|j\rangle.$$

The Bures–Uhlmann fidelity used here is the unsquared quantity $F_{\mathrm{BU}}(\sigma,\tau)=\operatorname{tr}\sqrt{\sqrt\sigma\,\tau\,\sqrt\sigma}$. For the classicizing channel, the reversal operation realizes the pretty good measurement, as shown by equation (36) and the discussion after equation (37) in the preprint, p. 10.

Formalization targets

Recovery error

The goal, in the reading established by the paper's proof, is

$$F_{\mathrm{cl}}(\rho,R_{A,\rho}A) \geq 1-\sum_{\substack{i,j\in J\\i\ne j}} \sqrt{p_ip_j}\,F_{\mathrm{BU}}(\hat\rho_i,\hat\rho_j).$$

The sum is over ordered pairs; each unordered pair of distinct labels is counted twice. The coefficient is exactly one. The goal applies to every finite ensemble with the spectral data above and a full-support output. It does not fix the number of labels or the dimension of the output.

The milestones are the reversal formula (36), the classical-fidelity identities in (38), the unit squared Frobenius norm (40), the diagonal-block expression (41), the off-diagonal trace-norm identity following (42), and the two-block estimate of Lemma 6. They record the paper's mathematical statements and keep the attack path tied to the authors' displayed results.

Significance

The result bounds a measurement's probability of error using only pairwise similarities of the possible output states and their prior probabilities. For nearly distinguishable states, the weighted fidelity sum is small, so this particular measurement succeeds with high probability. The theorem therefore gives a usable guarantee for a specified recovery procedure, rather than only asserting that some procedure exists. In the preprint, §VII, Barnum and Knill describe quantum-information applications of such recovery bounds.

The mathematical result is already proved in the paper, subject to the correction explained below. The formalization work is to make the mixed-state channel, its recovery, the finite-dimensional spectral conventions, and the block-matrix norm estimate precise in Lean. The published Prove2Me definitions for Kraus updates and trace norm supply reusable starting points. A complete proof of this mission would add a checked mixed-state pretty-good-measurement bound; the local statements here compile as open theorems, and no proof is claimed.

Difficulty

The obvious pairwise-overlap estimate does not by itself express the error of the recovery channel. The recovery's classical fidelity is initially a channel evaluation on basis states, while the bound uses trace norms of blocks of a Gram matrix. The key obstacle is controlling the off-diagonal Frobenius mass of the positive square root of that Gram matrix by the trace norms of the corresponding blocks of the Gram matrix itself. Lemma 6 states the needed two-block comparison, including rectangular blocks. The matrix dimension and block labels must remain consistent when it is applied across a larger array.

Formalization scope

All systems and index sets are finite, with matrices over $\mathbb C$ and real probabilities. A general completely positive map is represented by an unbundled finite family of Kraus matrices. The classicizing family has rectangular matrices from the input-label space to the output space; the reversal has matrices in the opposite direction. Composite Kraus families are indexed by pairs. The classical fidelity is defined from the channel action in equation (10); the goal does not define it using the desired overlap bound. The reversal is defined by equation (12) for a general family, so its specialized formula remains a theorem.

The spectral hypotheses include nonnegative probabilities and eigenvalues, unit sums, and orthonormal eigenvectors. Full support of $\rho_{\mathrm{out}}$ is an explicit hypothesis wherever the reversal appears, following page 7. Empty input or output types cannot satisfy the normalized data together with these hypotheses. The Bures–Uhlmann expression is the unsquared trace of a positive square root; using the squared fidelity would change the constant and is outside this mission. Lemma 6 is independent of the ensemble and can be reused for finite block-matrix estimates. Contributions to the spectral identities, the array equalities, and the block-norm argument are welcome.

Equation (39) prints the square of the optimal success probability on its left. The first line of (38) compares that quantity with the recovery fidelity in the opposite direction to Corollary 4. The proof on pages 12–13 concludes the displayed bound for $F_{\mathrm{cl}}(\rho,R_{A,\rho}A)$. This mission states that proved conclusion and records the printed discrepancy in its item and audit notes.

Selected references

• Howard Barnum and Emanuel Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, arXiv:quant-ph/0004088v2, 2000/2026 version. arXiv
• Howard Barnum and Emanuel Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, Journal of Mathematical Physics 43 (2002), 2097–2106. DOI

Motivation

Biometric readings, typed passphrases and physical measurements are secrets that are never reproduced exactly: a second reading $w'$ of the same fingerprint differs from the enrolled reading $w$ in a few positions. Dodis, Ostrovsky, Reyzin and Smith (arXiv:cs/0602007, SIAM J. Comput. 38(1), 2008) introduced the secure sketch, public helper data that lets anyone holding a nearby $w'$ recover $w$ while leaking as little as possible about $w$, and the fuzzy extractor, which in addition turns $w$ into a nearly uniform key. Their constructions for the Hamming, set-difference and edit metrics are the standard reference for this primitive in cryptography.

A construction is judged by its entropy loss: how much min-entropy of the secret the published sketch destroys. To call a construction optimal one needs a lower bound on that loss which holds for every sketch, whatever its algorithm. Appendix C of the paper supplies such a bound from coding theory. It shows that, for uniformly distributed inputs, the code-offset sketch for the Hamming metric and the set-difference sketches lose no more entropy than any sketch must. This mission formalizes that bound, Lemma C.1.

Setting

A metric space is a finite set $\mathcal M$ with an integer-valued distance $\mathrm{dis}$; the paper also requires $\mathrm{dis}(x,y)=0$ exactly when $x=y$, symmetry, and the triangle inequality (§2.1, p. 7). Random variables are identified with their laws; logarithms are base 2.

The min-entropy of a random variable $A$ is $\mathbf H_\infty(A) = -\log \max_a \Pr[A=a]$. For a pair $(A,B)$ the average min-entropy is

$$\tilde{\mathbf H}_\infty(A\mid B) = -\log \mathbb E_{b\leftarrow B}\Big[\max_a \Pr[A=a\mid B=b]\Big],$$

the negative logarithm of the probability that an adversary who sees $B$ guesses $A$.

An $(\mathcal M,m,\tilde m,t)$-secure sketch (Definition 3, p. 11) is a pair of randomized procedures: $\mathsf{SS}$ maps $w\in\mathcal M$ to a string $s$, and $\mathsf{Rec}$ maps $(w',s)$ back to $\mathcal M$. Correctness: if $\mathrm{dis}(w,w')\le t$ then $\mathsf{Rec}(w',\mathsf{SS}(w))=w$. Security: for every distribution $W$ on $\mathcal M$ with $\mathbf H_\infty(W)\ge m$, one has $\tilde{\mathbf H}_\infty(W\mid \mathsf{SS}(W))\ge\tilde m$.

An $(\mathcal M,K,t)$-code (§2.2, p. 8) is a set $C\subseteq\mathcal M$ of $K$ points such that every ball $\{c : \mathrm{dis}(w,c)\le t\}$ around a point $w\in\mathcal M$ contains at most one codeword. For $S\subseteq\mathcal M$, $K(\mathcal M,t,S)$ is the largest $K$ for which an $(\mathcal M,K,t)$-code lies inside $S$, and $K(\mathcal M,t)=K(\mathcal M,t,\mathcal M)$. Finally (Appendix C, p. 40)

$$L(\mathcal M,t,m) = \log\Big(\min_{|S|=2^m} K(\mathcal M,t,S)\Big),$$

the worst case, over all sets $S$ of $2^m$ points, of the largest $t$-error-correcting code inside $S$.

In the Lean development these are minEntropy, avgMinEntropy, IsSecureSketch, IsCode, K dis t S and L dis t N hN, in the namespace FuzzyExtractors.LowerBound.

Formalization targets

Goal: Lemma C.1

If $(\mathsf{SS},\mathsf{Rec})$ is an $(\mathcal M,m,m',t)$-secure sketch and $2^m=N$ is a natural number with $N\le|\mathcal M|$, then

$$m' \le L(\mathcal M,t,m).$$

The bound fixes no particular metric and no particular sketch; it is stated for every finite integer-valued metric and every sketch, with an arbitrary type of sketch values.

Milestones

The proof in Appendix C has three steps, each a milestone. For $W$ uniform on a set $S$ of $2^m$ points:

1. some sketch value $v$ has $\Pr[\mathsf{SS}(W)=v]>0$ and $\mathbf H_\infty(W\mid\mathsf{SS}(W)=v)\ge m'$;
2. the set $T$ of points of $S$ that can produce $v$ has $|T|\ge 2^{m'}$;
3. under the correctness property alone, $T$ is an $(\mathcal M,|T|,t)$-code.

A fourth milestone is the lemma's second sentence: when $m=\log|\mathcal M|$,

$$m' \le \log K(\mathcal M,t).$$

Significance

The result. Lemma C.1 converts any secure sketch into a code: the residual entropy $m'$ of the sketch can be no larger than the logarithm of the best $t$-error-correcting code inside a worst-case set of $2^m$ points. For uniform inputs it says $m'\le\log K(\mathcal M,t)$, so the entropy loss is at least $\log|\mathcal M|-\log K(\mathcal M,t)$. The code-offset construction built from an optimal code attains that loss, which is how the paper certifies its Hamming and set-difference constructions as optimal for uniform passwords. The companion Lemma C.2 gives the analogous bound for fuzzy extractors, up to a $-\log(1-\varepsilon)$ term. Lower bounds of this shape are what separate an efficient construction from a provably best one.

Formalizing it. The lemma has a complete, short proof in the paper; it has no machine-checked proof that we know of. The mission produces a checked version of the bound for arbitrary finite integer metrics and arbitrary randomized sketches, together with reusable definitions of min-entropy and average min-entropy on probability mass functions, of secure sketches, and of $t$-error-correcting codes in a general finite metric space.

Difficulty

The combinatorial core, that the preimage set of one sketch value is a code, is immediate from correctness. The work lies in the probabilistic bookkeeping. One must pass from an average bound on guessing probability to a single good sketch value, which requires handling sketch values of probability zero and an infinite (possibly uncountable) space of sketch outputs. One must then pass from "$\Pr[W=w\mid v]\le 2^{-m'}$ for all $w$" to "at least $2^{m'}$ points carry positive probability", and compute the min-entropy of a uniform distribution exactly. Finally the bound must be transferred to the minimum over all sets of size $2^m$, a finite but large family. A first idea, to reason only about deterministic sketches, does not suffice: Definition 3 allows randomized $\mathsf{SS}$ and $\mathsf{Rec}$, and the statement quantifies over them.

Formalization scope

Laws are Mathlib PMFs; randomized procedures are maps into PMF. The sketch value type V is arbitrary, standing in for $\{0,1\}^*$. Average min-entropy is written in the equivalent joint form $-\log\sum_b\max_a\Pr[A=a\wedge B=b]$, which avoids conditioning on null events. "Min-entropy $m$" is read as $\mathbf H_\infty(W)\ge m$, and $m, m'$ are real numbers. $\mathsf{Rec}$ is randomized and correctness asks that it return $w$ with probability one for every possible sketch value of $w$.

The explicit choices:

• $L(\mathcal M,t,m)$ is defined only when $2^m$ is a natural number $N\le|\mathcal M|$ (otherwise the minimum ranges over no sets); the goal takes such an $N$ with $(N:\mathbb R)=2^m$. The printed $K(n,t,S)$ inside the minimum is read as $K(\mathcal M,t,S)$, and the printed $L(\mathcal M,t,n)$ as $L(\mathcal M,t,\log|\mathcal M|)$.
• The code-bound statements explicitly assume all metric axioms from §2.1: zero distance exactly for equal points, symmetry, and the triangle inequality. Symmetry is used because the ball condition of a code measures $\mathrm{dis}(w',c)$, while correctness is stated for $\mathrm{dis}(c,w')$. The second-sentence milestone also assumes $\mathcal M$ nonempty, which the paper leaves implicit.
• The hypothesis is the worst-case secure sketch of Definition 3, not the average-case one of Definition 4, which would weaken the lemma.
• Definition 3's efficiency requirement is dropped; no complexity theory is formalized, and no placeholder predicate replaces it.

Two trivializing formalizations are ruled out: $K(\mathcal M,t,S)$ is the largest size of a code in $S$, not a count of codes; and a code is defined by the ball condition, not by "distinct codewords are at distance greater than $t$", which is weaker in the absence of the triangle inequality.

Needed infrastructure: the min-entropy of a uniform PMF on a finset, the averaging argument over a tsum of ENNReal values, and monotonicity of Finset.inf'. The min-entropy and code definitions are reusable by every other mission of this paper. Contributions are welcome on any milestone, in any order.

Selected references

• Y. Dodis, R. Ostrovsky, L. Reyzin, A. Smith, Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data, SIAM J. Comput. 38(1):97–139, 2008. arXiv:cs/0602007v4. https://arxiv.org/abs/cs/0602007 — DOI https://doi.org/10.1137/060651380
• A. Juels, M. Wattenberg, A Fuzzy Commitment Scheme, ACM CCS 1999. https://doi.org/10.1145/319709.319714
• R. Renner, S. Wolf, Simple and Tight Bounds for Information Reconciliation and Privacy Amplification, ASIACRYPT 2005. https://doi.org/10.1007/11593447_11

Motivation

A learning algorithm trained on a finite sample generalizes when its empirical risk on that sample is close to its risk on fresh data. Classical guarantees come from uniform convergence over the hypothesis class (VC dimension, Rademacher complexity) or from algorithmic stability, such as uniform stability (Bousquet and Elisseeff, 2002) and on-average stability (Shalev-Shwartz et al., 2010). Both families look at the class or at the algorithm's worst-case sensitivity, not at how much the trained hypothesis actually depends on the data it was trained on.

Russo and Zou (arXiv:1511.05219, 2016) bounded the bias of adaptive data analysis by mutual information, and Xu and Raginsky (arXiv:1705.07809, NIPS 2017) turned this into a generalization bound for learning algorithms: the expected generalization error is at most $\sqrt{2\sigma^2 I(S;W)/n}$, where $I(S;W)$ is the mutual information between the training sample and the output hypothesis. This bound started the line of information-theoretic generalization bounds, later refined to individual-sample mutual information (Bu, Zou and Veeravalli, 2020), conditional mutual information (Steinke and Zakynthinou, 2020) and chaining variants (Asadi, Abbe and Verdú, 2018).

Timeline:

• 2016, Russo and Zou: bias of adaptive analysis bounded by $I(\Lambda_{\mathsf W}(S);W)$, the information carried by the vector of empirical risks, for a finite hypothesis space.
• 2017, Xu and Raginsky: the bound with the input–output mutual information $I(S;W)$, for arbitrary hypothesis spaces (Theorem 1); high-probability versions and an analysis of the Gibbs algorithm.
• 2018–2020: chaining, individual-sample and conditional mutual information refinements.

Setting

There is an instance space $\mathsf Z$, a hypothesis space $\mathsf W$ and a nonnegative loss $\ell:\mathsf W\times\mathsf Z\to\mathbb R_+$, written ℓ : W → Z → ℝ in Lean. Data are drawn from an unknown probability measure $\mu$ on $\mathsf Z$; a dataset of size $n$ is an i.i.d. sample $S=(Z_1,\dots,Z_n)\sim\mu^{\otimes n}$ (sampleLaw μ n).

A learning algorithm is a Markov kernel $P_{W|S}$ (κ : Kernel (Fin n → Z) W): given the dataset, it outputs a random hypothesis $W$. The pair $(S,W)$ has joint law $P_{S,W}=\mu^{\otimes n}\otimes P_{W|S}$ (sampleLaw μ n ⊗ₘ κ), with marginals $P_S=\mu^{\otimes n}$ and $P_W$.

The population risk and the empirical risk of a hypothesis $w$ are

$$L_\mu(w)=\int_{\mathsf Z}\ell(w,z)\,\mu(dz),\qquad L_S(w)=\frac1n\sum_{i=1}^n \ell(w,Z_i)$$

(risk ℓ μ w, empRisk ℓ s w). The expected generalization error is

$$\mathrm{gen}(\mu,P_{W|S})=\mathbb E\big[L_\mu(W)-L_S(W)\big],$$

the expectation taken under $P_{S,W}$ (genError ℓ μ κ).

The mutual information of a pair $(X,Y)$ with joint law $P_{X,Y}$ is the relative entropy $I(X;Y)=D(P_{X,Y}\,\|\,P_X\otimes P_Y)\in[0,\infty]$ (mutualInfo). A real random variable $U$ is $\sigma$-subgaussian if $\log\mathbb E[e^{\lambda(U-\mathbb EU)}]\le\lambda^2\sigma^2/2$ for all $\lambda\in\mathbb R$.

Formalization targets

Goal: Theorem 1 (p. 4)

If $\ell(w,Z)$ is $\sigma$-subgaussian under $\mu$ for every $w\in\mathsf W$, then

$$\big|\mathrm{gen}(\mu,P_{W|S})\big|\le\sqrt{\frac{2\sigma^2}{n}\,I(S;W)} .$$

The statement fixes no structure on $\mathsf W$ (it may be uncountable) and no bound on the loss beyond subgaussianity.

Milestones

1. (A.1), Donsker–Varadhan (p. 11), the inequality $\int F\,d\pi-D(\pi\|\rho)\le\log\int e^F\,d\rho$. Already proved on the platform and referenced.
2. Lemma 1 (p. 3), the decoupling estimate: if $f(\bar X,\bar Y)$ is $\sigma$-subgaussian under $P_X\otimes P_Y$, then

$$\big|\mathbb E f(X,Y)-\mathbb E f(\bar X,\bar Y)\big|\le\sqrt{2\sigma^2 I(X;Y)} .$$

3. Subgaussianity of the empirical risk (§3.2, p. 4): for every $w$, $L_S(w)-L_\mu(w)$ is $\sigma/\sqrt n$-subgaussian under $\mu^{\otimes n}$.
4. The mixture step (§3.2, p. 4, corrected): under $P_S\otimes P_W$, $f(\bar S,\bar W)=L_{\bar S}(\bar W)-L_\mu(\bar W)$ is $\sigma/\sqrt n$-subgaussian with mean $0$.

Significance

The result. Theorem 1 makes generalization a property of the dependence between data and output rather than of the size of the hypothesis class. It applies to randomized algorithms on uncountable or infinite-dimensional hypothesis spaces, where uniform convergence gives nothing, and to unbounded subgaussian losses. Any mechanism that limits $I(S;W)$, such as noise injection, differential privacy, compression or relative-entropy regularization, inherits a generalization guarantee. A loss with values in $[a,b]$ is $(b-a)/2$-subgaussian for every $\mu$, so the theorem covers all bounded losses. The bound is also the template for the later refinements listed above, which share Lemma 1's decoupling argument.

Formalizing it. The result is proved on paper; no machine-checked proof is known. A formalization supplies a reusable statement of mutual information as a relative entropy of a joint law on general measurable spaces, a decoupling lemma for subgaussian functions, and the mixture argument for subgaussian families, all of which recur in the later literature. It also settles a point the paper leaves loose: the printed proof applies Lemma 1 to the uncentred empirical risk, which is not subgaussian in general; the milestones state the corrected step.

Difficulty

The two halves of the proof are short on paper, but each step that "follows" uses a fact the page does not state. The decoupling estimate needs $\mathbb E f(X,Y)$ to be finite, which holds only because finite relative entropy and exponential integrability under the product together force integrability under the joint law. The mixture step needs the moment-generating-function bound of each section $w\mapsto f(\cdot,w)$ to integrate over $P_W$, which requires joint measurability and the centring of every section at its own mean: the uncentred empirical risk $L_{\bar S}(\bar W)$ mixes laws with different means and is not subgaussian.

A natural first attempt applies Lemma 1 directly to $f(s,w)=L_s(w)$ as printed; it fails on the example $\ell(w,z)=w$ with $W$ uniform on $\{0,1\}$ and independent of $S$.

Formalization scope

• Objects. The sample law, $L_\mu$ and $L_S$ are reused from the published LearnStability.Characterization.Setting. This mission defines mutualInfo P := klDiv P (P.fst.prod P.snd) (values in $[0,\infty]$) and genError, the integral of the pointwise difference $L_\mu(w)-L_s(w)$ under sampleLaw μ n ⊗ₘ κ. Samples are Fin n → Z; the algorithm is a Markov kernel.
• Subgaussianity is Mathlib's HasSubgaussianMGF of the centred variable, whose parameter is the variance proxy: $\sigma^2$ for the loss, $\sigma^2/n$ for the empirical risk.
• Added hypotheses, all implicit on the page: $n\ge1$ (the bound divides by $n$); joint measurability of $\ell$ (so that $L_\mu(W)$ and $L_S(W)$ are random variables); and $I\ne\infty$ in Lemma 1 and Theorem 1, because Lean's conversion of $\infty$ to a real number gives $0$, which would turn the page's vacuous bound into a false claim. The page's nonnegativity of $\ell$ is kept. No integrability hypothesis on $f$ or on the losses is assumed beyond subgaussianity.
• Correction of the print. The page says that $f(\bar S,\bar W)=L_{\bar S}(\bar W)$ is $\sigma/\sqrt n$-subgaussian; milestone 4 states it for the centred $L_{\bar S}(\bar W)-L_\mu(\bar W)$, together with its mean being $0$. Equation (9) is not posed separately.
• Ruled out. The goal is stated for genError and the mutual information of the algorithm's own joint law; a version through Lemma 1's abstract pair $(\bar X,\bar Y)$, through $I(\Lambda_{\mathsf W}(S);W)$ (Theorem 2, out of scope), or with $I$ truncated to a real number would not be this theorem.
• Infrastructure. Integrability transfer from $P_X\otimes P_Y$ to $P_{X,Y}$ under finite relative entropy; sums of independent subgaussian variables on Measure.pi (Mathlib has HasSubgaussianMGF.sum_of_iIndepFun); mixtures of mean-zero subgaussian families under a product measure. These are reusable beyond this mission, and contributions of each are welcome.

Selected references

• A. Xu, M. Raginsky, Information-theoretic analysis of generalization capability of learning algorithms, NIPS 2017; arXiv:1705.07809v2. https://arxiv.org/abs/1705.07809
• D. Russo, J. Zou, Controlling bias in adaptive data analysis using information theory, AISTATS 2016. https://arxiv.org/abs/1511.05219
• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, stability and uniform convergence, JMLR 11, 2010. https://jmlr.org/papers/v11/shalev-shwartz10a.html
• O. Bousquet, A. Elisseeff, Stability and generalization, JMLR 2, 2002. https://www.jmlr.org/papers/v2/bousquet02a.html
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities, Oxford University Press, 2013 (Donsker–Varadhan, Cor. 4.15). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• A. Asadi, E. Abbe, S. Verdú, Chaining mutual information and tightening generalization bounds, NeurIPS 2018. https://arxiv.org/abs/1806.03803
• Y. Bu, S. Zou, V. Veeravalli, Tightening mutual information based bounds on generalization error, IEEE JSAIT 2020. https://arxiv.org/abs/1901.04609
• T. Steinke, L. Zakynthinou, Reasoning about generalization via conditional mutual information, COLT 2020. https://arxiv.org/abs/2001.09122

Motivation

Draw $n$ independent fair bits $X$, compute a one-bit summary $f(X)$, and send the bits through independent binary symmetric channels with crossover probability $\varepsilon$, producing $Y$. Which summary tells the receiver the most about $Y$? Kumar and Courtade conjectured that a single coordinate, $f(X)=X_1$, is optimal: $I(f(X);Y)\le 1-h_2(\varepsilon)$ bits for every Boolean $f$, in every dimension and at every noise level (ISIT 2013; IEEE Trans. Inf. Theory 2014). The Courtade–Kumar (most informative Boolean function) conjecture is a basic question about how noise destroys information on the discrete cube, connecting information theory with Boolean Fourier analysis and hypercontractivity.

This mission asks for a formal proof of a sharp contraction theorem for arbitrary randomized binary summaries, whose Boolean case is the Courtade–Kumar conjecture, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1970–1976 — Hypercontractivity on the cube (Bonami, Ann. Inst. Fourier 1970; Gross, Amer. J. Math. 1975; Beckner, Annals 1975); Mrs. Gerber's lemma (Wyner–Ziv, IEEE TIT 1973).
• 2013–2014 — Kumar and Courtade pose the conjecture and prove a coordinatewise sum bound.
• 2016 — High-noise results: Ordentlich, Shayevitz and Weinstein for balanced functions (ISIT 2016); Samorodnitsky for all Boolean functions in a dimension-independent high-noise range (IEEE TIT 2016).
• 2018 — Pichler, Piantanida and Matz prove coordinate optimality when the observation is also reduced to one bit (Ann. Appl. Probab. 2018).
• 2020–2023 — Barnes–Özgür's symmetrized reformulation (ISIT 2020); Li–Médard on fixed-mean optimizers (IEEE TIT 2021); Yu's $\Phi$-stability (PTRF 2023).
• 2025–2026 — Chen, Gohari and Nair's differential (entropy-production) approach; independent preprints announcing proofs by Chen, Gohari, Javanmard, Lin, Mirrokni, Nair and Woodruff (arXiv:2609.24931), Ky and Tran (arXiv:2609.24184), Mahdavifar and Beirami (arXiv:2609.26444), and a bias-retaining finite-noise bound by Kramer and Saglam.
• September 2026 — The OpenAI preprint (Theorems 1.1 and 1.3, Corollary 1.2, pp. 1–4).

Setting

Let $\Omega_n=\{-1,1\}^n$ with uniform measure; information is in nats unless stated. For $r\in[-1,1]$ put

$$L=\log2,\quad H(r)=-\tfrac{1+r}2\log\tfrac{1+r}2-\tfrac{1-r}2\log\tfrac{1-r}2,\quad \psi(r)=L-H(r),$$

with $0\log0=0$; $\psi^{-1}$ is the increasing branch $[0,L]\to[0,1]$. A soft channel is $u:\Omega_n\to[-1,1]$, the conditional mean of an auxiliary sign $U$ given $X$; its information is $I(u)=H(\mathbb Eu)-\mathbb EH(u)=I(U;X)$. For $\rho\in[-1,1]$ let $Y_i=X_iZ_i$ with independent signs $\mathbb EZ_i=\rho$, and let $T_\rho u(y)=\mathbb E[u(X)\mid Y=y]$, so $I(T_\rho u)=I(U;Y)$. For an interior field $g:\Omega_n\to(-1,1)$ with $m=\mathbb Eg$, the production is $D(g)=\mathbb E[\operatorname{atanh}(g)\,Ng]$ with $Ng=\frac12\sum_i(g-g\circ\mathrm{flip}_i)$; the rate $F$ is defined by $F(\psi(r))=r\operatorname{atanh}r$; $S(I)=F(I)-2I$ (zero for $I<0$); $B_m(I)=2I+(1-m^2)S\bigl(L-\frac{H(m)-I}{1-m^2}\bigr)$.

Formalization targets

Milestone: Courtade–Kumar inequality in bits (Corollary 1.2, p. 2)

For $n\ge1$, $0\le\varepsilon\le\frac12$ and every Boolean $f$ on $\{0,1\}^n$,

$$I_2(f(X);Y)\le 1-h_2(\varepsilon),$$

with equality for every coordinate $x\mapsto x_i$ and its complement.

Goal: the soft contraction package (Theorem 1.1, p. 1; Corollary 1.2, p. 2; Theorem 1.3, p. 4)

The goal OAI.SoftChannel204.fullMain is the conjunction of:

1. Theorem 1.1. For all $n$, $u:\Omega_n\to[-1,1]$, $\rho\in[-1,1]$:

$$I(T_\rho u)\le\psi\bigl(|\rho|\,\psi^{-1}(I(u))\bigr),$$

with equality for every soft coordinate $u(x)=a x_i$, $|a|\le1$; and $I(U;Y)=I(T_\rho u)$ for the joint law of $(U,Y)$. 2. Corollary 1.2. For Boolean $f$ with $m=\mathbb Ef$ and $r_m=\psi^{-1}(H(m))$: $I(f(X);Y)\le\psi(|\rho|r_m)\le\psi(|\rho|)$, strictly below $\psi(|\rho|)$ when $0<|m|<1$ and $0<|\rho|$; coordinates and their negations attain $\psi(|\rho|)$; and the bits conversion $\psi(1-2\varepsilon)/L=1-h_2(\varepsilon)$. 3. Theorem 1.3. For every interior $g$: $D(g)\ge\max\{B_m(I(g)),F(I(g))\}\ge F(I(g))$.

Significance

The result itself. It settles the Courtade–Kumar conjecture and strengthens it in two directions: to randomized summaries at fixed initial information, and to a bias-dependent bound that is strictly better for nonconstant biased outputs. Theorem 1.3 is a mean-dependent entropy-production inequality, stronger than the scalar rate needed for Theorem 1.1. Several independent proofs of the Boolean conjecture were announced in the same period; the preprint compares its production profile with that of Chen et al. in Section 8.

Formalizing it. All objects are finite sums over $\{-1,1\}^n$, so the statements are elementary to state in Lean. The proof requires an explicit three-point optimizer for a joining problem, convexity facts about $F$ and $S$ (Lemmas 2.2–2.4, pp. 5–6), dimension induction and integration along the noise semigroup. A formal proof would give a checked solution of a conjecture with several competing announced proofs, some computer-assisted.

Difficulty

The local-to-global method of Chen, Gohari and Nair needs a local inequality to pass from the two halves of the cube to the whole. The natural information-only profile $\Phi_m(I)=F(I)$ fails the corresponding local comparison for some coupled pair laws, so the induction must carry the mean $m$ as well. The preprint uses the maximum of two profiles, $B_m$ and $F$; it must solve the minimization of the joining cost exactly (Section 3), pay the interior pair with a variance-refined one-bit inequality (Lemma 4.1, p. 12), and control the common-output corners by a thinning argument (Theorem 6.1, p. 17). The linear bound $D(g)\ge2I(g)$ from the log-Sobolev inequality does not suffice; the nonlinear surplus above $2I$ is where the difficulty lies.

Formalization scope

• Cube n = Fin n → Bool, averages are finite sums divided by $2^n$, logs are natural; sign maps Bool to $\pm1$.
• psiInv is Function.invFunOn psi (Icc 0 1); since $\psi$ is strictly increasing on $[0,1]$ and $I(u)\in[0,L]$, this is the paper's branch.
• noise ρ u y = ∑ x, kernel ρ y x * u x with kernel the product of $(1\pm\rho)/2$, which is $T_\rho$. Mutual information is the finite sum over the joint table, with terms omitted where the joint probability is $0$.
• F is stated as psiInv s * artanh (psiInv s) and is only used on $[0,L)$; for interior $g$, $|m|<1$ and $0\le I(g)<H(m)\le L$, so reserve and hybrid are evaluated in their source domain.
• All results hold for every $n\ge0$; the attainment statements quantify over i : Fin n. The milestone (separate definition file) uses the crossover form with bits.

Selected references

• OpenAI, Sharp binary-information contraction on the discrete cube, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026/main.pdf
• T. A. Courtade, G. R. Kumar, Which Boolean functions maximize mutual information on noisy inputs?, IEEE Trans. Inf. Theory 60 (2014). https://doi.org/10.1109/TIT.2014.2326877
• G. R. Kumar, T. A. Courtade, Which Boolean functions are most informative?, ISIT 2013. https://doi.org/10.1109/ISIT.2013.6620221
• A. Samorodnitsky, On the entropy of a noisy function, IEEE Trans. Inf. Theory (2016). https://doi.org/10.1109/TIT.2016.2584625
• O. Ordentlich, O. Shayevitz, O. Weinstein, An improved upper bound for the most informative Boolean function conjecture, ISIT 2016. https://doi.org/10.1109/ISIT.2016.7541349
• G. Pichler, P. Piantanida, G. Matz, Dictator functions maximize mutual information, Ann. Appl. Probab. (2018). https://doi.org/10.1214/18-AAP1384
• L. Yu, On the $\Phi$-stability and related conjectures, Probab. Theory Relat. Fields (2023). https://doi.org/10.1007/s00440-023-01209-5
• A. Gohari, C. Nair, Outer bounds for multiuser settings: the auxiliary receiver approach, IEEE Trans. Inf. Theory (2022). https://doi.org/10.1109/TIT.2021.3128136
• Z. Chen, A. Gohari, A. Javanmard, et al., A proof of the most informative Boolean function conjecture, arXiv:2609.24931 (2026). https://arxiv.org/abs/2609.24931
• V. K. Ky, T. Tran, Dictators are most informative, arXiv:2609.24184 (2026). https://arxiv.org/abs/2609.24184
• H. Mahdavifar, A. Beirami, The most informative bit and beyond, arXiv:2609.26444 (2026). https://arxiv.org/abs/2609.26444
• S. G. Bobkov, P. Tetali, Modified logarithmic Sobolev inequalities in discrete settings, J. Theoret. Probab. (2006). https://doi.org/10.1007/s10959-006-0016-3

Motivation

Many security-relevant inputs are noisy and do not repeat exactly: fingerprint minutiae, iris codes, lists of personal preferences, the set of features extracted from a document. A cryptographic key derived from such an input must be reproducible from a later, slightly different reading, without storing the input itself. Dodis, Ostrovsky, Reyzin and Smith (SIAM J. Comput. 38(1), 2008; arXiv:cs/0602007) introduced secure sketches for this purpose: public helper data that lets the holder of a nearby reading recover the original exactly, while revealing as little as possible about it.

When the input is a set of features, the natural distance is the size of the symmetric difference. Juels and Sudan proposed the fuzzy vault for this setting (Des. Codes Cryptogr. 38, 2006). Section 6.2 of Dodis et al. gives a simpler, deterministic variant, the improved Juels–Sudan sketch (Construction 5), whose storage and entropy loss are both $t\log n$ for $s$-element subsets of an $n$-element universe, independent of $s$. The paper's Theorem 6.1 is the analysis of that construction. This mission formalizes it.

Setting

Laws and average min-entropy. A random variable is identified with its law. For a pair $(A,B)$,

$$\tilde H_\infty(A\mid B) = -\log_2 \sum_b \max_a \Pr[A=a \wedge B=b],$$

which equals $-\log_2 \mathbb E_{b\leftarrow B}\big[\max_a\Pr[A=a\mid B=b]\big]$, the average min-entropy of §2.4: the negative logarithm of the best probability of guessing $A$ after seeing $B$.

Secure sketches. Let $\mathcal M$ be a set with an integer-valued distance $\mathrm{dis}$. A pair of procedures $(\mathsf{SS},\mathsf{Rec})$ is an average-case $(\mathcal M,m,\tilde m,t)$-secure sketch (Definitions 3 and 4) if

1. (correctness) $\mathrm{dis}(w,w')\le t$ implies $\mathsf{Rec}(w',\mathsf{SS}(w))=w$;
2. (security) for all random variables $W$ over $\mathcal M$ and $I$ with $\tilde H_\infty(W\mid I)\ge m$, one has $\tilde H_\infty(W\mid (\mathsf{SS}(W),I))\ge\tilde m$.

The difference $m-\tilde m$ is the entropy loss.

The metric. For a finite universe $\mathcal U$ with $n=|\mathcal U|$, $\mathrm{SDif}_s(\mathcal U)$ is the set of $s$-element subsets of $\mathcal U$ with $\mathrm{dis}(w,w')=|w\triangle w'|$.

Construction 5. Identify $\mathcal U$ with a finite field $\mathcal F$ of $n$ elements and let $t\le s$.

• $\mathsf{SS}(w)$: form $p'(z)=\prod_{x\in w}(z-x)$, monic of degree $s$, and output its coefficients $a_{s-1},\dots,a_{s-t}$ of degree $s-1$ down to $s-t$.
• $\mathsf{Rec}(w',(a_{s-1},\dots,a_{s-t}))$: form $p_{\mathrm{high}}(z)=z^s+\sum_{i=s-t}^{s-1}a_iz^i$; find a polynomial $p_{\mathrm{low}}$ of degree at most $s-t-1$ that agrees with $p_{\mathrm{high}}$ on at least $s-t/2$ points of $w'$ (Reed–Solomon decoding); output the roots of $p_{\mathrm{high}}-p_{\mathrm{low}}$.

The Lean development names these charPoly, sketchCoeffs, sketch, pHigh, Step3Cond and recover, and the metric SDifS with distance sdifDist, in the namespace FuzzyExtractors.ImprovedJS.

Formalization targets

Goal: Theorem 6.1

For every finite field $\mathcal F$ with $n$ elements, all $t\le s$ and every real $m$,

$$(\mathsf{SS},\mathsf{Rec})\ \text{is an average-case}\ \big(\mathrm{SDif}_s(\mathcal F),\,m,\,m-t\log_2 n,\,t\big)\text{-secure sketch}.$$

The goal is uniform in $m$: the entropy loss $t\log n$ does not depend on the input distribution.

Milestones (the correctness half)

The paper's argument on p. 21 splits into four steps, each a milestone:

1. $p'=p_{\mathrm{high}}+q$ with $\deg q\le s-t-1$, and $p_{\mathrm{high}}=-q$ on $w$;
2. $|w\triangle w'|\le t$ implies $|w\cap w'|\ge s-t/2$, so $-q$ is a valid $p_{\mathrm{low}}$;
3. any two valid $p_{\mathrm{low}}$ coincide;
4. $\mathsf{Rec}(w',\mathsf{SS}(w))=w$ whenever $|w\triangle w'|\le t$.

A fifth, off the goal's path, records Step 2's remark that the sketch consists of the first $t$ elementary symmetric polynomials of $w$, up to sign.

The security half is the entropy bound: since $\mathsf{SS}$ takes at most $n^t$ values, $\tilde H_\infty(W\mid(\mathsf{SS}(W),I))\ge\tilde H_\infty(W\mid I)-t\log n$ (the paper cites its Lemma 3.1, which is posed in the first mission of this series and is not restated here).

Significance

The result. Theorem 6.1 gives a secure sketch for set difference whose sketch length and entropy loss are $t\log n$, which the paper shows is essentially optimal when $n\gg s$ (§6.2, via Lemma C.1 and a constant-weight code bound). It improves the original fuzzy vault, whose entropy loss the paper analyses in Appendix D and finds good only when the stored data is very large. Through the paper's generic composition with randomness extractors (Lemma 4.1), it yields fuzzy extractors for set-valued inputs in large universes, the regime of biometric feature sets.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists on Prove2Me or, to our knowledge, elsewhere. A formal proof combines three pieces of reusable infrastructure: a probabilistic layer (average min-entropy of laws on arbitrary types, and the chain-rule-type bound for a function with few values), the combinatorics of symmetric differences of equal-size sets, and the algebra of Reed–Solomon unique decoding (a low-degree polynomial is determined by its values on enough points). Each of these is useful beyond this mission.

Difficulty

No step is deep; the difficulty is in the bookkeeping. The correctness argument relies on exact degree accounting: $p_{\mathrm{high}}$ must agree with $p'$ in every coefficient of degree at least $s-t$, so that the remainder has degree at most $s-t-1$, and the uniqueness count ("two candidates agree on at least $s-t$ points") requires the threshold to be at least $s-t/2$; the paper's sentence says "more than", which does not support the argument as written. The roots of $p_{\mathrm{high}}-p_{\mathrm{low}}$ must be shown to form exactly the set $w$, with no multiplicities lost. The security half needs the average min-entropy of a joint law with a deterministic, $n^t$-valued component bounded uniformly over all auxiliary variables, including those with infinite or uncountable range, where sums are infinite sums of extended nonnegative reals.

Formalization scope

Conventions committed to in Lean:

• Laws are PMFs; the procedures are kernels M → PMF S, here deterministic (PMF.pure). Average min-entropy is the joint form above, logarithms base 2, and the auxiliary $I$ ranges over an arbitrary ι : Type (a superset of the paper's $\{0,1\}^*$), never restricted to finite types.
• The universe is the field $\mathcal F$ itself, [Field 𝔽] [Fintype 𝔽], with $n$ = Fintype.card 𝔽; the paper's "$n$ is a prime power" is then automatic.
• The paper leaves $t\le s$ implicit; every statement assumes it. No parity condition on $t$ is imposed: "at least $s-t/2$" is written $2\cdot\#\ge 2s-t$ in $\mathbb N$, which covers odd $t$.
• "Degree at most $s-t-1$" is degree < s - t, so $p_{\mathrm{low}}=0$ when $t=s$.
• The sketch is a vector in $\mathcal F^t$ indexed from $0$: entry $i$ is the coefficient of degree $s-1-i$. The storage bound $t\log n$ holds by this type and is not restated.
• $\mathsf{Rec}$ takes an arbitrary valid $p_{\mathrm{low}}$ (by choice) instead of running a decoding algorithm. The paper's "fail" output is encoded as returning $w'$, which only occurs when correctness makes no claim.
• Running time is out of scope. Theorem 6.1's clause that $\mathsf{SS}$ and $\mathsf{Rec}$ run in time polynomial in $s$, $t$ and $\log n$ is dropped, and no surrogate predicate replaces it.

A formalization that checks only correctness, drops or trivializes the entropy clause, or lets $\mathsf{Rec}$ see $w$ itself, would not be Theorem 6.1. The goal states both clauses through the definition of an average-case secure sketch, with $\mathsf{Rec}$ given only $w'$ and the sketch.

Contributions welcome: proofs of the milestones, a general lemma bounding average min-entropy loss by the logarithm of the number of sketch values (the paper's Lemma 2.2(b) and Lemma 3.1), and Reed–Solomon uniqueness lemmas stated for reuse.

Selected references

• Y. Dodis, R. Ostrovsky, L. Reyzin, A. Smith, Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data, SIAM J. Comput. 38(1):97–139, 2008. https://doi.org/10.1137/060651380 ; arXiv:cs/0602007v4, https://arxiv.org/abs/cs/0602007
• A. Juels, M. Sudan, A Fuzzy Vault Scheme, Designs, Codes and Cryptography 38(2):237–257, 2006. https://doi.org/10.1007/s10623-005-6343-z
• E. Agrell, A. Vardy, K. Zeger, Upper Bounds for Constant-Weight Codes, IEEE Trans. Inform. Theory 46(7):2373–2395, 2000. https://doi.org/10.1109/18.887851

Motivation

Cryptographic keys must be uniformly random and reproducible exactly. Many secrets people actually possess are neither: a biometric reading (an iris code, a fingerprint template), a long passphrase recalled with typos, or the correlated bits two parties obtain from a quantum channel are noisy, so two readings of the same secret differ in a few positions, and they are not uniform. Fuzzy extractors, introduced by Dodis, Ostrovsky, Reyzin and Smith (arXiv:cs/0602007; SIAM J. Comput. 38(1), 2008), turn such a secret into a nearly uniform key that can be regenerated from any sufficiently close reading, using public helper data that does not compromise the key.

The construction for the Hamming metric is the one most used in practice and in later work on biometric key derivation and physically unclonable functions. Its history is short. Juels and Wattenberg's fuzzy commitment (CCS 1999) shifted an error-correcting code onto the secret but was analysed only for uniform inputs. The syndrome of a linear code had been used for information reconciliation in quantum key agreement (Bennett, Bessette, Brassard, Salvail and Smolin, J. Cryptology 1992). Dodis et al. defined secure sketches and fuzzy extractors for arbitrary entropy distributions, introduced average min-entropy to handle side information, and proved the bound formalized here. This mission is the first of four drawn from that paper.

Setting

All logarithms are base 2. A random variable is identified with its law. For a random variable $A$, the min-entropy is $\mathbf H_\infty(A) = -\log \max_a \Pr[A=a]$. For a pair $(A,B)$, the average min-entropy of $A$ given $B$ is

$$\tilde{\mathbf H}_\infty(A\mid B) = -\log \mathbb E_{b\leftarrow B}\big[\max_a \Pr[A=a\mid B=b]\big],$$

the adversary's chance of guessing $A$ after seeing $B$, on a log scale. The statistical distance is $\mathbf{SD}(A,B)=\tfrac12\sum_v|\Pr(A=v)-\Pr(B=v)|$, and $U_\ell$ is uniform on $\{0,1\}^\ell$.

The space is $\mathcal M=\mathcal F^n$, where $\mathcal F$ is a finite additive group with $F$ elements, $f=\log F$, and $\mathrm{dis}(w,w')$ is the Hamming distance, the number of positions where $w$ and $w'$ differ. A code $C\subseteq\mathcal F^n$ with $K$ codewords is an $[n,k,2t+1]_{\mathcal F}$ code if distinct codewords are at distance at least $2t+1$; its dimension is $k=\log_F K$, so $kf=\log K$.

A secure sketch $(\mathsf{SS},\mathsf{Rec})$ is a pair of randomized procedures with $\mathsf{Rec}(w',\mathsf{SS}(w))=w$ whenever $\mathrm{dis}(w,w')\le t$. It is an average-case $(\mathcal M,m,\tilde m,t)$-secure sketch if $\tilde{\mathbf H}_\infty(W\mid(\mathsf{SS}(W),I))\ge\tilde m$ for every pair $(W,I)$ with $\tilde{\mathbf H}_\infty(W\mid I)\ge m$. A fuzzy extractor $(\mathsf{Gen},\mathsf{Rep})$ has $\mathsf{Gen}(w)=(R,P)$ with $R\in\{0,1\}^\ell$, and $\mathsf{Rep}(w',P)=R$ whenever $\mathrm{dis}(w,w')\le t$. It is an average-case $(\mathcal M,m,\ell,t,\varepsilon)$-fuzzy extractor if

$$\mathbf{SD}\big((R,P,I),(U_\ell,P,I)\big)\le\varepsilon \quad\text{whenever}\quad \tilde{\mathbf H}_\infty(W\mid I)\ge m .$$

A family $\{H_x\}_{x\in X}$ of functions into $\{0,1\}^\ell$ is universal if $\Pr_{x}[H_x(a)=H_x(b)]=2^{-\ell}$ for all $a\ne b$.

Formalization targets

Goal: Theorem 5.2 (p. 17)

For every $[n,k,2t+1]_{\mathcal F}$ code, every $m$, every $\varepsilon>0$ and every natural number

$$\ell\;\le\;m+kf-nf-2\log(1/\varepsilon)+2,$$

there is an average-case $(\mathcal F^n,m,\ell,t,\varepsilon)$-fuzzy extractor.

The sketch branch

• Lemma 2.2(b): publishing a value with at most $2^\lambda$ possibilities lowers average min-entropy by at most $\lambda$.
• Lemma 3.1: a correct sketch with at most $2^\lambda$ outputs is an average-case secure sketch with entropy loss $\lambda$.
• Lemma 4.5: the sketch for transitive metric spaces (Construction 1) loses at most $\log|\Pi|-\log\Gamma-\log K$.
• §5, p. 17: at most one word within distance $t$ of $w'$ has a given syndrome.
• Theorem 5.1: the code-offset sketch is an average-case $(\mathcal F^n,m,m-(n-k)f,t)$-secure sketch; for a linear code, the syndrome sketch is deterministic, $n-k$ symbols long, with the same loss.

The extractor branch

• Lemma 2.1 and Lemma 2.4: the leftover hash lemma and its average-case generalization, $\mathbf{SD}\big((H_X(W),X,I),(U_\ell,X,I)\big)\le\frac12\sqrt{2^{-\tilde{\mathbf H}_\infty(W\mid I)}2^\ell}$.
• Lemma 4.1 (average-case form): an average-case sketch plus an average-case strong extractor gives an average-case fuzzy extractor.
• Lemma 4.3 (average-case form): with universal hashing, any $\ell\le\tilde m-2\log(1/\varepsilon)+2$ is achievable.

Significance

Theorem 5.2 says that the only costs of tolerating $t$ Hamming errors are the redundancy of the code, $(n-k)f$ bits, and the $2\log(1/\varepsilon)$ bits that any extractor loses. Appendix C of the paper shows the redundancy term cannot be avoided for uniform inputs, so for optimal codes the construction is optimal there. The average-case form matters for composition: it remains valid when the adversary holds side information correlated with the secret, which is the situation of every protocol that uses the key afterwards or reuses the reading.

Formalizing it produces machine-checked versions of the leftover hash lemma in its average-case form, the basic calculus of average min-entropy, and the code-offset and syndrome sketches. These are the standard tools of information-theoretic cryptography, used well beyond fuzzy extraction (privacy amplification, randomness extraction, information reconciliation). All results are proved in the paper; as far as is known, none of them has a formal proof in Lean or on this platform.

Difficulty

The obvious route bounds the leakage of the sketch with min-entropy and then applies an extractor to $W$ conditioned on each sketch value. That fails: conditioned on a particular sketch value, $W$ may have far less min-entropy than average, so a worst-case extractor has nothing to work with on some values, and paying for those bad values costs an extra error term (Corollary 4.2). The average-case notions exist to avoid this loss, and the chain must be kept average-case at every step. In Lean the work is in the probability bookkeeping: computing laws of pairs and triples formed by independent coin flips, rearranging them, and bounding sums of maxima over possibly infinite auxiliary types, together with the leftover hash lemma itself, which Mathlib does not provide.

Formalization scope

Random variables are their laws, Mathlib PMFs; pairs are joint laws and randomized procedures are kernels whose coins are independent of everything else. Average min-entropy is written in the equivalent joint form $-\log\sum_b\max_a\Pr[A=a\wedge B=b]$, which needs no conditioning on null events. The auxiliary variable $I$ ranges over every type, not only finite ones. Logarithms are Real.logb 2; $\{0,1\}^\ell$ is Fin ℓ → Bool; $\mathcal F^n$ is Fin n → F with Mathlib's hammingDist.

Explicit choices:

• Efficiency is dropped. Every "efficient" and polynomial-time clause (Definitions 1–5, Lemma 4.5, Theorems 5.1 and 5.2) is omitted; there is no complexity substrate, and no vacuous predicate stands in for it.
• $\ell$ is a natural number with $\ell\le m+kf-nf-2\log(1/\varepsilon)+2$ as a real inequality; the printed $\ell$ is a real expression.
• $\varepsilon>0$ is stated wherever $\log(1/\varepsilon)$ appears.
• "Min-entropy $m$" means $\mathbf H_\infty(W)\ge m$; minimum distance $2t+1$ means at least $2t+1$; $kf=\log K$, so non-linear codes are covered.
• $\mathcal F$ is any finite additive commutative group (the paper's additive cyclic group is a special case); the syndrome is any linear map onto $\mathcal F^{n-k}$ with kernel $C$.
• Extractor domains are arbitrary finite sets with arbitrary finite nonempty seed sets, instead of $\{0,1\}^n$ and $\{0,1\}^r$.
• $\Gamma$ in Lemma 4.5 is read as "for each $w$ and $b$ there are at least $\Gamma\ge1$ permutations with $\pi(w)=b$"; symmetry of the distance is an explicit hypothesis there.
• Theorem 5.1 is stated for the code-offset and syndrome constructions themselves, not as a bare existence claim.

A trivializing formalization is ruled out: the security clause quantifies over every auxiliary type and every joint law meeting the entropy bound, $\varepsilon$ and $\ell$ are constrained exactly as in the paper, and the universal hash family is constructed inside the goal (a supporting item states that universal families exist), never assumed.

Contributions welcome: proofs of any milestone; general lemmas on PMF marginals, statistical distance and average min-entropy, which are reusable across all four missions of this paper and in other information-theoretic cryptography; and the leftover hash lemma as a standalone result.

Selected references

• Y. Dodis, R. Ostrovsky, L. Reyzin, A. Smith, Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data, SIAM J. Comput. 38(1):97–139, 2008. arXiv:cs/0602007v4. https://arxiv.org/abs/cs/0602007 , https://doi.org/10.1137/060651380
• A. Juels, M. Wattenberg, A Fuzzy Commitment Scheme, ACM CCS 1999. https://doi.org/10.1145/319709.319714
• J. L. Carter, M. N. Wegman, Universal Classes of Hash Functions, J. Comput. System Sci. 18(2):143–154, 1979. https://doi.org/10.1016/0022-0000(79)90044-8
• J. Håstad, R. Impagliazzo, L. Levin, M. Luby, A Pseudorandom Generator from any One-way Function, SIAM J. Comput. 28(4):1364–1396, 1999. https://doi.org/10.1137/S0097539793244708
• C. H. Bennett, F. Bessette, G. Brassard, L. Salvail, J. Smolin, Experimental Quantum Cryptography, J. Cryptology 5(1):3–28, 1992. https://doi.org/10.1007/BF00191318