Information Theory

Motivation

Sending classical messages through a quantum device requires choosing input states that remain distinguishable after noise. The one-shot classical capacity measures the best information rate when each channel use is signaled with a separate input state. For many channels the optimization is difficult because it ranges over all ensembles of quantum states. Fermionic systems provide a finite-dimensional setting in which the noise has a direct description on elementary operators, but the optimal signaling states still need not be obvious. Bravyi's 2005 paper isolates a family of fermionic product channels, computes the best rate from Gaussian input states for any number of qubits, and proves that this restricted rate is the full one-shot rate for one or two qubits.

Setting

The system has $n$ qubits, with computational basis indexed by bit strings $x\in\{0,1\}^n$. The Jordan–Wigner Majorana operators $c_1,\ldots,c_{2n}$ are tensor products of Pauli matrices: $c_{2j-1}$ has $Z$ on qubits before $j$, $X$ on qubit $j$, and identity afterwards; $c_{2j}$ replaces $X$ with $Y$. Their ordered monomials $c(x)=c_1^{x_1}\cdots c_{2n}^{x_{2n}}$, $x\in\{0,1\}^{2n}$, form a basis of all operators on the qubits. The paper gives these operators and their monomials in Eq. (3).

A fermionic product channel $\Phi_b$ is determined by attenuation coefficients $b_p\in[0,1]$. On each monomial it acts by $\Phi_b(c(x))=(\prod_{p:x_p=1}b_p)c(x)$, and linearity defines it on every operator. A state is a positive semidefinite matrix of trace one. For a finite ensemble of output states $\{(p_a,\rho_a)\}$, with nonnegative weights summing to one, its Holevo quantity in bits is

$$\chi= S\!\left(\sum_a p_a\rho_a\right)-\sum_a p_aS(\rho_a), \qquad S(\rho)=-\operatorname{Tr}(\rho\log_2\rho).$$

The supremum of $\chi$ over all finite ensembles of outputs of $\Phi_b$ is $C_1(\Phi_b)$. A Gaussian state has the specific form $U\rho_\lambda U^\dagger$ of Definition 1: $\rho_\lambda=2^{-n}\prod_j(I+\lambda_j Z_j)$, each $\lambda_j\in[-1,1]$, and $U=\exp(iH_2+iH_1)$ for Hermitian quadratic and linear combinations of Majorana operators. Requiring Gaussian input states gives $C_1^g(\Phi_b)$. Setting $H_1=0$ gives an even Gaussian state. These are separate classes; the even class supplies an intermediate entropy minimum. Definition 1 and Eq. (13) are on page 4.

Formalization targets

Gaussian capacity

Write $b_1^\downarrow\ge\cdots\ge b_{2n}^\downarrow$ for the coefficients in decreasing order, and let $H(t)=-t\log_2t-(1-t)\log_2(1-t)$. The main formula, Theorem 1 and Eq. (6), is

$$C_1^g(\Phi_b)=n-H\!\left(\frac{1+b_1^\downarrow}{2}\right) -\sum_{j=1}^{n-1}H\!\left(\frac{1+b_{2j}^\downarrow b_{2j+1}^\downarrow}{2}\right).$$

It holds for every $n\ge1$ and every unsorted $b\in[0,1]^{2n}$. The milestones identify the covariance and Gaussian-preservation facts, the exact even and general Gaussian minimum-output entropies, and an ensemble attaining the capacity.

Full one-shot capacity for at most two qubits

The second clause of Theorem 1 states

$$C_1(\Phi_b)=C_1^g(\Phi_b)\qquad(n\le2).$$

Thus restricting the input ensemble to Gaussian states loses no one-shot capacity in these dimensions. The paper does not prove this equality for arbitrary $n$.

Significance

The formula replaces an optimization over arbitrary finite Gaussian ensembles with binary entropies of sorted attenuation coefficients. In the one- and two-qubit cases it also settles the unrestricted one-shot optimization for this channel family. The intermediate result $C_1=n-S_{\min}$ relates signaling directly to minimum output entropy; the even-Gaussian and Gaussian minima make the distinction between the two state classes explicit. These relationships are established in Sections II–IV of the paper.

The mathematical results are proved in the 2005 paper. This mission asks for machine-checked proofs of their exact finite-dimensional statements. The definitions of bit-valued von Neumann entropy, finite output ensembles, ordered Majorana monomials, Gaussian-state predicates, and covariance matrices can support later work on fermionic channels. The submitted goal and milestones are presently proof obligations rather than claims of existing Lean proofs.

Difficulty

The channel is simple on each Majorana monomial, but the entropy of a general output state is not determined by its one- and two-point correlations. Even within the Gaussian class, optimizing only the even Gaussian states gives a different formula from optimizing all Gaussian states: linear Majorana terms change the optimum. A direct search over density matrices therefore does not expose the closed expression in Theorem 1. For the unrestricted two-qubit clause, one must also relate arbitrary states to the Gaussian class; the paper invokes a three-qubit parity result for that step. The distinctions and parity result appear in Sections III–IV.

Formalization scope

Lean represents qubit basis vectors by Fin n → Fin 2 and operators by complex matrices on that finite type. Majorana indices start at zero in Lean, so the paper's $c_{2j-1},c_{2j}$ correspond to consecutive indices $2j-2,2j-1$. The Jordan–Wigner tensor factor at coordinate $j$ acts on qubit $j$; the monomial product follows increasing Majorana index. The channel is defined on all matrices by the trace-orthogonal monomial expansion of Eq. (4), not merely on covariance matrices. Attenuations may equal zero or one. Entropies use logarithms to base two, with $0\log_2 0=0$.

Every capacity uses a real supremum over all finite normalized ensembles, with arbitrary ensemble size. The inputs are density matrices, and their channel outputs must be density matrices. The Gaussian capacity requires every input to satisfy Definition 1; Lemma 2 ensures these outputs are Gaussian too. The minimum-output quantities are real infima over their stated input classes, and the corresponding milestone theorems assert attainment. For the actual channels the relevant sets are nonempty and bounded: the maximally mixed state supplies an output state, while every Holevo quantity lies between zero and $n$. This representation rules out restricting the Gaussian ensemble to the displayed optimizing family, assuming the goal's coefficients are initially sorted, or replacing bit entropy with natural-log entropy.

The development needs finite-matrix functional calculus, positivity, matrix exponentials, permutation and singular-value reasoning, and finite ensemble entropy bounds. Contributions to those reusable layers and to the paper's covariance, Gaussian-preservation, and minimum-output results are within scope. Lemma 3 is stated in its even-Gaussian form, which its proof establishes; the displayed lemma says only “Gaussian.”

Selected references

• Sergey Bravyi, Classical capacity of fermionic product channels, arXiv preprint quant-ph/0507282v1, 2005. arXiv

Motivation

A mixed strategy assumes a player can draw from any distribution. A real player may only have a limited or imperfect source of randomness, and an opponent may observe part of it. Repeated games with bounded randomness ask how much a player can guarantee in that situation. Gossner and Vieille (2002, Games Econ. Behav. 41(2), 206–226) studied a repeated zero-sum game in which the maximizer's only source of randomness is an i.i.d. sequence she observes privately. Valizadeh and Gohari (2017) generalized this to a leaked randomness source, in which the opponent observes a correlated sequence, and characterized the long-run max-min value. This mission formalizes the next question, studied in Valizadeh and Gohari, Playing Games with Bounded Entropy: Convergence Rate and Approximate Equilibria (arXiv:1902.03676v1, 2019; published as Simulation of a Random Variable and its Application to Game Theory, Math. Oper. Res. 2021): how fast does the max-min value of the $n$-stage game approach its long-run limit?

Timeline:

• 2002, Gossner and Vieille: the long-run max-min value when Alice's private source is i.i.d. and Bob does not observe it.
• 2017, Valizadeh and Gohari: the long-run max-min value $J^{(A)}_{cav}(H(X|Y))$ with a leaked source. The same quantity bounds every $n$-stage max-min value from above (Theorem 5 of the paper, cited there and not proved).
• 2019, Valizadeh and Gohari (this paper): an explicit lower bound for the $n$-stage game (Theorem 6), which gives the rate $\sqrt{\log n}/n^{1/4}$ (Corollary 7). The tool is a one-shot simulation lemma for random mappings (Lemma 14).

Setting

Alice (maximizer) and Bob (minimizer) have finite nonempty action sets $\mathcal A$ and $\mathcal B$, and Bob pays Alice $u_{ab}$ when the actions are $(a,b)$. A joint pmf $p_{XY}$ on finite alphabets $\mathcal X\times\mathcal Y$ is publicly known. At each stage $t=1,\dots,n$ a fresh pair $(X_t,Y_t)\sim p_{XY}$ is drawn, independently of the past. Alice observes $X_t$ and Bob observes $Y_t$. Both then act, and both actions are publicly monitored.

Strategies are deterministic. Alice's stage-$t$ action is $A_t=\sigma_t(A_1,B_1,\dots,A_{t-1},B_{t-1},X_1,\dots,X_t)$, and Bob's is $B_t=\tau_t(A_1,B_1,\dots,A_{t-1},B_{t-1},Y_1,\dots,Y_t)$. Each player's only randomness is their own source. The payoff is the expected average

$$\lambda(\sigma^n,\tau^n)=\mathbb E\Big[\frac1n\sum_{t=1}^nu_{A_tB_t}\Big],$$

with the expectation taken over the i.i.d. sources.

Logarithms are base 2. $H(p)$ is the Shannon entropy and $H(X|Y)$ the conditional entropy. For $\alpha>0$, $\alpha\ne1$, $H_\alpha(p)=\frac{\alpha}{1-\alpha}\log\|p\|_\alpha$ is the Rényi entropy and $H_\alpha(X|Y)=\frac{\alpha}{1-\alpha}\log\sum_yp_Y(y)\|p_{X|Y=y}\|_\alpha$ the conditional Rényi entropy. The total variation distance is $\|p-q\|_{TV}=\frac12\sum|p-q|$.

The benchmark (Definition 4) is built in three steps:

• the security level $U^{(A)}(p_A)=\min_b\sum_ap_A(a)u_{ab}$;
• the entropy-constrained value $J^{(A)}(h)=\max\{U^{(A)}(p_A):H(p_A)\le h\}$;
• its upper concave envelope $J^{(A)}_{cav}$ on $[0,\infty)$.

Formalization targets

Goal: Theorem 6 (p. 14)

There exist $r>0$, $\beta>0$, $\gamma\ge0$ and $\mu\ge0$ with the following property. For all sequences $f_n\in\mathbb N$, $0\le g_n\le r$, $0\le h_n\le1$, there are Alice strategies $\sigma^n$ such that for all Bob strategies $\tau^n$ and all $n$,

$$\lambda(\sigma^n,\tau^n)\ge J^{(A)}_{cav}(H(X|Y))-\mu\Big(\frac1n+\frac1{f_n}+\frac{f_n}n+g_n+2^{-\frac12(\frac n{f_n}-1)h_n(\beta g_n-\gamma h_n)}\Big).\quad(10)$$

Milestones

The milestones are the results that the paper's proof (§3.3 and Appendix A) uses, in attack order:

• the total variation properties of Lemma 1;
• the second-order Taylor bounds (3)–(6) for Rényi entropies on $[1/2,2]$;
• the random-mapping estimates (A.9), (A.11) and (A.5);
• the simulation Lemma 14,

$$\sum_fp_F(f)\|p_{f(X)Y}-p_Ap_Y\|_{TV}\le\min_{\alpha\in[1,2]}2^{-(1-\frac1\alpha)(H_\alpha(X|Y)-H_{1/\alpha}(A)+2)};$$

• the block lengths (17);
• the two-point representation (18)–(19) of $J^{(A)}_{cav}(H(X|Y))$ and its degenerate cases (Lemma 16);
• Rényi additivity (24)–(25), the entropy-gap inequality (29), and the per-block bound (31).

Significance

Theorem 6 makes the convergence of the $n$-stage max-min value quantitative. With $f_n\asymp\sqrt n$ and $g_n\asymp\sqrt{\log n}/n^{1/4}$ it gives a rate of $\sqrt{\log n}/n^{1/4}$. Combined with the cited upper bound, it says how long a game must be before limited, partially leaked randomness costs Alice at most $\varepsilon$. Lemma 14 is of independent use: it bounds how well a deterministic function of one correlated source can imitate an independent random variable in total variation, and it is stated with Rényi entropies of both orders $\alpha$ and $1/\alpha$. The paper also uses it for approximate equilibria.

On formalization: none of these results has a machine-checked proof. The mission produces finite pmf-level definitions of Shannon and Rényi entropy in bits, a model of repeated games with history-dependent deterministic strategies, and the random-mapping simulation bound. The proofs exist on paper (§3.3, Appendix A). The work is to formalize them, which includes an instance of Riesz–Thorin interpolation for finite measure spaces that Mathlib does not have.

Difficulty

Alice cannot randomize at will, so the natural strategy, playing the mixed action that attains $J^{(A)}_{cav}$, is not available. She has to manufacture mixed actions from her source, and Bob's correlated observation leaks information about them. In the paper's block construction, the actions of block $i$ are a function of the previous block's source. Three steps of this argument are hard to formalize:

• Simulation bound (Lemma 14). Its proof controls an operator from $L^\alpha(\mathcal X)$ to $L^\alpha(p_F)$ at $\alpha=1$ and $\alpha=2$, then interpolates.
• Taylor control of Rényi entropies (3)–(6). The Rényi entropy must be expanded through the removable point $\alpha=1$, uniformly on $[1/2,2]$.
• Bob's adaptivity. The final payoff bound has to hold against every Bob strategy, including ones that condition on the whole history. The required conditional-independence argument is where a careless formalization would quietly restrict Bob.

Formalization scope

Conventions:

• All alphabets are finite types. $\mathcal A$ and $\mathcal B$ are nonempty.
• A pmf is a nonnegative real function summing to one. $\Delta(\mathcal A)$ is stdSimplex ℝ 𝒜.
• Logarithms are Real.logb 2, with $0\log0=0$.
• Stages and blocks are 0-based (Fin n).
• $\lambda$ is a finite sum over $(x^n,y^n)$ weighted by $\prod_tp_{XY}(x_t,y_t)$.
• $J^{(A)}$ is the supremum of $U^{(A)}$ over $\{p\in\Delta(\mathcal A):H(p)\le h\}$, which is attained for $h\ge0$. $J^{(A)}_{cav}(h)$ is the infimum of $g(h)$ over functions $g$ that are concave on $[0,\infty)$ and majorize $J^{(A)}$ there.
• The random mapping's law is $p_F(f)=\prod_xp_A(f(x))$ on the finite set of maps $\mathcal X\to\mathcal A$.

Standing readings and added hypotheses:

• "$n\in\mathbb N$" and "$f_n\in\mathbb N$" are read as $n\ge1$ and $f_n\ge1$, because (10) divides by both.
• The constants $d_2$ of (4) and (6) are replaced by existential constants in the same position, and so is the $\gamma$ of (29) and (31).
• Lemma 16 is posed as the dichotomy its proof establishes.
• (31) adds $f\le n$, the only case in which the paper's blocks are nonempty.
• The Rényi formulas are junk at $\alpha=1$, so every statement excludes that point or multiplies by $1-1/\alpha=0$.

The goal must not be trivialized:

• The constants come before the sequences $f,g,h$, the strategies and $n$. A $\mu$ chosen after $n$ would make (10) trivial.
• Alice's action reads only past actions and her own sources, and Bob ranges over all deterministic history-dependent strategies.
• The expectation is over the i.i.d. product of $p_{XY}$, not of its marginals.
• $J^{(A)}_{cav}$ is the least concave majorant, not a two-point supremum, so (18)–(19) has content.

Not posed: Theorem 31 (Riesz–Thorin), the block payoff bound of p. 24 (which rests on (32)), and the block summation (33)–(35). Contributions are welcome on all of them. The entropy, total variation and random-mapping layers can be reused for other one-shot simulation and channel-resolvability statements.

Selected references

• M. Valizadeh, A. Gohari, Playing Games with Bounded Entropy: Convergence Rate and Approximate Equilibria, arXiv:1902.03676v1, 2019. https://arxiv.org/abs/1902.03676v1 (published as Simulation of a Random Variable and its Application to Game Theory, Mathematics of Operations Research, 2021).
• M. Valizadeh, A. Gohari, Playing games with bounded entropy, arXiv:1702.05719, 2017. https://arxiv.org/abs/1702.05719
• O. Gossner, N. Vieille, How to play with a biased coin?, Games and Economic Behavior 41(2), 206–226, 2002.
• C. Beck, F. Schögl, Thermodynamics of Chaotic Systems: An Introduction, Cambridge University Press, 1995 (cited in the paper for the analysis of $H_\alpha$ in $\alpha$, §5).

Motivation

Graph alignment asks for the correspondence between the vertices of two graphs that are noisy copies of each other with hidden labels. It arises in the de-anonymization of social networks, where an anonymized friendship graph is matched against a public one (Narayanan–Shmatikov 2009), and in computational biology, where protein–protein interaction networks of related species are aligned. The standard random model is the correlated Erdős–Rényi model of Pedarsani–Grossglauser 2011, for which exact recovery thresholds are known (Cullina–Kiyavash 2016) and almost-exact recovery is known to be impossible when $nqs=O(1)$ (Cullina–Kiyavash–Mittal–Poor 2018).

Hall and Massoulié (arXiv:2007.00533) study the weaker goal of partial recovery: output a permutation that agrees with the hidden one on a constant fraction $\alpha$ of the vertices. This mission formalizes their impossibility theorem; a companion mission (II) formalizes their possibility theorem.

Setting

Fix $n$ and scalars $0\le q<s\le1$. A parent graph $G\sim G(n,q/s)$ is copied twice and each copy keeps every edge independently with probability $s$, giving graphs $G_A$ and $G_{B'}$ with adjacency matrices $A$ and $B'$. Every unordered pair $\{i,j\}$ of distinct vertices independently carries the pair $(A_{ij},B'_{ij})\in\{0,1\}^2$ with law $P$ (equation (3)):

$$p_{00}=1-2q+qs,\qquad p_{01}=p_{10}=q(1-s),\qquad p_{11}=qs .$$

Two independent edges of $G(n,q)$ have law $Q$ (equation (4)):

$$q_{00}=1-2q+q^2,\qquad q_{01}=q_{10}=q(1-q),\qquad q_{11}=q^2 .$$

The Kullback–Leibler divergence is $D(P\|Q)=\sum_{x\in\{0,1\}^2}P(x)\log\frac{P(x)}{Q(x)}$.

A hidden permutation $\pi^*$ of the vertices, drawn uniformly from the $n!$ permutations, relabels $G_{B'}$ into $G_B$: $B_{\pi^*(i)\pi^*(j)}=B'_{ij}$. An algorithm sees only $(A,B)$ and returns a permutation $\hat\pi$, possibly at random. Its quality is the overlap

$$\beta(\hat\pi,\pi^*)=\frac1n\sum_{i=1}^n\mathbf 1_{\hat\pi(i)=\pi^*(i)} .$$

The mutual information $I(\pi^*;(A,B))$ is that of the joint law of $\pi^*$ and the observation, and $M_\alpha=\max_{\pi^*}|\{\pi\mid\beta(\pi,\pi^*)\ge\alpha\}|$ counts the permutations that are $\alpha$-close to a given one, out of $M=n!$.

Formalization targets

Goal: Theorem 2.1 (p. 8)

Let $\alpha_n\in(0,1)$, bounded below by a constant $c>0$ for large $n$. If

$$\frac{D(P\|Q)}{\alpha_n}=o\Big(\frac{\log n}{n}\Big),$$

then for every sequence of algorithms,

$$\mathbb P\big[\beta(\hat\pi,\pi^*)<\alpha_n\big]\to1\qquad(n\to\infty).$$

Milestones

1. Theorem 3.1 (generalized Fano inequality): $\mathbb P[d(\hat Z,Z)>d]\ge1-\frac{I(Z;\hat X)+1}{\log(M/M_d)}$ for any Markov chain $Z\to\hat X\to\hat Z$ with $Z$ uniform.
2. Corollary 3.2: $\mathbb P(\beta(\hat\pi,\pi^*)<\alpha)\ge1-\frac{I(\pi^*;(A,B))+1}{\log(M/M_\alpha)}$.
3. Proposition 3.3: $M/M_\alpha=\Omega(\lceil n\alpha\rceil!)$.
4. Inequality (8): $I(\pi^*;(A,B))\le\mathbb E_{\pi^*}\big[D(\mathbb P((A,B)=\cdot\mid\pi^*)\,\|\,\mathcal Q)\big]$, with $\mathcal Q$ the law of two independent $G(n,q)$ graphs.
5. The display after (8), p. 13: $I(\pi^*;(A,B))\le\binom n2D(P\|Q)$.

Significance

The theorem gives a sufficient condition, in terms of a single per-pair divergence, under which no algorithm (efficient or not) recovers even a fraction $\alpha$ of the alignment. Together with the companion possibility result (Theorem 2.3: partial recovery is possible when $nqs$ exceeds an explicit constant under sparsity conditions), it brackets the partial-recovery threshold; the paper's Corollary 2.2 specializes it to $nqs=o(1)$ in the regime $n^{-k}\le q=o(n^{-1/2})$.

On the formal side, the mission produces a finite, self-contained model of correlated random graphs with a planted permutation, a generalized Fano inequality for finite hypothesis classes with an arbitrary distance, and the bound of mutual information by a product divergence. The Fano inequality and the mutual-information bounds are reusable for other information-theoretic lower bounds (community detection, planted matching, testing). The paper proves the results on paper; none of them is formalized, and no Fano inequality is proved on the platform.

Difficulty

The Fano inequality (Theorem 3.1) is cited from Lemma 20 of Banerjee–Hegde–Massoulié (2012) and not proved in the paper, and the entropy calculus it rests on is not in Mathlib in a finite, real-valued form. The counting step (Proposition 3.3) concerns rencontres numbers; the paper uses the asymptotic $D_{n,k}\sim e^{-1}n!/k!$, which is valid only for fixed $k$, while the statement needs control uniform in $k$. Bounding $I(\pi^*;(A,B))$ requires relating the conditional law of the observation, a relabelled product law, to the unlabelled reference law $\mathcal Q$ on a space of $4^{n^2}$ matrix pairs, most of which have probability zero.

A natural first idea for the goal, taking $\alpha$ arbitrary as printed, fails: if $\alpha_n=1/n$, the identity algorithm succeeds whenever $\pi^*$ has a fixed point, with probability tending to $1-e^{-1}$, even when the divergence condition holds. The argument needs $\log(M/M_\alpha)$ to grow like $n\alpha_n\log n$, which needs $\alpha_n$ bounded below.

Formalization scope

Vertices are Fin n; a vertex pair is an off-diagonal element of Sym2 (Fin n); an edge state is a Bool × Bool with first coordinate $A$, second $B'$. The probability of a configuration is the product of $P$ over pairs, and $B$ is computed through $\pi^{*-1}$. Every probability is a finite sum; logarithms are natural. Standing assumptions on the parameters are $0\le q<s\le1$ (pp. 5 and 7); the remark "we assume $s<1$" of p. 6 is not used and not imposed.

Algorithms are real stochastic kernels from the observed pair $(A,B)$ to permutations, so randomized algorithms are included and deterministic ones are the 0/1 kernels. The algorithm's argument is the observation only: it does not see $\pi^*$ or $G_{B'}$. Mutual information and Kullback–Leibler divergence are defined as finite sums (Lean's $0\cdot\log 0=0$).

Hypotheses added relative to the page, each disclosed in the item's note:

• Theorem 2.1: $\alpha_n\ge c>0$ for large $n$ (the printed statement is false for $\alpha_n\to0$ fast).
• Theorem 3.1 and Corollary 3.2: $M_d<M$ (resp. $M_\alpha<n!$), without which $\log(M/M_d)=0$ and the bound is meaningless.
• Theorem 3.1: the observation space is finite; no metric axioms on $d$ are assumed.

Proposition 3.3 reads $(n\alpha)!$ as $\lceil n\alpha\rceil!$.

Trivializing formalizations are ruled out: the algorithm cannot be given $\pi^*$ (an oracle wins) or nothing (the statement becomes empty); the little-$o$ hypothesis is a limit of a ratio, not an inequality; the configuration law is built from (3) and sums to 1, not chosen by the solver.

Infrastructure a complete development needs: finite entropy and mutual information with the chain rule and data processing; Gibbs' inequality; derangement and rencontres counts (numDerangements in Mathlib); Stirling-type lower bounds on $\log k!$. Contributions are welcome on each milestone independently; the Fano inequality is the piece with the widest reuse.

The source is the arXiv preprint v5 (13 Jan 2022); its numbering is used throughout.

Selected references

• G. Hall, L. Massoulié, Partial Recovery in the Graph Alignment Problem, arXiv:2007.00533v5, 2022; Operations Research, 2023. https://arxiv.org/abs/2007.00533
• P. Pedarsani, M. Grossglauser, On the privacy of anonymized networks, KDD 2011. https://doi.org/10.1145/2020408.2020596
• D. Cullina, N. Kiyavash, Improved achievability and converse bounds for Erdős–Rényi graph matching, SIGMETRICS 2016. https://arxiv.org/abs/1602.01042
• D. Cullina, N. Kiyavash, P. Mittal, H. V. Poor, Partial recovery of Erdős–Rényi graph alignment via k-core alignment, arXiv:1809.03553, 2018. https://arxiv.org/abs/1809.03553
• S. Banerjee, N. Hegde, L. Massoulié, The price of privacy in untrusted recommendation engines, Allerton 2012, pp. 920–927 (Lemma 20: the generalized Fano inequality); cited as [3] in the paper.
• A. Narayanan, V. Shmatikov, De-anonymizing social networks, IEEE S&P 2009. https://doi.org/10.1109/SP.2009.22
• T. M. Cover, J. A. Thomas, Elements of Information Theory, 2nd ed., Wiley, 2006. https://doi.org/10.1002/047174882X

Why this phase transition matters

Sparse recovery asks when a vector with few nonzero coordinates can be reconstructed from fewer linear measurements than unknowns. A related geometric question asks how many faces of a high-dimensional cross-polytope survive a random linear projection. The two questions meet at the same threshold: uniqueness of a minimum-one-norm solution corresponds to a face of the projected cross-polytope. For Gaussian measurement matrices this threshold was known before the work of Bayati, Lelarge and Montanari, from Donoho's face-counting analysis (Donoho 2006); the same curve was later identified as the transition of approximate message passing (Donoho, Maleki and Montanari 2009). Their 2015 paper establishes the same weak-neighborliness curve for a broader class of independent sub-Gaussian entries with a nonzero Gaussian component. The result addresses the universality question posed for these projections: does the asymptotic transition depend on the full entry distribution or only on broad features of the matrix law?

The mathematical theorem is established in that paper. This mission records its statement in Lean and leaves the machine-checked proof open. The relevant statement is Theorem 2 on page 5 of the pinned arXiv version 2, rather than a claim about every random projection without a Gaussian component.

Polytopes, faces, and random matrices

The cross-polytope $C_n$ is the unit ball for the coordinate one-norm in $\mathbb R^n$:

$$C_n=\left\{x\in\mathbb R^n:\sum_{i=1}^n|x_i|\leq1\right\}.$$

For an $m\times n$ matrix $A$, the projected polytope $AC_n$ consists of all $Ax$ with $x\in C_n$. Write $F(Q;\ell)$ for the number of nonempty faces of $Q$ whose affine dimension is $\lfloor\ell\rfloor$. The weak neighborliness level $\rho\in(0,1)$ of a random sequence $Q_n\subseteq\mathbb R^{m(n)}$ means that, for every $\xi>0$, the ratio $F(Q_n;m(n)\rho(1-\xi))/F(C_n;m(n)\rho(1-\xi))$ converges in probability to one, while the analogous ratio with $1+\xi$ converges in probability to zero. Both limits belong to the definition; the first alone would record only survival below a candidate threshold.

The matrices have $m(n)=\lfloor n\delta\rfloor$ rows for a fixed sampling ratio $\delta\in(0,1)$. Within each matrix, the entries are independent, centered, unit-variance, and sub-Gaussian with one scale factor independent of $n$. They also admit a decomposition $A(n)=\widetilde A(n)+\nu_0G(n)$, where $\nu_0>0$ and the entries of $G(n)$ are independent standard normal variables, jointly independent of $\widetilde A(n)$. The theorem imposes no independence between matrices with different values of $n$ Bayati–Lelarge–Montanari, Theorem 2.

Formalization targets

Let $\phi$ and $\Phi$ be the density and distribution function of a standard normal random variable. The paper defines its phase boundary through a positive parameter $\alpha$:

$$f_\delta(\alpha)=\frac{2\phi(\alpha)}{\alpha+2\bigl(\phi(\alpha)-\alpha\Phi(-\alpha)\bigr)},\qquad f_\rho(\alpha)=1-\frac{\alpha\Phi(-\alpha)}{\phi(\alpha)}.$$

Footnote 3 states that $f_\delta$ decreases from one to zero on the nonnegative half-line, so each $\delta\in(0,1)$ has exactly one positive parameter. The goal, Theorem 2, says that whenever $f_\delta(\alpha)=\delta$, the sequence $A(n)C_n$ has weak neighborliness $f_\rho(\alpha)$ in probability. The Lean theorem spells out this parameter relation; it does not apply an inverse function at an argument outside a proved range.

The milestone list covers the two scalar results identifying the boundary, a deterministic condition for exact recovery, and the compressed-sensing transition. With $Z$ standard normal and $u_+=\max(u,0)$, the scalar function is

$$G_\varepsilon(\alpha)=\varepsilon(1+\alpha^2)+2(1-\varepsilon)\mathbb E[(Z-\alpha)_+^2].$$

Lemma 8 gives its unique positive minimizer and its minimum value. Lemma 9 relates that minimum to both sides of the boundary. The scalar state evolution $\sigma_{t+1}^2=\mathsf F(\sigma_t^2,\alpha\sigma_t)$, with $\mathsf F(\sigma^2,\theta)=\delta^{-1}\mathbb E\{[\eta(X+\sigma Z;\theta)-X]^2\}$ and $\eta(u;\theta)=\operatorname{sign}(u)(|u|-\theta)_+$ soft thresholding, has slope $G_\varepsilon(\alpha)/\delta$ at the origin and is concave (Lemma 7). Lemma 10 shows that a two-time correlation map $\mathcal F_{\alpha,\varepsilon}$ satisfies $\mathcal F_{\alpha,\varepsilon}(Q)>Q$ on $[0,1)$. Theorem 10, cited from Bürgisser and Cucker, bounds the probability that a Gaussian-perturbed rectangular matrix has a small least singular value:

$$\mathbb P\{\sigma_N(B+\nu G)\le\nu z\}\le(a_1z)^{M-N+1}.$$

Lemma 5 gives a recovery condition based on an approximate dual certificate and singular-value bounds. Theorem 8 states that minimum-one-norm recovery succeeds with probability tending to one below the boundary and fails with probability tending to one above it Bayati–Lelarge–Montanari, pp. 39–41, 60–61.

What a formal proof would establish

The goal would certify that the same face-count transition applies to every entry law in the stated class, including laws that are not identically distributed across the matrix. The conclusion is geometric: it counts faces of an actual projected one-norm ball. The recovery milestone provides a second way to state the threshold for sparse signals. Together they make the normalization and the two sides of the transition explicit, so future variants can compare their assumptions and conclusions with a fixed formal statement.

No machine-checked proof of Theorem 2 or of the selected milestones is known. The declarations are open Lean statements over explicit definitions. A complete development would formalize the known argument in the paper, including the probabilistic estimates and the bridge from recovery probabilities to face counts. Sharper results that remove the Gaussian component would be separate theorems with their own hypotheses.

Where the difficulty lies

The count of surviving faces depends on many supports and sign patterns simultaneously. Matching means and variances of matrix entries does not make their finite-dimensional face counts equal. Likewise, controlling recovery for one fixed signal does not immediately control the fraction of all faces. Near the boundary, exact recovery also requires uniform singular-value information for many column submatrices. These are the points where elementary concentration for a single entry or a single support is insufficient. The source paper treats the geometric statement and the recovery transition under a Gaussian-component condition; a proof that silently assumes full Gaussianity would miss its universality claim.

Formalization scope

Vectors are functions on Fin n, and every one-norm is an explicit sum of absolute values. The squared Euclidean norm is a sum of coordinate squares; the default norm on Fin n → ℝ is not used for it. Face counts reuse the published Grunbaum2003.faceCount definition, with dimension $\lfloor\ell\rfloor$ for nonnegative $\ell$; negative dimensions have zero nonempty faces. The two limits in weak neighborliness use convergence in measure, which expresses convergence in probability here. The printed lower ratio has a zero denominator for $\xi>1$, so that limit is stated for $0<\xi\leq1$. Ratios at small $n$ may involve zero denominators, but the asymptotic assertion concerns arbitrarily large $n$.

Theorem 2 uses variance one and an $N(0,1)$ Gaussian component. Theorem 8 instead uses variance $1/m(n)$ and an $N(0,1/m(n))$ component, exactly as printed. Sub-Gaussianity uses Mathlib's moment-generating-function predicate for all real parameters; this is the operative two-sided reading of the paper's stated scale condition. The scalar Gaussian expectation in $G_\varepsilon$ is accompanied by an explicit integrability conclusion in Lemma 8, excluding Lean's zero value for a nonintegrable integral. The restricted least singular value is the infimum of output norms on unit column vectors. This gives zero when a wide submatrix has a kernel and is the bound needed by Lemma 5. The state-evolution map is written as a function of $\sigma^2$, and its derivative at $0$ is a right derivative. In Lemma 10 the law of $X_\infty$ is the three-atom mixture on $\{0,+\infty,-\infty\}$, with the split of the mass $\varepsilon$ between the two infinite atoms left free. The page's clause $\mathcal F'_{\alpha,\varepsilon}(1)<1$ is stated for $\alpha>\alpha_*(\varepsilon)$, since the derivative equals $1$ at $\alpha=\alpha_*$. Theorem 10 quantifies $\nu>0$ and $z>0$, which the page leaves implicit.

The random-matrix predicates require measurability, independence within each $n$, the stated marginal laws, and independence of $G(n)$ from $\widetilde A(n)$. They leave the matrix law otherwise arbitrary. The weak-neighborliness predicate contains both face-ratio limits and $0<\rho<1$; neither the goal nor a milestone defines the threshold by assuming its conclusion. A full proof needs reusable facts about Gaussian integrals, independence of finite arrays, random face counts, restricted singular values, and the relation between projected faces and unique one-norm recovery. Contributions establishing those facts or closing any of the listed theorem statements are within scope.

Selected references

• Mohsen Bayati, Marc Lelarge and Andrea Montanari, Universality in polytope phase transitions and message passing algorithms, Annals of Applied Probability 25(2), 2015. arXiv:1207.7321v2
• David L. Donoho, High-dimensional centrally symmetric polytopes with neighborliness proportional to dimension, Discrete & Computational Geometry 35, 617–652, 2006. MR2225676
• David L. Donoho, Arian Maleki and Andrea Montanari, Message-passing algorithms for compressed sensing, Proceedings of the National Academy of Sciences 106, 18914–18919, 2009. doi:10.1073/pnas.0909892106
• Peter Bürgisser and Felipe Cucker, Smoothed analysis of Moore–Penrose inversion, SIAM Journal on Matrix Analysis and Applications 31, 2769–2783, 2010. MR2740632

Motivation

A learning algorithm picks a hypothesis $W$ from a dataset $S$; its generalization error $L_\mu(W) - L_S(W)$ measures how far the empirical risk the algorithm sees is from the population risk it is judged by. Classical bounds control this error through the complexity of the hypothesis space (VC dimension, Rademacher complexity) or through the algorithm's stability. An information-theoretic approach instead controls it through how much the output reveals about the data. Russo and Zou (arXiv:1511.05219) introduced this view for adaptive data analysis, and Xu and Raginsky (arXiv:1705.07809) turned it into a general framework for learning algorithms; the framework underlies a large later literature on mutual-information and conditional-mutual-information generalization bounds.

Expected-value bounds of the form $|\mathbb E[L_\mu(W) - L_S(W)]| \le \sqrt{2\sigma^2 I/n}$ say nothing about a single run of the algorithm. A learner usually needs the error to be small with high probability. This mission formalizes Xu and Raginsky's high-probability result, Theorem 3, which gives a sample size sufficient for $|L_\mu(W) - L_S(W)| \le \alpha$ with probability at least $1-\beta$ under an information budget.

Timeline. 2016: Russo and Zou bound the expected bias of adaptively selected statistics by mutual information, for finite hypothesis classes. 2016: Bassily, Nissim, Smith, Steinke, Stemmer and Ullman (arXiv:1511.02513) introduce the "monitor technique" to convert expected bounds into high-probability bounds for differentially private and stable algorithms. 2017: Xu and Raginsky adapt the monitor technique to mutual information, obtaining Theorem 3 and its byproduct Theorem 4.

Setting

There is an instance space $\mathsf Z$ with an unknown probability measure $\mu$, a hypothesis space $\mathsf W$, and a nonnegative loss $\ell:\mathsf W\times\mathsf Z\to\mathbb R_+$. A learning algorithm is a Markov kernel $P_{W|S}$: it receives a dataset $S = (Z_1,\dots,Z_n)$ of $n$ i.i.d. draws from $\mu$ and outputs a random $W\in\mathsf W$. The joint law of data and output is $P_{S,W} = \mu^{\otimes n}\otimes P_{W|S}$.

The population risk and empirical risk of $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).$$

The empirical-risk vector is $\Lambda_{\mathsf W}(S) = (L_S(w))_{w\in\mathsf W}$. For random variables $X, Y$ with joint law $P_{X,Y}$, the mutual information is $I(X;Y) = D(P_{X,Y}\,\|\,P_X\otimes P_Y)\in[0,\infty]$, the Kullback–Leibler divergence from the joint law to the product of the marginals. The algorithm's information budget is $I(\Lambda_{\mathsf W}(S);W)\le\varepsilon$.

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$. The standing assumption is that $\ell(w,Z)$, $Z\sim\mu$, is $\sigma$-subgaussian for every $w$; a loss with values in $[a,b]$ qualifies with $\sigma = (b-a)/2$.

Formalization targets

Goal: Theorem 3

If $I(\Lambda_{\mathsf W}(S);W)\le\varepsilon$, then for any $\alpha>0$ and $0<\beta\le1$, every sample size

$$n\ \ge\ \frac{8\sigma^2}{\alpha^2}\Big(\frac{\varepsilon}{\beta}+\log\frac2\beta\Big)\quad\text{guarantees}\quad \mathbb P\big[|L_\mu(W)-L_S(W)|>\alpha\big]\le\beta,$$

the probability being under $P_{S,W}$.

Milestones

1. Lemma B.1 — $m$ independent parallel runs: $I(\Lambda_{\mathsf W}(S_1),\dots,\Lambda_{\mathsf W}(S_m);W^m)\le m\varepsilon$.
2. Lemma B.2 — for any algorithm outputting $(W,T,R)\in\mathsf W\times[m]\times\{\pm1\}$ from $m$ datasets with information at most $\varepsilon$: $\mathbb E[R(L_{S_T}(W)-L_\mu(W))]\le\sqrt{2\sigma^2\varepsilon/n}$.
3. The monitor's information (p. 12): the arg max selector $(W^*,T^*,R^*)$ of one of the $m$ runs satisfies $I(\Lambda_{\mathsf W}(S_1),\dots,\Lambda_{\mathsf W}(S_m);W^*,T^*,R^*)\le m\varepsilon+\log(2m)$.
4. (B.7) — $\mathbb E\big[\max_{t\in[m]}|L_{S_t}(W_t)-L_\mu(W_t)|\big]\le\sqrt{\tfrac{2\sigma^2}{n}(m\varepsilon+\log(2m))}$.
5. Theorem 4 — the case $m=1$: $\mathbb E|L_\mu(W)-L_S(W)|\le\sqrt{\tfrac{2\sigma^2}{n}(\varepsilon+\log 2)}$.

Significance

The result. Theorem 3 shows that a sample complexity polynomial in $1/\alpha$ and logarithmic in $1/\beta$, the same order as for a data-independent hypothesis (where Chernoff–Hoeffding gives $\frac{2\sigma^2}{\alpha^2}\log\frac2\beta$), still suffices for a data-dependent one, provided the information budget $\varepsilon$ is small relative to $\beta$. It requires only subgaussian losses, whereas the earlier high-probability bounds of differential privacy apply to bounded losses or bounded-difference functions. Since $I(\Lambda_{\mathsf W}(S);W)\le I(S;W)$, any algorithm with small input-output mutual information (the Gibbs algorithm, noisy empirical risk minimization, adaptive compositions of such) inherits the guarantee. Theorem 4 improves Russo and Zou's bound on the expected absolute error.

Formalizing it. The result is proved in the paper; to the best of current knowledge no machine-checked version exists. The mission produces a Lean statement of the theorem with the correct domain of validity (see the scope section), and its proof will require a reusable layer of measure-theoretic information theory: mutual information of joint laws, its additivity over independent pairs, the data-processing inequality, a bound by the logarithm of the number of values of a discrete variable, and the Donsker–Varadhan route from mutual information to expectations of subgaussian functions.

Difficulty

The obvious argument fails at the step from an expectation to a probability. Markov's inequality applied to Theorem 4 gives a sample size of order $\sigma^2(\varepsilon+\log 2)/(\alpha^2\beta^2)$, quadratic in $1/\beta$. A union-bound or Chernoff argument per hypothesis does not apply, because $W$ depends on $S$ and the deviation at the selected hypothesis is not a sum of independent terms. The paper's route runs $m\approx 1/\beta$ independent copies and selects the worst one; the delicate part is bounding the information the selection itself adds, which needs the chain rule and data processing for mutual information on general (non-discrete) spaces, and an expectation bound that holds uniformly over every selection rule.

Formalization scope

Lean conventions:

• $\mathsf Z$, $\mathsf W$ are measurable spaces; datasets are Fin n → Z with law Measure.pi, taken from the published LearnStability.Characterization.Setting (sampleLaw, risk, empRisk); the algorithm is a Markov kernel; the joint law is sampleLaw μ n ⊗ₘ κ.
• $\mathsf W$ is countable with measurable singletons in the deviation bounds (Lemma B.2, (B.7), Theorems 3 and 4). The paper claims its results hold "even when $\mathsf W$ is uncountably infinite" (p. 4). Under the product σ-algebra on $\mathbb R^{\mathsf W}$ this fails: with $\mathsf Z=[0,1]$, $\mu$ uniform, $\mathsf W=[0,1]^n$, $\ell(w,z)=\mathbf 1\{z\in\{w_1,\dots,w_n\}\}$ and the algorithm $W=S$, one has $I(\Lambda_{\mathsf W}(S);W)=0$ but $|L_\mu(W)-L_S(W)|=1$ always. Lemma B.1 and the monitor's information bound hold for arbitrary measurable $\mathsf W$.
• The loss is jointly measurable; $n\ge1$; $\varepsilon\ge0$; $\sigma$-subgaussianity is Mathlib's HasSubgaussianMGF of the centred loss with variance proxy $\sigma^2$.
• Mutual information is valued in $[0,\infty]$; the budget is I ≤ ENNReal.ofReal ε. Expectations of nonnegative quantities ($|\cdot|$, $\max_t$) are lower Lebesgue integrals; Lemma B.2's signed expectation is a Bochner integral whose integrand is integrable under the hypotheses.
• $[m]$ is Fin m; the sign $r\in\{\pm1\}$ is a Bool read through sgn.
• "A sample complexity of $n = \dots$" is read as $n\ge\dots$, as the proof requires.
• The monitor of milestone 3 is a Markov kernel selecting $(T^*,R^*)$ from all runs and choosing an arg max as in (B.3) almost surely; ties may be resolved randomly.

Two printed slips are corrected in the Lean and disclosed in the item notes: the proof of Lemma B.2 claims $rL_{s_t}(w)$ is $\sigma/\sqrt n$-subgaussian under the product of marginals (false; the centred version is), and (B.6) bounds the negative of the quantity in (B.4) ((B.7) is still correct).

The hypothesis is $I(\Lambda_{\mathsf W}(S);W)\le\varepsilon$, not the stronger $I(S;W)\le\varepsilon$, and the goal mentions neither the parallel copies nor the monitor; a formalization that strengthened the hypothesis, dropped the measurability of the loss (so that the law of $(\Lambda_{\mathsf W}(S),W)$ collapses to the zero measure and every mutual information is $0$), or allowed $\varepsilon<0$ would be a weaker, vacuous or false statement.

Welcome contributions: chain rule and data processing for klDiv-based mutual information, additivity over independent products, the $\log k$ bound for finitely-valued outputs, and the Donsker–Varadhan decoupling lemma; these are reusable across the series and beyond.

Selected references

• A. Xu and M. Raginsky, Information-theoretic analysis of generalization capability of learning algorithms, NIPS 2017. arXiv:1705.07809v2
• D. Russo and J. Zou, Controlling bias in adaptive data analysis using information theory, AISTATS 2016. arXiv:1511.05219
• R. Bassily, K. Nissim, A. Smith, T. Steinke, U. Stemmer and J. Ullman, Algorithmic stability for adaptive data analysis, STOC 2016. arXiv:1511.02513
• S. Shalev-Shwartz, O. Shamir, N. Srebro and K. Sridharan, Learnability, stability and uniform convergence, JMLR 11, 2010. jmlr.org

Motivation

A finite message chosen from data changes the conditional distribution of those data. In memory-constrained inference this matters directly: a learner observing a signal $S$ through exact Gaussian equations keeps a finite state $W$, and after conditioning on $W$ the rows that were used to select it are biased. An independent Gaussian matrix has the same unconditional law as those rows, but once its labels are revealed it need not leave the same information about $S$.

This preprint quantifies the cost of that replacement. For a uniform signal on the sphere and a message of entropy at most $d^2$, replacing the actual rows by fresh independent rows increases the remaining conditional information by at most $O(d)$. As an application, learners with $o(d^2)$ persistent bits need $\Omega(d\log(1/\epsilon))$ exact Gaussian observations to reach angular accuracy $\epsilon$.

Background

• 1975. Mattila's two-point averaging estimate controls projection energies by inverse distances.
• 2015–2017. Steinhardt and Duchi establish memory-dependent minimax bounds for sparse noisy regression; Raz proves branching-program time–space lower bounds for parity learning (2016) and broader discrete problems (2017).
• 2016–2017. Russo and Zou bound the bias of a selected statistic by the information used for selection; Xu and Raginsky give an information-theoretic bound on generalization via a sub-Gaussian test under the product law.
• 2019. Sharan, Sidford and Valiant prove an $\Omega(d\log r)$ sample lower bound for Gaussian regression with small uniform noise and $d^2/4$ bits at Euclidean accuracy $d^{-r}$. Dagan, Kur and Shamir prove quadratic-space lower bounds for related linear-algebra tasks.
• 2026. The OpenAI preprint Replacing Gaussian observations in memory-constrained inference (dated September 27, 2026) proves the replacement comparison and its streaming consequence. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

Let $\sigma$ be uniform probability on $S^{d-1}$, $\gamma_k$ the law of a $k \times d$ matrix with i.i.d. $N(0,1)$ entries, $H$ discrete entropy and $I(\cdot\,;\cdot\mid\cdot)$ conditional mutual information, all in nats. Put

$$m = \lfloor d/10\rfloor, \qquad \ell = \lfloor d/2\rfloor, \qquad r = \ell - m.$$

Let $S \sim \sigma$ and $A \sim \gamma_m$ be independent, and let $W$ be a countable message with an arbitrary joint law with $(S, A)$.

• In the aligned experiment, keep $(S, A, W)$ and append an independent $r$-row Gaussian matrix $C$, so the analyst sees $G_1 = (A; C)$ and $G_1 S$.
• In the independent experiment, keep $(S, W)$ and draw a fresh $\ell$-row Gaussian matrix $G_0$ independent of $(S, W)$.

In Lean (OAI.CurrentProjection), the joint law of $((S, W), A)$ is a probability measure P on (Sphere d × W) × Rows (d/10) d whose $(S, A)$ marginal is uniformSphere d ⊗ gaussianRows (d/10) d; alignedExperiment and P.fst.prod (gaussianRows ...) are the two experiments; exposedInformation is $I(S; W \mid G, GS)$ computed as a relative entropy via condKernel; shannonEntropy is $H(W)$.

Formalization targets

Goal: Theorem 4.1 (Critical-radius comparison)

There are an absolute $K$ and $d_0$ such that for $d \ge d_0$ and every such countable $W$ with $H(W) \le d^2$,

$$I_0(S; W \mid G_0, G_0 S) \le I_1(S; W \mid G_1, G_1 S) + K d .$$

Milestones

• Theorem 3.1 (mixed projection moment and exact density version): for $\ell = m + r < d - 1$, $r \ge q$, and a finite measure $\rho$ on the sphere with $\rho(B(z,t)) \le B t^\ell$ and $\rho(B(z,t)) \le D t^{d-1}$,

$$\Big[\mathbb{E}_X\big(\mathbb{E}_Z\, p_{\rho,\delta}((X;Z),(X;Z)s)\big)^q\Big]^{1/q} \le e^{Cd} B\big(1 + \log^+(D/B)\big),$$

with an exact-density version when $\rho \ll \sigma$.

• Proposition 3.2 (actual-row tilt and exact-label limit).
• Propositions 5.3 and 5.4 (one-level and two-label auxiliary-row comparisons).
• Proposition 6.1 (averaged information increase per block, hybrid route).
• Proposition 7.1 (information through a Gaussian block, fiber route) and Lemma 7.2 (two-point Gaussian fiber measure identity).

Significance

The result. Theorem 4.1 converts a statement about the actual, selection-biased rows into one about fresh rows at an additive cost of $O(d)$, which is the step that lets block-by-block information bounds be iterated along a stream. With the residual-sphere endpoint it gives the lower bound $T = \Omega(d\log(1/\epsilon))$ for learners with $o(d^2)$ bits (Theorem 8.4, Corollary 8.7). The mixed projection moment (Theorem 3.1) is a reusable estimate on exact Gaussian projections of measures with local mass control.

Formalizing it. All results are in an unrefereed preprint, with no machine-checked proofs. The streaming theorems themselves (Theorem 8.4, Theorem 8.6, Corollary 8.7) are not among the published Lean targets and remain future work.

Difficulty

Conditioning on $W$ biases $A$ in a way that depends on the unknown signal, so the two experiments have different joint laws even though their $(S, W)$ and $(S, G)$ marginals agree. A direct comparison of densities fails because the exact label density under the actual law can be large on a selection-dependent set; controlling it requires a high moment of the projected density with the row-information charge $I(A; W \mid S) \le H(W)$ entering only with coefficient $1/q$.

Formalization scope

• Signals live on Metric.sphere (0 : EuclideanSpace ℝ (Fin d)) 1 with normalized surface measure; rows are Fin k → EuclideanSpace ℝ (Fin d) with stdGaussian entries.
• Messages are countable types with measurable singletons (finite types for some milestones); entropies and informations are ℝ≥0∞-valued.
• Row counts are d/10, d/2 - d/10, d/32, d/8, d/4, d/3 as in each source statement.

The goal is not vacuous: it quantifies over all joint laws with the stated marginal and entropy bound, and the right side is finite for many of them.

Needed infrastructure: conditional mutual information for standard Borel variables, chain rules, exact density versions of Gaussian projections, local mass bounds on the sphere. Contributions toward any milestone are welcome.

Selected references

• OpenAI, Replacing Gaussian observations in memory-constrained inference, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Replacing-Gaussian-observations-in-memory-constrained-inference-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
• J. Steinhardt, J. Duchi, Minimax Rates for Memory-Bounded Sparse Linear Regression, COLT 2015. https://proceedings.mlr.press/v40/Steinhardt15.html
• 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
• 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
• D. Russo, J. Zou, Controlling Bias in Adaptive Data Analysis Using Information Theory, AISTATS 2016. https://proceedings.mlr.press/v51/russo16.html
• A. Xu, M. Raginsky, Information-theoretic analysis of generalization capability of learning algorithms, NeurIPS 2017. https://papers.nips.cc/paper_files/paper/2017/hash/ad71c82b22f4f65b9398f76d8be4c615-Abstract.html
• P. Mattila, Hausdorff Dimension, Orthogonal Projections and Intersections with Planes, Ann. Acad. Sci. Fenn. 1 (1975). https://doi.org/10.5186/aasfm.1975.0110

Motivation

Suppose an unknown unit vector $s \in S^{d-1}$ is observed through exact linear measurements $Y_j = \langle X_j, s\rangle$ with independent Gaussian rows $X_j \sim N(0, I_d)$. If every pair is kept, $d$ rows determine $s$. A learner that can keep only a bounded number of bits between measurements must compress each exact real label into a state update, and the question is how many measurements this costs for a prescribed angular accuracy $\epsilon$. Exact labels make the question delicate: a real label has no built-in bit precision, so noise-based arguments do not apply.

This preprint attacks the question through a conditional information bound for a single block of observations: how much information about $s$ can a finite message formed from $k$ exact Gaussian measurements carry, beyond what an independent Gaussian projection of $s$ (revealed only to the analyst) already reveals? Iterating such a block bound over a stream gives a memory–sample lower bound.

Timeline

• 1960. Watanabe introduces total correlation as a measure of multivariate dependence; Austin (2020) develops its chain rules on general probability spaces.
• 2015. Steinhardt and Duchi prove memory and communication lower bounds for noisy sparse linear regression.
• 2016–2017. Raz proves that learning parities requires quadratic memory or exponentially many samples, and extends the branching-program method to a large class of finite learning problems.
• 2019. Sharan, Sidford and Valiant prove an $\Omega(d\log r)$ sample lower bound for Gaussian regression with tiny uniform noise, at most $d^2/4$ bits and Euclidean accuracy $d^{-r}$, in a stated range of $r$. Dagan, Kur and Shamir prove quadratic-space lower bounds for two other linear-prediction tasks.
• 2026. Two companion OpenAI preprints treat exact observations: Memory and precision in noiseless Gaussian regression (memory $Ad^2$, backward propagation of success bounds) and Replacing Gaussian observations in memory-constrained inference. The present OpenAI preprint, Posterior replicas and conditional information in Gaussian regression (dated September 27, 2026), gives multi-replica block bounds and derives the $o(d^2)$-memory consequence. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

Let $\sigma_d$ be uniform probability on $S^{d-1}$. In a block experiment the signal $S$ has law $p = f\sigma_d$ with a Borel density $0 \le f \le L$. Independently draw a $k\times d$ standard Gaussian matrix $A$ and observe $(A, AS)$. A message $W$ with values in a finite set is drawn from a measurable Markov kernel of $(A, AS)$. Finally an $\ell \times d$ standard Gaussian matrix $B$ is drawn independently of everything. The quantity of interest is the conditional mutual information

$$I(S; W \mid B, BS),$$

in nats, and $H(W)$ denotes the Shannon entropy of the message.

A finite-state learner with $M$ bits reads pairs $(X_j, Y_j)$ once, in order, keeps a state in a set of size $2^M$, may stop at any index up to a deterministic horizon $T$, and outputs a unit vector from its terminal state, stopping index and fresh randomness only. Transitions and stopping may be arbitrary measurable randomized rules of the current state and current pair; shared randomness is independent of the signal and samples.

In Lean (OAI.PosteriorReplicas), sphereLaw d is normalized surface measure, gaussianRows d k is the product of stdGaussian, signalMessageLaw p κ is the law of $(S, W)$, sideLaw ℓ appends $(B, BS)$, conditionalInformation is the relative entropy of the joint law from the conditionally independent coupling, and messageEntropy is $H(W)$. Learners are CompletedKernelLearner d M with Markov-kernel transitions on the completed observation space, wrapped in a JointKernelExperiment over a seed space $(\Omega, \rho)$.

Formalization targets

Goal: OAI.PosteriorReplicas.source_main

The goal is the conjunction of the paper's principal statements:

• Theorem 1.1 (Gaussian replica block bound). For large $d$, with $k = 2\lfloor d/16\rfloor$, $t = k+1$, $\ell = 4k$, there is an absolute $C$ with

$$I(S; W \mid B, BS) \le \frac{H(W)}{t} + Cd + C\log(2 + \log L),$$

uniformly over the prior, $L$, and the message kernel.

• Theorem 1.2 (Uniform-prior sample lower bound). There is an absolute $c > 0$ such that for every $M(d) = o(d^2)$, eventually in $d$, every learner with uniform-prior success $\Pr\{\arccos\langle \hat S, S\rangle \le \epsilon\} \ge 2/3$, $0 < \epsilon \le 1/10$, has $T \ge c\,d\log(1/\epsilon)$.
• Theorem 3.3 (the finite equal-label measure identity) and the accompanying density-version statement for projected laws.
• The alternative block comparisons: Theorem 5.1 (distance bins), Proposition 7.5 (Haar frames), Proposition 8.1 (synthetic Gaussian route) and Proposition 9.1 (Stiefel incidence).

Significance

The result. Theorem 1.2 shows that with $o(d^2)$ persistent bits, the $d\log(1/\epsilon)$ sample scale of real-valued Kaczmarz-type methods cannot be improved for exact Gaussian measurements, under the uniform prior and with an absolute constant. Theorem 1.1 is a reusable statement in its own right: the entropy of a message is divided by a factor proportional to $d$, and the dependence on the prior density bound $L$ is only doubly logarithmic, which is what allows conditioning on rare learner states.

Formalizing it. These results appear only in an unrefereed preprint, and none has a machine-checked proof. The companion preprint Memory and precision in noiseless Gaussian regression proves a related statement for memory $Ad^2$ by a different method; the two missions share the learner model but not the block estimates. Formalizing the goal requires conditional mutual information for general (non-discrete) random variables and the exact equal-label geometry, both of which would be reusable.

Difficulty

Conditioning on one exact observation confines the signal to a lower-dimensional section of the sphere, so posterior densities with respect to $\sigma_d$ do not exist and density-based arguments fail. Bounding the information in the message by $H(W)$ alone is far too weak: a message of $d^2$ bits could then carry all relevant information. The block bound must instead account for what the analyst's independent projection already reveals, uniformly over priors with large density bounds $L$, since rare learner states produce such priors.

Formalization scope

• Vectors are EuclideanSpace ℝ (Fin d); priors are measures on the ambient space given as (sphereLaw d).withDensity f with $0 \le f \le L$.
• Messages are Markov kernels into Fin N with NeZero N; information quantities are ℝ≥0∞-valued relative entropies (klDiv), entropies use natural logarithms.
• Row counts are natural-number floors such as 2 * (d / 16), d / 8, d / 2 as in the paper.
• The streaming conjunct quantifies over all memory sequences with IsLittleO atTop M (d^2), all horizons $T$, all $0 < \epsilon \le 1/10$, all seed spaces and all JointKernelExperiments whose output kernel agrees almost surely with the run of the per-seed learner.

The goal cannot be met vacuously: block bounds are stated for every finite message kernel, and the streaming hypothesis (success at least $2/3$) is satisfiable by learners with large $T$.

A complete development needs Gaussian matrices and their projections, coarea-type identities for equal labels, conditional kernels (condKernel), relative entropy chain rules, and spherical measure estimates. Contributions that isolate one conjunct (for example Theorem 3.3 or Theorem 1.1) are welcome.

Selected references

• OpenAI, Posterior replicas and conditional information in Gaussian regression, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Posterior-replicas-and-conditional-information-in-Gaussian-regression-September-27-2026/paper.pdf
• OpenAI, Memory and precision in noiseless Gaussian regression, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/main/preprints/Memory-and-precision-in-noiseless-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: A Time-Space Lower Bound for Parity Learning, 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, 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
• S. Watanabe, Information Theoretical Analysis of Multivariate Correlation, IBM J. Res. Dev., 1960.
• T. Austin, Multi-variate correlation and mixtures of product measures, Kybernetika, 2020.