Completed

Quantum Information Statistics·Captain: mikedeng1

Shadow Tomography of Quantum States 2: Even the Classical Special Case Needs Ω(min{D, log M}/ε²) CopiesResearch Paper

Why the copy count matters

Shadow tomography asks for predictions of many specified measurements of an unknown quantum state, while using as few prepared copies of that state as possible. The requested output is a list of acceptance probabilities, not a full description of the state. A procedure might exploit the fact that these are only $M$ numbers, even when the state has dimension $D$ . The natural question is how far this saving can go. Aaronson's paper gives upper bounds and separates two sources of difficulty: one already present for ordinary probability distributions, and one arising from noncommuting quantum measurements.

This mission concerns the first source. It formalizes Theorem 16, which says that even when the state and every requested measurement are diagonal in the same basis, the number of copies must grow with $\min\{D,\log M\}/\varepsilon^2$ in the relevant asymptotic regime. In that special case, the unknown state is an ordinary distribution on $D$ outcomes. The theorem therefore puts a limit on any proposed improvement to shadow tomography that would promise fewer copies in all instances.

States, measurements, and estimates

A mixed state $\rho$ on a $D$ -dimensional system is a positive semidefinite $D\times D$ complex matrix with trace one. A two-outcome measurement is represented by an effect $E$ satisfying $0\preceq E\preceq I$ ; it accepts $\rho$ with probability $\operatorname{Tr}(E\rho)$ . When $\rho$ is diagonal, its diagonal entries are the probabilities of the $D$ basis outcomes. When $E$ is diagonal too, it specifies a randomized yes-or-no test on those outcomes. These conventions are stated in Section 3 of the paper.

Given effects $E_1,\ldots,E_M$ , a shadow-tomography strategy measures $k$ independent copies $\rho^{\otimes k}$ and outputs estimates $b_1,\ldots,b_M$ . It succeeds on $\rho$ when every estimate differs from $\operatorname{Tr}(E_i\rho)$ by at most $\varepsilon$ . The lower bound requires success probability at least $2/3$ for every diagonal mixed state. The strategy may make a joint quantum measurement on all copies and may choose its estimates from its observed outcome. This is the same measurement model used in Problem 1.

Formalization targets

Classical special-case lower bound

The goal is the classical clause of Theorem 16. There are absolute constants $c>0$ and $N_0$ such that, for $D\ge N_0$ , $\log_2 M\ge N_0$ , and $0<\varepsilon\le1/6$ , there are $M$ diagonal effects with 0/1 entries, corresponding to the known Boolean functions in Section 6.1, for which every strategy successful on all diagonal states must use

k\ge c\,\frac{\min\{D,\log_2 M\}}{\varepsilon^2}.

The hard measurements are chosen before the strategy is quantified. The statement therefore also rules out a strategy with a smaller copy count that works uniformly for all quantum states and measurements. Its constants and threshold express the $\Omega$ notation in Theorem 16, rather than specifying a numerical optimum.

Supporting targets

Four milestones come from the proof on pages 20–21: the high-probability overlap bound for independently chosen half-size subsets (Eq. (1)); the acceptance probability of a subset under its associated biased distribution; an upper bound on the mutual information between the hidden subset index and the observed samples; and the exact entropy formula with a quadratic entropy deficit. These statements expose the combinatorial and information-theoretic parts of the lower bound while leaving the goal as the paper's copy-complexity result.

What the result supplies

Theorem 16 sets a floor for shadow tomography that survives even when all operators commute. Any uniform copy bound for the full quantum task must respect this floor. The result also distinguishes the difficulty of predicting many properties of a distribution from the extra difficulty possible for noncommuting states and measurements, which the paper treats in a separate lower bound. Section 6 presents both bounds.

A complete formalization would give machine-checked statements and proofs for the finite subset construction, the entropy calculation, the information inequality, and the reduction from a successful quantum measurement procedure on diagonal states to a lower bound on $k$ . The theorem is proved on paper; these draft statements are open Lean goals and do not claim that its proof has been machine checked. The finite-distribution and information-theory infrastructure is reusable for other lower bounds based on hidden-index families.

Where the argument is delicate

Counting how many possible measurements there are does not by itself show that samples reveal enough about which distribution generated them. The lower bound needs a quantitative relation between estimation accuracy and information about a hidden index, while each individual sample carries limited information. The paper's printed overlap condition (1) is too weak for the next displayed $\varepsilon/2$ estimate: at its boundary it gives $\varepsilon$ . The milestone preserves Eq. (1) as printed; closing the goal requires the correspondingly sharper overlap fact with $N/24$ , which follows from the same type of concentration statement after adjusting its constant. The printed assertion that learning the index requires mutual information at least $\log_2 K$ is also imprecise at success probability $2/3$ ; a quantitative decoding inequality is needed. Neither incorrect display is a draft milestone.

Formalization scope

Matrices are indexed by Fin D. WildeQIT.IsDensityOperator supplies the mixed-state predicate $\rho\succeq0$ and $\operatorname{Tr}(\rho)=1$ . Diagonal states and effects use the standard matrix diagonal predicate. An effect is positive semidefinite together with its complement. The tensor power uses functions Fin k → Fin D as basis indices; at $k=0$ it is a one-by-one identity matrix. A strategy is a finite-outcome POVM on that tensor power, followed by a real estimate vector for each outcome. The output values are not restricted to $[0,1]$ : clipping them to this interval cannot worsen an estimate of a probability. No restriction to classical estimators is placed in the goal; that would change the allowed strategies before the theorem has been proved.

The asymptotic threshold excludes the one-dimensional and single-measurement corners where the claimed rate does not describe the problem. The bound $\varepsilon\le1/6$ keeps the biased distributions used on page 20 nonnegative; $\varepsilon\ge1/2$ would permit a zero-copy constant estimate. Subset milestones require even $N$ or explicitly require a half-size subset, so $N/2$ has its intended meaning. The natural logarithm appears nowhere in the lower-bound rate; entropy, mutual information, and $\log_2 M$ use base two. At zero probability the entropy convention is $0\log 0=0$ .

The finite distributions, entropy, conditional entropy, and mutual information reuse the published WildeQIT definitions. Contributions that prove the four source milestones, establish the sharper overlap fact, or supply the quantitative decoding step are welcome. The goal must retain its order of quantifiers: one hard measurement family, then every strategy, with success demanded on every diagonal state.

Selected references

Scott Aaronson, Shadow Tomography of Quantum States, arXiv preprint arXiv:1711.01053v2, 2018. Preprint.

14 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Conditional and Dynamic Convex Risk Measures II: The Conditional Entropic Risk Measure and Conditional Relative EntropyResearch Paper

Motivation

A risk measure assigns to a random financial position $X$ a capital requirement $\rho(X)$ : the amount of cash that must be added to $X$ to make it acceptable. The axiomatic theory of convex risk measures (Föllmer–Schied 2002; Frittelli–Rosazza Gianin 2002) treats this number as computed with no information beyond the model. In practice a regulator or a risk manager revises the requirement as information arrives, so the requirement becomes a random variable measurable with respect to the information available at the time of measurement. Detlefsen and Scandolo (SFB 649 Discussion Paper 2005-006; published in Finance and Stochastics 9(4), 2005, doi:10.1007/s00780-005-0159-6) develop this conditional theory: axioms, a robust representation, and a treatment of dynamic risk measurement.

The entropic risk measure is the standard example of a convex risk measure that is not coherent. It is the capital requirement of an agent with exponential utility $u_\gamma(x)=1-e^{-\gamma x}$ , and its penalty function in the robust representation is the relative entropy $\frac1\gamma H(Q\mid P)$ (Föllmer–Schied, Stochastic Finance, Example 4.60, as cited by the paper). Section 5 of the paper carries this example to the conditional setting and shows that its penalty is a conditional relative entropy. The same identity appears in dynamic entropic risk measures, exponential-utility indifference pricing and recursive utility, where one-period conditional entropic measures are composed over time.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ and a sub- $\sigma$ -algebra $\mathcal G\subseteq\mathcal F$ , the information available at the time of measurement. $L^\infty$ is the space of essentially bounded random variables and $L^\infty_{\mathcal G}$ its $\mathcal G$ -measurable part. All equalities and inequalities between random variables hold $P$ -almost surely.

A conditional convex risk measure is a map $\rho:L^\infty\to L^\infty_{\mathcal G}$ that is translation invariant ( $\rho(X+Z)=\rho(X)-Z$ for $Z\in L^\infty_{\mathcal G}$ ), monotone ( $X\le Y\Rightarrow\rho(X)\ge\rho(Y)$ ), conditionally convex ( $\rho(\Lambda X+(1-\Lambda)Y)\le\Lambda\rho(X)+(1-\Lambda)\rho(Y)$ for $\Lambda\in L^\infty_{\mathcal G}$ , $0\le\Lambda\le1$ ), and satisfies $\rho(0)=0$ .

The relevant probability models are

\mathcal P_{\mathcal G}=\{Q \text{ probability on } (\Omega,\mathcal F) : Q\ll P,\ Q(A)=P(A)\ \text{for all } A\in\mathcal G\}.

The essential supremum of a family $\mathcal X$ of $[-\infty,+\infty]$ -valued random variables is the a.s. smallest random variable that dominates every member a.s.; the essential infimum is defined symmetrically. The minimal penalty of $\rho$ is

\alpha^*(Q)=\operatorname{ess.sup}_{X\in L^\infty}\{-E_Q(X\mid\mathcal G)-\rho(X)\},\qquad Q\in\mathcal P_{\mathcal G}.

For a risk aversion $\gamma>0$ , the conditional entropic risk measure is

\rho_\gamma(X)=\frac1\gamma\log E_P\big(e^{-\gamma X}\mid\mathcal G\big),

the capital requirement for the acceptance set $A_\gamma=\{X\in L^\infty : E_P(e^{-\gamma X}\mid\mathcal G)\le1\}$ . For $Q\in\mathcal P_{\mathcal G}$ with density $\varphi=dQ/dP$ , the conditional relative entropy is

H_{\mathcal G}(Q\mid P)=E_P(\varphi\log\varphi\mid\mathcal G)\in[0,+\infty],\qquad 0\log0=0.

Formalization targets

Goal: Proposition 5.4

For every $\gamma>0$ :

\rho_\gamma(X)=\operatorname{ess.sup}_{Q\in\mathcal P_{\mathcal G}}\Big\{-E_Q(X\mid\mathcal G)-\tfrac1\gamma H_{\mathcal G}(Q\mid P)\Big\}\quad(X\in L^\infty),\qquad \alpha^*(Q)=\tfrac1\gamma H_{\mathcal G}(Q\mid P)\quad(Q\in\mathcal P_{\mathcal G}).

The first identity is representability with the minimal penalty as the penalty; the second identifies that penalty.

Milestones

(Section 5, p. 12) $\rho_\gamma$ is a conditional convex risk measure.
(Section 5, p. 12) $\rho_\gamma(X)=\operatorname{ess.inf}\{Y\in L^\infty_{\mathcal G}: X+Y\in A_\gamma\}=\operatorname{ess.inf}\{Y\in L^\infty_{\mathcal G}: E_P(e^{-\gamma X}\mid\mathcal G)\le e^{\gamma Y}\}$ .
(Proof of Proposition 5.4) $\rho_\gamma$ is continuous from above: $X_n\searrow X$ implies $\rho_\gamma(X_n)\nearrow\rho_\gamma(X)$ .
(Section 5, p. 13) For $Q\in\mathcal P_{\mathcal G}$ : $E_P(\varphi\mid\mathcal G)=1$ and $H_{\mathcal G}(Q\mid P)=E_Q(\log\varphi\mid\mathcal G)$ .
(Proof of Proposition 5.4) $\alpha^*(Q)=\frac1\gamma\operatorname{ess.sup}_{Z\in L^\infty}\{E_Q(Z\mid\mathcal G)-\log E_P(e^Z\mid\mathcal G)\}$ .
(Lemma 5.5) The conditional Donsker–Varadhan formula

\operatorname{ess.sup}_{Z\in L^\infty}\{E_Q(Z\mid\mathcal G)-\log E_P(e^Z\mid\mathcal G)\}=H_{\mathcal G}(Q\mid P),\qquad Q\in\mathcal P_{\mathcal G}.

Significance

The result gives the conditional entropic risk measure an explicit dual description: the capital requirement is a worst case over conditional models, each penalized by its conditional relative entropy. This duality is what makes entropic risk measures computable in dynamic settings. Recursive compositions of $\rho_\gamma$ over a filtration are time consistent, and their penalties add up by the chain rule for conditional relative entropy. Lemma 5.5 is also the conditional form of the Donsker–Varadhan (Gibbs) variational principle, which is used on its own in large deviations and in PAC-Bayesian bounds.

On status: the results are proved in the paper, and the unconditional versions are textbook material. Mathlib has unconditional Kullback–Leibler divergence, tilted measures, conditional Jensen's inequality and a $[0,+\infty]$ -valued conditional expectation. As far as the platform search could establish, neither the conditional relative entropy nor the conditional Donsker–Varadhan formula nor any conditional risk measure has been formalized. This mission produces the first machine-checked conditional version, with $H_{\mathcal G}$ allowed to be infinite.

Difficulty

In the unconditional case both sides of Lemma 5.5 are numbers, and the supremum is a supremum over reals. Conditionally, both sides are random variables. The supremum over the uncountable family indexed by $L^\infty$ must be taken in the essential sense, and a pointwise supremum is neither measurable nor meaningful. The conditional relative entropy can be $+\infty$ on a set of positive probability. The integrand $\varphi\log\varphi$ need not be integrable, so the usual conditional expectation of $L^1$ is not available for it, and the " $\ge$ " direction must reach an unbounded target through bounded test variables while controlling $\log E_P(e^{Z}\mid\mathcal G)$ at the same time. The ess.sup in the goal ranges over measures, not random variables, and each $E_Q(\cdot\mid\mathcal G)$ is a conditional expectation under a different measure. These are identified with $P$ -a.s. objects through the condition $Q=P$ on $\mathcal G$ .

Formalization scope

$(\Omega,\mathcal F,P)$ is a probability space (IsProbabilityMeasure P), and $\mathcal G$ is m : MeasurableSpace Ω with hm : m ≤ mΩ. Payoffs are real functions with MemLp X ⊤ P. $L^\infty_{\mathcal G}$ membership is StronglyMeasurable[m] plus MemLp ⊤. Every (in)equality between random variables is $P$ -a.e.
$\mathcal P_{\mathcal G}$ is the subtype of probability measures $Q\ll P$ with $Q(A)=P(A)$ for all $A\in\mathcal G$ . This is equality on $\mathcal G$ , not equivalence of measures.
$E_P(\cdot\mid\mathcal G)$ and $E_Q(\cdot\mid\mathcal G)$ on bounded variables are Mathlib's conditional expectations P[·|m] and Q[·|m]. Bounded variables are integrable under every $Q\ll P$ , so no junk value arises.
$\rho_\gamma$ is the paper's closed form $\frac1\gamma\log E_P(e^{-\gamma X}\mid\mathcal G)$ . The ess.inf descriptions are a milestone, and no positivity hypothesis on $X$ is imposed.
$\varphi$ is the real part of the Radon–Nikodym derivative Q.rnDeriv P. $H_{\mathcal G}(Q\mid P)$ and $E_Q(\log\varphi\mid\mathcal G)$ are generalized conditional expectations, $E(f^+\mid\mathcal G)-E(f^-\mid\mathcal G)$ , built from Mathlib's $[0,+\infty]$ -valued condLExp and valued in EReal. The negative parts are integrable, so $+\infty-(+\infty)$ never arises. In EReal, a real number minus $+\infty$ is $-\infty$ , which is how a model with infinite entropy drops out of the supremum.
Essential suprema and infima are predicates (IsEssSup, IsEssInf) on a candidate $P$ -a.e. measurable EReal-valued function. The candidate must dominate every member a.s. and lie a.s. below every a.s. upper bound.
Continuity from above means: a.s. monotone convergence $X_n\searrow X$ in $L^\infty$ implies a.s. monotone convergence $\rho(X_n)\nearrow\rho(X)$ .
$\gamma$ is a real constant with $\gamma>0$ . The random risk aversion of Remark 5.6 is not formalized.
Ruled out: defining $H_{\mathcal G}$ through the Bochner conditional expectation P[φ * log φ | m] (which returns $0$ when $\varphi\log\varphi$ is not integrable) or $\alpha^*$ through a pointwise supremum would make the goal false or vacuous, and so would stating it for an abstract convex risk measure in place of $\rho_\gamma$ . The formalization uses the extended-valued $H_{\mathcal G}$ , the essential supremum, and the explicit $\rho_\gamma$ .
The mission is self-contained. It redefines conditional convex risk measures, $\mathcal P_{\mathcal G}$ and the essential supremum in its own namespace CondConvexRisk.Entropic and does not assume the general representation theorem (Theorem 3.2). The generalized conditional expectation and the conditional Donsker–Varadhan formula are reusable beyond risk measures. Contributions are welcome on the ess.sup API (existence, upward-directed families), on conditional monotone convergence for condExp, and on the conditional Jensen step for $x\log x$ .

Selected references

S. Detlefsen, G. Scandolo, Conditional and Dynamic Convex Risk Measures, SFB 649 Discussion Paper 2005-006, Humboldt-Universität zu Berlin, 2005 (the version formalized; published in Finance and Stochastics 9(4), 2005, https://doi.org/10.1007/s00780-005-0159-6).
H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, de Gruyter, Berlin, 2002 (reference [8] of the paper).
H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6:429–447, 2002. https://doi.org/10.1007/s007800200072
M. D. Donsker, S. R. S. Varadhan, Asymptotic evaluation of certain Markov process expectations for large time, III, Comm. Pure Appl. Math. 29:389–461, 1976. https://doi.org/10.1002/cpa.3160290405

9 thms3 active usersReviewed

Completed

Active Inference Probability·Captain: ActiveInference

Free Energy Principle II: expected free energy, Markov blankets, Gaussian variational free energy, and Bayesian model reductionResearch Paper

Free Energy Principle II: expected free energy, Markov blankets, Gaussian variational free energy, and Bayesian model reduction

Motivation

Mission Free Energy Principle I published the core variational step of the free energy principle (FEP): whatever recognition density a system carries, the posterior-form variational free energy never undercuts the data's surprisal, the bound is exact at the Bayesian posterior, and equality characterizes the posterior. That mission's shared finite substrate — normalized finite laws, finite kernels, entropy/cross-entropy/KL, and the finite generative model — now exists as platform definitions in the namespace FreeEnergyPrinciple.

The Free Energy Principle II mission formalizes the four structures the FEP literature builds on top of that core, all already machine-checked in the source repository fep_lean / fep_formal (Active Inference Institute):

Expected free energy — the policy-selection functional of active inference: what a course of action is expected to cost in preference divergence and what it is expected to reveal. Its canonical decomposition [Friston et al. 2017] splits $G$ into risk (pragmatic divergence of predicted outcomes from preferences) plus ambiguity (expected entropy of outcomes given latent states), with epistemic value fixing the sign.
Markov blankets — the partition that makes a self-organizing system statable: internal states are conditionally independent of external states given the sensory-active blanket. The source development proves this at the level of Mathlib's native conditional distributions, not as a finite mutual-information proxy.
Gaussian variational free energy — the closed-form instantiation of the FEP-I bound for the exact scalar Gaussian filter, where the native Gaussian KL is exactly the squared mean error over twice the posterior variance.
Bayesian model reduction — model comparison by Bayes factors: posterior odds equal prior odds times the likelihood ratio, the multiplicative update applied whenever a reduced model is compared against the model it was reduced from [Friston & Penny 2011].

Timeline of the mathematical content this mission formalizes:

2006/2010 — Friston's free energy principle: variational free energy as the quantity a self-organizing system minimizes (formalized in FEP-I).
2011 — Friston & Penny, Post hoc Bayesian model selection: Bayesian model reduction — evidence of reduced models evaluated by the free-energy difference; comparison by Bayes factors.
2015 — Friston, Rigoli, Sengupta, Pezzulo — the Markov-blanket partition (sensory/active states) as the geometry of the FEP.
2017 — Friston, FitzGerald, Rigoli, Schwartenbeck, Pezzulo, Active inference: a process theory: expected free energy $G(\pi) = \text{risk} + \text{ambiguity}$ drives policy selection.
2022 — Parr, Pezzulo, Friston, Active Inference (MIT Press): Gaussian treatments of filtering and the posterior-form free energy as the working equations.
2026 — fep_formal (Active Inference Institute): a machine-checked Lean 4 catalogue of 155 FEP topics compiled with zero proof holes against a pinned Mathlib. This mission transcribes the proved modules behind expected free energy, native Markov blankets, the scalar Gaussian filter/VFE, and Bayesian model reduction onto the platform.

Setting

Two carriers, both fully machine-checked in the source repository:

Finite (reusing FEP-I's published substrate). Laws are normalized real mass functions on finite types; kernels are normalized rows. This mission's expected-free-energy, model-reduction, and Markov-blanket families import the published Definitions.Def_fep_finite_laws, Def_fep_finite_information, and Def_fep_generative_model — no substrate is re-published. Zero-mass atoms are handled by the same totalized conventions as FEP-I: entropy uses Real.negMulLog (so $0\log 0 = 0$ exactly), KL is the nonnegative klFun integrand, and division premises are explicit.
Native Gaussian (self-contained on Mathlib). The Gaussian family is Mathlib's own gaussianReal/gaussianPDF at a fixed strictly positive variance; the scalar OU prediction and the closed filter update give the posterior mean/variance the recognition family varies over. The native KL between two family members is exactly $\frac{(\mu_1-\mu_2)^2}{2v}$ — proved against Mathlib's log-likelihood-ratio definition.

The four definition items of this mission package exactly these carriers:

Def_fep2_expected_free_energy — the predicted state-outcome joint, preference risk, likelihood ambiguity, epistemic value, pragmatic cost, expected free energy (epistemic sign fixed by definition), the full-support contract, and the marginal/product/conditional-entropy/mutual-information lemmas the decomposition needs. Imports FEP-I.
Def_fep2_gaussian_vfe — fixed-variance Gaussian family with its exact KL, scalar OU parameters, the exact scalar Gaussian filter (prediction, observation kernel, gain, closed posterior, evidence law), evidence surprisal, and the posterior-form Gaussian variational free energy. Self-contained.
Def_fep2_bayesian_model_reduction — posterior odds, Bayes factor, and the model-odds update $odds \leftarrow odds \times Z_f/Z_r$ , with totalized division boundaries kept explicit. Imports FEP-I.
Def_fep2_native_blanket — the static blanket factorization, the Dirac-mass embedding of finite laws into native measures, blanket/internal/external coordinates, the conditional-pair kernel, and the marginal/composition identifications the independence proof needs. Imports FEP-I.

Formalization targets

Goal: expected free energy decomposes into risk plus ambiguity

For every finite generative model, every policy $\pi$ , and every model with full support:

G[\pi] \;=\; \mathrm{KL}\big(P(o\mid\pi)\,\|\,C\big) \;+\; \sum_s P(s\mid\pi)\,H\big(A[\cdot\mid s]\big).

The epistemic-value sign is fixed by definition ( $G[\pi] =$ pragmatic cost $-$ epistemic value); the decomposition follows from two entropy identities: epistemic value $I(s;o\mid\pi)$ is predicted outcome entropy minus ambiguity, and risk is cross-entropy minus the same entropy (Gibbs' inequality under full reference support). Nonnegativity of $G$ follows as a corollary — but the decomposition, not the bound, is the target.

Gaussian variational free energy in closed form

For the exact scalar Gaussian filter, the posterior-form variational free energy at recognition mean $\mu$ is

F[\mu] = \frac{(\mu - m^*)^2}{2v^*} + S(o),

the exact fixed-variance Gaussian KL (the recognition-to-posterior gap) plus the density-relative evidence surprisal. Equality with the surprisal holds exactly at the posterior mean — the Gaussian analogue of FEP-I's exactness theorem.

Odds recursion of Bayesian model reduction

Bayes' rule in odds form: at positive evidence,

\frac{P(h_f\mid e)}{P(h_r\mid e)} = \frac{P(h_f)}{P(h_r)}\cdot\frac{P(e\mid h_f)}{P(e\mid h_r)},

with the reference prior mass and reference likelihood as exact division premises. The multiplicative Bayes-factor structure (topic fep-120: factorized evidence ratios multiply; sequential model-odds updates agree with one update by product evidence) is available from the same definition layer as a further target.

Native Markov blanket conditional independence

The embedded static blanket factorization satisfies Mathlib's native CondIndepFun predicate: internal coordinates are conditionally independent of external coordinates given the blanket coordinate. The result is obtained by identifying the authored finite conditional kernels with Mathlib conditional distributions (the embedding preserves marginals and joints exactly on discrete carriers) — not by a finite mutual-information argument.

Significance

These four results are the load-bearing extensions of FEP-I's bound: expected free energy converts the variational principle into a theory of action selection; Markov blankets make "internal states" and "external states" well-defined relative to a blanket, which is what lets the FEP talk about self-organizing systems at all; the Gaussian filter is the tractable regime in which the variational machinery becomes the Kalman update; and Bayesian model reduction is the learning/comparison step that updates structure, not just parameters.

Formalizing them. All four families are proved with zero proof holes in the source repository, against a pinned Mathlib; the definition layer here is faithful (same carriers, same totalized conventions, same support contracts made explicit) and every item below compiles locally against the platform environment. The mission's value is reusable community infrastructure: the definition items publish the EFE layer, the Gaussian filter, the odds layer, and the native-blanket embedding in the shared namespace FreeEnergyPrinciple, so later missions (policy trees, collective inference, predictive coding) can import them instead of re-deriving. Status honesty: all eight items below are formalized and machine-checked locally against the platform environment; each is an open problem on the platform only in the sense that no proof has yet been submitted to it.

Difficulty

The EFE decomposition looks like an algebraic rearrangement but the sign conventions are load-bearing: the epistemic value enters $G$ with a minus sign, and the two helper identities (epistemic value = outcome entropy $-$ ambiguity; risk = cross-entropy $-$ outcome entropy) both hold only under the full-support contract, which the definition makes explicit rather than hiding in a carrier.
The Gaussian identity requires the exact native KL between Gaussian laws — the proof goes through Mathlib's log-likelihood-ratio definition and the Gaussian first moment — and the closed-form update's positivity (positive prediction variance, positive innovation variance) is what makes the recognition family genuine rather than degenerate.
The odds recursion is a field-simp identity, but the premises are the point: a plausible rendering that hides division by zero behind totalized division changes the statement.
The blanket theorem is the most intricate item: it must transport a finite factorization through the Dirac-mass embedding into Mathlib's conditional-distribution machinery, with nonemptiness premises for the conditional distributions to exist. A "proof" via finite mutual information would prove something weaker than the source.

Formalization scope

Committed conventions of this mission's Lean development:

The expected-free-energy and model-reduction families reuse the published Free Energy Principle I finite substrate (namespace FreeEnergyPrinciple, definitions Def_fep_finite_laws, Def_fep_finite_information, Def_fep_generative_model); this mission adds definition items Def_fep2_expected_free_energy, Def_fep2_gaussian_vfe, Def_fep2_bayesian_model_reduction, and Def_fep2_native_blanket, all in the same namespace.
The Gaussian family is deliberately native: Mathlib gaussianReal/gaussianPDF, no finite substrate, no manifold geometry, no singular (zero-variance) branch.
Totalized real division boundaries (zero evidence, zero reference mass) are stated, never silently absorbed.
The natural-gradient / dynamic-flow layer of the source's Gaussian module (natural gradient flow, strict descent away from the posterior) is deliberately left out of this mission and is a natural extension target; likewise the row-wise dynamical blanket theorem (every authored factorized transition row preserves the native blanket conditional independence), which follows directly from the static theorem via the source's nextStaticModel construction.
Contributions welcome: the epistemic/pragmatic ENNReal balance (catalogue topic fep-021) onto this substrate, the treewise EFE decomposition (fep-133), Bayes-factor multiplicativity (fep-120), and blanket nonvacuity witnesses.

Selected references

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

8 thms3 active usersReviewed

Completed

Mathematical Physics·Captain: Lucas

Boltzmann Constant: Kinetic Theory, Boltzmann Factors and EntropyTextbook

Motivation

The Boltzmann constant $k_B$ is the proportionality factor relating the average thermal energy of the particles of a system to its thermodynamic temperature. It appears wherever a microscopic energy has to be compared with a macroscopic temperature: in the ideal gas law written per molecule, in the equipartition theorem, in the Boltzmann factor $e^{-E/k_BT}$ that governs equilibrium occupation probabilities, in Boltzmann's entropy formula $S = k\log W$ , in the thermal voltage of a $p$ – $n$ junction, and in the Johnson noise of a resistor.

The constant also has an unusual documentary history. Boltzmann linked entropy and probability in 1877 but never introduced a constant; Max Planck first wrote $k$ , and gave the first numerical value ( $1.346\times10^{-23}$ J/K, about 2.5% below the modern figure), in his 1900–1901 derivation of the black-body law — the terse $S = k\log W$ on Boltzmann's tombstone is Planck's formulation. For most of the twentieth century $k_B$ was a measured quantity; the 2017 acoustic gas thermometry campaign reached a relative uncertainty of 0.2 ppm, and as part of the 2019 revision of the SI the constant was defined to the exact value $1.380649\times10^{-23}$ J·K⁻¹, which is now what fixes the kelvin.

This mission formalizes the elementary quantitative content of that picture: the identities that make $k_B$ a conversion factor, and the exact arithmetic that the 2019 SI definitions make possible.

Setting

Work throughout with real numbers; units are carried in the prose, not in the types. Fix the exact post-2019 SI values

k_B = 1.380649\times10^{-23}\ \mathrm{J\,K^{-1}}, \qquad N_A = 6.02214076\times10^{23}\ \mathrm{mol^{-1}}, \qquad q = 1.602176634\times10^{-19}\ \mathrm{C},

and define the molar gas constant as the product $R = k_B N_A$ .

A gas sample is described by its pressure $p$ , volume $V$ , absolute temperature $T$ , amount of substance $n$ , molecule count $N = nN_A$ , particle mass $m$ , and mean square particle speed $\langle v^2\rangle$ . A system with a finite set $s$ of microstates is described by an energy function $E : s \to \mathbb{R}$ ; its partition function is $Z = \sum_{i\in s} e^{-E_i/(k_BT)}$ and its Boltzmann probabilities are $P_i = e^{-E_i/(k_BT)}/Z$ . For a distribution $p$ on $s$ , the Gibbs entropy is $S = -k_B\sum_i p_i\log p_i$ , the Shannon entropy (in nats) is $-\sum_i p_i\log p_i$ , and for $W$ equiprobable microstates Boltzmann's entropy is $k_B \log W$ . The thermal voltage is $V_T(T) = k_BT/q$ . All logarithms are natural.

Target

The goal theorem is the statement that fixes the physical meaning of $k_B$ : kinetic theory plus the per-molecule gas law determine the mean translational kinetic energy. From

pV = \tfrac{1}{3}Nm\langle v^2\rangle \qquad\text{and}\qquad pV = Nk_BT

conclude

\tfrac{1}{2}m\langle v^2\rangle = \tfrac{3}{2}k_BT, \qquad v_{\mathrm{rms}} = \sqrt{3k_BT/m}.

The milestones are the surrounding identities, in the order of the source: the equivalence $pV = nRT \iff pV = Nk_BT$ ; equipartition, $\tfrac{1}{2}m\langle v_x^2\rangle = \tfrac{1}{2}k_BT$ per degree of freedom; the ratio law $v_{\mathrm{rms}}(m_1)/v_{\mathrm{rms}}(m_2) = \sqrt{m_2/m_1}$ ; normalisation of the Boltzmann factors, $\sum_i P_i = 1$ ; the reduction of the Gibbs entropy on the uniform distribution to $S = k_B\log W$ ; the identification $S/k_B =$ Shannon entropy; the energy $k_BT$ of one nat of rescaled entropy; and three numerical facts — $V_T(300\ \mathrm{K}) \approx 25.85$ mV, $k_B \approx 8.617333262\times10^{-5}$ eV/K, and the exact value $R = 8.31446261815324$ J·K⁻¹·mol⁻¹.

Significance

The results. Individually these are the standard first facts of kinetic theory and statistical mechanics; together they pin down what the constant does. The equipartition chain converts a temperature into a velocity distribution scale and explains the measured room-temperature rms speeds from helium (about 1370 m/s) to xenon (about 240 m/s). The entropy statements make precise the claim that thermodynamic entropy is Shannon entropy in energy units, with $k_B$ as the exchange rate — the statement behind the natural-unit convention $k_B = 1$ . The numerical milestones exercise the consequence of the 2019 SI revision that unit conversions involving $k_B$ are now exact rational arithmetic rather than propagated measurement uncertainty.

Formalizing them. All of these are settled physics; nothing here is open. What the mission produces is a small, reusable Lean development of the SI defining constants and of the elementary statistical-mechanical vocabulary (Boltzmann weights, partition function, Gibbs/Shannon/Boltzmann entropies), with each textbook identity stated against that shared model rather than re-derived ad hoc. It is a suitable entry-level mission and a foundation other physics missions can import.

Difficulty

The mathematics is elementary; the difficulty is entirely one of faithful modelling, and solvers should expect the friction to be there rather than in the proofs. Three specific points. First, Lean's division and logarithm are total: $e^{-E/(k_BT)}$ is defined at $T = 0$ and evaluates to $1$ , and $\log x = 0$ for $x \le 0$ , so statements must carry the positivity hypotheses that keep them physically meaningful rather than relying on the definitions to exclude bad inputs. Second, the entropy definitions are stated for an arbitrary real-valued weight function, not for a distribution; normalisation is a hypothesis where it is needed, never an assumption baked into the type. Third, the numerical milestones are claims about specific decimal numerals, and the tolerance in each is part of the statement: two of them are genuine approximations and one, the value of $R$ , is an exact identity, which is only true because both factors are exact SI numerals.

Formalization scope

Quantities are real numbers (ℝ); no dimensional-analysis layer is used, and unit correctness is a convention of the prose. Finite state spaces are Finsets over an arbitrary index type, with nonemptiness stated as a hypothesis where the partition function must be nonzero. Entropies use the natural logarithm, so they are measured in nats, and the Shannon entropy is the Gibbs entropy divided by $k_B$ by construction. Temperatures, masses, volumes and particle counts are positive reals where the physics requires it. The mean square speed is a free real variable constrained only by the stated equations; it is not built from a velocity distribution, and extending the development to an actual Maxwell–Boltzmann distribution is out of scope here and a natural follow-up mission.

The statements are deliberately non-vacuous: every hypothesis set in the mission is satisfiable (positive temperature, positive mass, nonempty state space), and the numerical items admit no trivializing reading since they are closed claims about fixed numerals. Only Mathlib is required — Real.exp, Real.log, Real.sqrt, and Finset.sum. The definition file is intended to be reusable: any later mission about thermodynamics, black-body radiation, or the Shockley diode equation can import the SI constants and entropy vocabulary unchanged.

Selected references

Wikipedia, Boltzmann constant — the source text this mission formalizes: https://en.wikipedia.org/wiki/Boltzmann_constant
D. B. Newell and E. Tiesinga (eds.), The International System of Units (SI), NIST Special Publication 330 (2019). DOI: https://doi.org/10.6028/NIST.SP.330-2019 — the exact defining values of $k_B$ , $N_A$ and $q$ .
M. Planck, "Ueber das Gesetz der Energieverteilung im Normalspectrum", Annalen der Physik 309(3):553–563 (1901). DOI: https://doi.org/10.1002/andp.19013090310 — the first introduction of $k$ and of $S = k\log W$ .
R. P. Feynman, R. B. Leighton and M. Sands, The Feynman Lectures on Physics, Vol. I, ch. 39 (kinetic theory of gases): https://www.feynmanlectures.caltech.edu/I_39.html

12 thms3 active usersReviewed

Quantum Information·Captain: mikedeng1

An Intuitive Proof of the Data Processing Inequality: Conditional von Neumann Entropy Cannot Increase Under Partial Trace, via the Smooth Min-Entropy DPI and the Quantum AEPResearch Paper

Motivation

The data processing inequality (DPI) for the conditional von Neumann entropy says that discarding part of the side information cannot make a quantum system less uncertain: for every tripartite state $\rho_{ABC}$ ,

H(A|BC)_\rho \le H(A|B)_\rho .

It is equivalent to strong subadditivity of the von Neumann entropy, proved by Lieb and Ruskai in 1973 (Lieb–Ruskai), and it underlies most of quantum Shannon theory: the converse bounds of channel coding, the monotonicity of mutual information under local operations, and the security analysis of quantum key distribution all reduce to it. The known proofs rest on operator convexity (Lieb's concavity theorem) or on other non-elementary matrix analysis.

Beaudry and Renner (arXiv:1107.0740v2, Quantum Inf. Comput. 12 (2012) 432) give a proof that avoids operator convexity entirely. It first proves the DPI for a one-shot quantity, the smooth min-entropy, where it follows almost directly from the definition, and then recovers the von Neumann statement through the quantum asymptotic equipartition property (QAEP) of Tomamichel, Colbeck and Renner (arXiv:0811.1221), for which the paper supplies a short self-contained proof.

Timeline. 1973: Lieb–Ruskai prove strong subadditivity. 2009: Tomamichel–Colbeck–Renner prove the QAEP with explicit convergence rates. 2010: Tomamichel–Colbeck–Renner establish the duality and data processing of smooth entropies (arXiv:0907.5238). 2011–2012: Beaudry–Renner assemble these into the route formalized here.

Setting

All Hilbert spaces are finite-dimensional, and all logarithms are base 2. A density matrix is a positive semidefinite matrix of trace one; $S_=(\mathcal H)$ is their set and $S_\le(\mathcal H)$ is the set of subnormalized states (positive semidefinite, trace at most one). A state on $\mathcal H_A\otimes\mathcal H_B$ is written $\rho_{AB}$ , and its marginal $\rho_B=\operatorname{Tr}_A\rho_{AB}$ . The von Neumann entropy is $H(A)_\rho=-\operatorname{Tr}\rho_A\log\rho_A$ and the conditional entropy $H(A|B)_\rho=H(AB)_\rho-H(B)_\rho$ .

The min-entropy of $A$ conditioned on $B$ is

H_{\min}(A|B)_\rho=\max\{\lambda\in\mathbb R : \exists\,\sigma_B\in S_=(\mathcal H_B),\ \rho_{AB}\le 2^{-\lambda}\,\mathbb 1_A\otimes\sigma_B\}.

The purified distance between subnormalized states is $P(\rho,\sigma)=\sqrt{1-\bar F(\rho,\sigma)^2}$ , where $\bar F(\rho,\sigma)=\|\sqrt\rho\sqrt\sigma\|_1+\sqrt{(1-\operatorname{Tr}\rho)(1-\operatorname{Tr}\sigma)}$ is the generalized fidelity. The smooth min-entropy maximizes the min-entropy over the ball $\mathcal B^\varepsilon(\rho)=\{\rho'\in S_\le : P(\rho,\rho')\le\varepsilon\}$ :

H^\varepsilon_{\min}(A|B)_\rho=\max_{\rho'\in\mathcal B^\varepsilon(\rho_{AB})}H_{\min}(A|B)_{\rho'} .

For $n$ independent copies, $\rho^{\otimes n}$ is a state on $A^n\otimes B^n$ . The non-conditional entropies $H_{\min}(A)_\rho=-\log\|\rho\|_\infty$ , $H_0(A)_\rho=\log\operatorname{rank}\rho$ and $H_\alpha(A)_\rho=\frac{1}{1-\alpha}\log\operatorname{Tr}\rho^\alpha$ , and their smoothings over the same ball, appear in the intermediate lemmas.

Formalization targets

Goal: the von Neumann entropy DPI (Theorem 3)

H(A|BC)_\rho\le H(A|B)_\rho\qquad(\rho\in S_=(\mathcal H_{ABC})).

The goal is the existing Open platform theorem QAlgorithms.Papers.Independent.Gap48.P20.strongSubadditivity, which states $0\le H(CB)+H(RB)-H(B)-H(CRB)$ for every density matrix on $C\otimes R\otimes B$ ; with $A\mapsto C$ , $C\mapsto R$ this is exactly $H(ABC)+H(B)\le H(AB)+H(BC)$ , the expanded form of the inequality above. It is referenced, not restated.

The smooth min-entropy DPI (Theorem 1)

H^\varepsilon_{\min}(A|BC)_\rho\le H^\varepsilon_{\min}(A|B)_\rho .

The QAEP (Theorem 2)

\lim_{\varepsilon\to0}\lim_{n\to\infty}\frac1n H^\varepsilon_{\min}(A^n|B^n)_{\rho^{\otimes n}}=H(A|B)_\rho ,

split into the lower bound (Lemma 4.1) and the upper bound (Lemma 4.2). The milestones below them are the paper's own lemmas: monotonicity of the purified distance (Lemma A.1), Uhlmann's theorem (Theorem A.1, an existing Open platform theorem), the chain rule (Lemma 5.1), the Rényi lower bound (Lemma 5.2), the limit $\alpha\to1$ of Rényi entropies (Lemma B.2), the non-conditional QAEP for $H^\varepsilon_{\min}$ and $H^\varepsilon_0$ (Lemmas 5.4, 5.5), the bound by a nearby conditional entropy (Lemma 5.6), the eigenvalue-alignment bound (Lemma A.2) and the almost-i.i.d. limit (Lemma B.1).

Significance

The DPI for the von Neumann entropy is the single most used inequality in quantum information theory, and strong subadditivity is the structural fact behind it. A machine-checked proof of it is a prerequisite for formalizing essentially any converse theorem of quantum Shannon theory. The QAEP, a milestone here, is independently the bridge between one-shot and asymptotic information theory: it is what makes smooth entropies the right finite-blocklength replacements for the von Neumann entropy.

Both strong subadditivity and the QAEP are proved results; nothing in this mission is open mathematics. What the mission adds is a machine-checked route through one-shot entropies. The goal theorem is Open on the platform: it is posed but has no accepted proof. The milestones of this route, from the smooth min-entropy DPI to the QAEP, are not formalized anywhere on the platform. A completed development would also leave reusable pieces: monotonicity of the purified distance, the chain rule for smooth entropies, and the i.i.d. limits of smooth entropies.

Difficulty

Theorem 1 is short once the purified distance is known to be monotone under trace non-increasing completely positive maps, and that monotonicity (Lemma A.1) is itself the first real obstacle, since it is a statement about the generalized fidelity of subnormalized states. The bulk of the work is the QAEP. Its lower half needs a chain rule that trades conditional for non-conditional entropies at the cost of tripling the smoothing parameter, then precise i.i.d. limits of the non-conditional smooth entropies. The upper half needs a continuity statement for the conditional entropy of states that are only close to $\rho^{\otimes n}$ , uniform in $n$ after division by $n$ . The tempting reading of the double limit as a single limit in $n$ at fixed $\varepsilon$ is stronger than what the paper proves; the inner limit's existence is not established there.

Formalization scope

States are complex matrices indexed by finite types; a bipartite state is a matrix on A × B, a tripartite one on A × (B × C) with B × C the conditioning system of $H(A|BC)$ . The smooth conditional min-entropy, the purified distance, the generalized fidelity, the conditional entropy $H(A|B)$ and the grouped tensor power $\rho^{\otimes n}$ on $A^nB^n$ are the published definitions QAlgorithms_Papers_Independent_Information100_P67; the Rényi entropy and $\operatorname{Tr}_C$ come from QAlgorithms_Papers_Independent_Dependency50_P35. Smooth entropies take values in the extended reals, so an empty ball gives $-\infty$ and a ball containing $0$ gives $+\infty$ .

A local definitions module adds the non-conditional entropies $H_{\min}$ , $H^\varepsilon_{\min}$ , $H_0$ , $H^\varepsilon_0$ , trace non-increasing Kraus families, and the conditional entropy (36) of a subnormalized state $\tilde\rho$ , $\frac{1}{\operatorname{Tr}\tilde\rho}\max_{\sigma_B}\operatorname{Tr}\tilde\rho(\log(\mathbb 1\otimes\sigma_B)-\log\tilde\rho)$ , with the maximum taken over positive definite $\sigma_B$ so that Lean's convention $\log0=0$ cannot enter. The double limit $\lim_{\varepsilon\to0}\lim_{n\to\infty}$ is read through two predicates: " $L\le\lim\lim f$ " means that for every $\delta>0$ there is $\varepsilon_0>0$ with $L-\delta\le f(\varepsilon,n)$ for all $\varepsilon\in(0,\varepsilon_0)$ and all large $n$ , and " $\lim\lim f\le L$ " is the mirror statement.

Trivializing encodings are ruled out: the smooth entropies are the published sup over the full subnormalized purified-distance ball, not free reals and not the ball $\{\rho\}$ ; $\varepsilon$ is quantified universally below $\varepsilon_0$ and is never allowed to depend on $n$ ; and the entropy of the nearby state in Lemma 5.6 is (36), not $H(AB)-H(B)$ .

The paper's Lemma 5.3, (30), is false as printed and is not posed: at $\varepsilon=0$ it states $H_0\le H_\alpha$ for $\alpha<1$ , the reverse of Rényi monotonicity, and $\rho=\operatorname{diag}(0.9,0.1)$ , $\alpha=3/4$ , $\varepsilon=0.1$ gives $1>0.8637$ . Lemma 5.5, which its proof serves, is true and is a milestone. Uhlmann's theorem (Theorem A.1) is the existing Open platform theorem Claimed50.P12.lemmaB_3.

Contributions of any milestone are welcome. The purified-distance monotonicity and the Rényi-limit lemmas are reusable well beyond this paper.

Selected references

N. J. Beaudry and R. Renner, An intuitive proof of the data processing inequality, Quantum Inf. Comput. 12 (2012) 432–441. https://arxiv.org/abs/1107.0740v2
E. H. Lieb and M. B. Ruskai, Proof of the strong subadditivity of quantum-mechanical entropy, J. Math. Phys. 14 (1973) 1938–1941. https://doi.org/10.1063/1.1666274
M. Tomamichel, R. Colbeck and R. Renner, A fully quantum asymptotic equipartition property, IEEE Trans. Inf. Theory 55 (2009) 5840–5847. https://arxiv.org/abs/0811.1221
M. Tomamichel, R. Colbeck and R. Renner, Duality between smooth min- and max-entropies, IEEE Trans. Inf. Theory 56 (2010) 4674–4681. https://arxiv.org/abs/0907.5238
B. Schumacher, Quantum coding, Phys. Rev. A 51 (1995) 2738–2747. https://doi.org/10.1103/PhysRevA.51.2738

18 thms2 active usersReviewed

Quantum Information·Captain: mikedeng1

Entropy and Optimal Decompositions of States Relative to a Maximal Commutative Subalgebra: Equivalent Characterizations of a Symmetric Optimal Pair for Transposition-Invariant Rank-Two StatesResearch Paper

Motivation

In finite dimensional quantum information, a state of a full matrix algebra can be restricted to a smaller algebra of observables. The resulting entropy depends on which observables are retained. For a maximal commutative subalgebra, the retained observables are equivalent to measurements in a fixed orthonormal basis. The restriction has an ordinary probability distribution, but the state before restriction can still contain coherence between basis vectors. Uhlmann studies how the entropy of this restricted state compares with the least average entropy obtainable from pure states whose mixture is the original state. This comparison is an instance of the entropy of a subalgebra introduced by Narnhofer and Thirring and developed in the setting of matrix algebras Uhlmann, pp. 2–4.

Symmetry can make that minimization more concrete. A unitary that swaps two basis projections acts on states and their decompositions. Uhlmann's Lemma 6 asks when a rank two state fixed by this swap has a distinguished two-state optimal decomposition, and relates that event to the geometry of a set on which the entropy roof is affine Uhlmann, pp. 8–11. The result is a specific connection between a physical symmetry, an optimization problem over pure states, and the extreme points of a convex set.

Setting

Let $\mathcal H=\mathbb C^d$ with its standard basis $|j\rangle$ , and let $\mathcal C$ be the diagonal algebra. Its minimal projections are $P_j=|j\rangle\langle j|$ . A state is represented by a positive semidefinite matrix $D$ of trace one. A pure state has density matrix $|\psi\rangle\langle\psi|$ for a unit vector $\psi$ . The state of $\mathcal C$ obtained by restricting $D$ records the diagonal probabilities $D_{jj}$ Uhlmann, p. 4, equations (1)–(3).

Write $s(x)=-x\ln x$ , with $s(0)=0$ . The diagonal entropy is $\widetilde S(D)=\sum_j s(D_{jj})$ . The convex roof $R(D)$ is the infimum of $\sum_k p_k\widetilde S(\rho_k)$ over finite decompositions $D=\sum_k p_k\rho_k$ into pure states with positive weights $p_k$ summing to one. A decomposition attaining the infimum is optimal. Uhlmann's entropy of $\mathcal C$ at $D$ is $H_D=\widetilde S(D)-R(D)$ Uhlmann, pp. 4–5, equations (4)–(7).

An affine functional $l$ supports $R$ if $l\le R$ on all states and equality holds at some state. Its contact set is $\Omega(l)=\{\nu:R(\nu)=l(\nu)\}$ . Given $D$ , define $\Omega_D$ as the intersection of all contact sets whose support functional touches $R$ at $D$ . This intersection is compact and convex, contains every pure state used by an optimal decomposition of $D$ , and is a region on which $R$ is affine Uhlmann, pp. 6–7, Lemma 3 and equation (10). A transposition $U$ swaps two $P_j$ and fixes the remaining minimal projections. It transforms a density matrix as $D\mapsto U^*DU$ Uhlmann, p. 8.

Formalization targets

Goal: equivalent rank two conditions

For a rank two state $D$ fixed by a transposition $U$ , Uhlmann's Lemma 6 asserts equivalence of three statements:

\begin{aligned} \text{(a)}\;&D\text{ is the only }U\text{-invariant state in }\Omega_D;\\ \text{(b)}\;&D\text{ has an optimal decomposition into two different pure states,}\ &\text{and some member of }\Omega_D\text{ does not commute with }U;\\ \text{(c)}\;&\operatorname{Ext}(\Omega_D)=\{\rho,U^*\rho U\}\text{ for two distinct states.} \end{aligned}

The milestone list follows the paper's supporting results: finite optimal decompositions with rank bounds (Lemma 1), comparison on an $R$ -set (Lemma 2), compact supporting contact sets and their covering (Lemma 3), the intersection properties of $\Omega_D$ (the Corollary at equation (10)), zero entropy implying purity (Lemma 4), and the rank two support projection formula (equation (13)) Uhlmann, pp. 5–9. The goal preserves all three clauses of the printed equivalence.

Significance

When the equivalent conditions hold, the rank two state has an optimal decomposition using just two pure states, while the entire supporting contact set has only the two swapped extreme points. Thus the statement identifies circumstances under which the symmetry of a matrix state controls both the optimizer and the geometry of the convex roof. Uhlmann subsequently gives an explicit expression for $R(D)$ under these conditions in equation (27), which is outside the present goal Uhlmann, pp. 10–12.

The result is proved in the cited paper; the remaining task here is a machine checked development of the definitions, supporting results, and equivalence. The local Lean files state the targets and compile with proof placeholders; they do not constitute machine checked proofs of the milestones or goal. A completed development would also supply reusable finite dimensional infrastructure for pure state roofs, supporting contact sets, and optimal decompositions of density matrices.

Difficulty

An optimal pair alone does not immediately determine every extreme point of $\Omega_D$ . That set is an intersection of all contact sets, and may be larger than the convex hull of the pure states seen in one decomposition. The paper itself says equality with that smaller convex hull remains a conjecture in general Uhlmann, p. 7, Remark and footnote 3. Its printed discussion of the implication from the optimal pair to the two extreme points does not resolve this general distinction. The equivalence is therefore retained exactly as printed and the gap is recorded for review.

Formalization scope

Matrices are indexed by Fin d, so the paper's indices $1,\ldots,d$ become $0,\ldots,d-1$ . The state predicate reuses the published QAlgorithms.IsDensityMatrix. Pure states are unit-vector outer products. Finite decompositions use strictly positive real weights and complex matrix mixtures. Real.negMulLog supplies natural logarithms and $s(0)=0$ . The real infimum defining $R$ is applied only to states; there the decomposition set is nonempty and its costs are bounded below. Off the state space, Lean's real infimum can return a default value that has no meaning in the paper.

Supporting affine functionals are represented by Hermitian matrices via $l_A(\nu)=\operatorname{Re}\operatorname{Tr}(\nu A)$ , as in the paper's equation (9). The set $\Omega_D$ is the full intersection in equation (10), and its extreme points are taken in the ambient real matrix space. The transposition in the goal is explicitly self-adjoint, $U^*=U$ , matching the identity used in the printed proof. The rank is matrix rank. “Length two” means two distinct pure states with positive weights whose cost attains $R(D)$ . No optimal pair is assumed as a hypothesis.

The needed contributions are proofs of the six stated milestones, the finite dimensional properties of the model definitions they use, and the three implications of Lemma 6. The model's pure state decomposition and supporting set definitions are reusable for other convex roof problems on finite density matrices.

Selected references

Armin Uhlmann, Entropy and optimal decompositions of states relative to a maximal commutative subalgebra, preprint arXiv:quant-ph/9704017v2, 1998. arXiv

9 thms2 active usersReviewed

Quantum Information·Captain: mikedeng1

General Benchmarks for Quantum Repeaters: For the Qudit Dephasing Channel the Entanglement-Flux Upper Bound Meets the Coherent Information, log₂ d − H(P)Research Paper

Motivation

A quantum repeater is judged by how much it beats direct transmission over a point-to-point link. The natural yardsticks are the two-way assisted capacities of the link's channel $\mathcal E$ : the quantum capacity $Q_2(\mathcal E)$ and the secret-key capacity $K(\mathcal E)$ , the best rates of entanglement and key that two parties can obtain over many uses of $\mathcal E$ when unlimited two-way classical communication and local operations are free. Computing them exactly for a given channel is rare, because it requires a lower and an upper bound that meet.

Pirandola and Laurenza (arXiv:1512.04945v2, 2016) obtain such matching bounds for a family of channels. The lower bound is the coherent information of the channel (with its reverse version), which is achievable by the hashing protocol. The upper bound is the entanglement flux $\Phi(\mathcal E)$ , the relative entropy of entanglement of the channel's Choi matrix, which bounds $K$ for channels that can be simulated by teleportation. For the qudit dephasing channel the two bounds coincide, which gives $Q_2=K=\log_2 d-H(\mathbf P)$ (Eqs. (20) and (95)). This mission formalizes that coincidence.

Setting

Fix a dimension $d\ge2$ and the computational basis $\{|j\rangle\}_{j=0}^{d-1}$ of a qudit. Let $\omega=e^{2\pi i/d}$ and let $Z$ be the generalized phase operator, $Z|j\rangle=\omega^j|j\rangle$ . For a dephasing probability $p\in[0,1]$ define the binomial weights

P_m(p,d)=\binom{d-1}{m}p^m(1-p)^{d-1-m},\qquad m=0,\dots,d-1,

and the qudit dephasing channel, given by its Kraus operators,

\mathcal P_d(\rho)=\sum_{m=0}^{d-1}E_m\rho E_m^\dagger,\qquad E_m=\sqrt{P_m(p,d)}\,Z^m .

Write $\mathbf P=\{P_m(p,d)\}_m$ and $H(\mathbf P)=-\sum_mP_m\log_2P_m$ (with $0\log0=0$ ) for its Shannon entropy.

The Choi matrix of a map $\mathcal E$ on $d\times d$ matrices is $\rho_{\mathcal E}=(\mathcal I\otimes\mathcal E)(\Psi_d)$ , where $|\Psi_d\rangle=d^{-1/2}\sum_i|ii\rangle$ . The first tensor factor is the reference $R$ , the second the channel output $B$ . With the von Neumann entropy $S(\rho)=-\mathrm{Tr}\,\rho\log_2\rho$ :

the coherent information of the channel is $I_C(\mathcal E)=S(\mathrm{Tr}_R\rho_{\mathcal E})-S(\rho_{\mathcal E})$ ;
the reverse coherent information is $I_{RC}(\mathcal E)=S(\mathrm{Tr}_B\rho_{\mathcal E})-S(\rho_{\mathcal E})$ ;
the relative entropy is $S(\rho\|\sigma)=\mathrm{Tr}[\rho(\log_2\rho-\log_2\sigma)]$ , and $+\infty$ when the support of $\rho$ is not inside that of $\sigma$ ;
the relative entropy of entanglement of a bipartite state is $E_R(\rho)=\inf_{\sigma\in\mathrm{SEP}}S(\rho\|\sigma)$ , the infimum over all separable states for the cut $R:B$ ;
the entanglement flux of the channel is $\Phi(\mathcal E)=E_R(\rho_{\mathcal E})$ .

The paper's candidate separable state is $\tilde\sigma=\sum_i\frac1d|i\rangle\langle i|\otimes\mathcal P_d(|i\rangle\langle i|)$ .

Formalization targets

Goal (Eqs. (94)–(95), p. 11)

For every $d\ge2$ and $p\in[0,1]$ :

I_C(\mathcal P_d)=I_{RC}(\mathcal P_d)=\log_2d-H(\mathbf P),\qquad \Phi(\mathcal P_d)\le\log_2d-H(\mathbf P).

The lower and the upper bound on the two-way capacities therefore meet. The statement keeps $d$ and $p$ free and asserts exact values, not numerical constants.

Milestones (in attack order)

The Choi matrix of $\mathcal P_d$ in closed form (p. 11, display between Eqs. (90) and (91)).
Eq. (91): $S(\rho_{\mathcal P_d})=H(\mathbf P)$ .
Eq. (68): $S(\rho\|\sigma)=-S(\rho)-\sum_i\langle i|\rho|i\rangle\log s_i$ in the eigenbasis of $\sigma$ , under support inclusion.
Eq. (92): $\tilde\sigma=\sum_i\frac1d|ii\rangle\langle ii|$ and $\tilde\sigma$ is separable.
Eq. (93): $\mathrm{Tr}(\rho_{\mathcal P_d}\log_2\tilde\sigma)=-\log_2d$ , with the support of $\rho_{\mathcal P_d}$ inside that of $\tilde\sigma$ .
Eq. (94): $\Phi(\mathcal P_d)\le S(\rho_{\mathcal P_d}\|\tilde\sigma)=\log_2d-H(\mathbf P)$ .
Eq. (45): for a unital, trace-preserving map $\mathcal E$ , $I_C(\mathcal E)=I_{RC}(\mathcal E)=\log_2d-S(\rho_{\mathcal E})$ .

Significance

The result. The coincidence of the two bounds pins down $Q_2$ and $K$ of the qudit dephasing channel for every $d$ and $p$ , which gives the repeaterless benchmark for any qudit link dominated by dephasing. At $d=2$ it recovers the qubit dephasing benchmark $1-H_2(p)$ of the same paper (Eq. (75), with $p\leftrightarrow1-p$ , which the binary entropy does not see). Combined with the operational facts the paper imports (the hashing inequality and the bound of $K$ by the flux for teleportation-covariant channels), it yields the capacity formula (95).

Formalizing it. The paper's computation is complete but terse. The formalization makes three implicit points explicit: the support of the Choi matrix lies inside the support of the rank- $d$ state $\tilde\sigma$ (so $\log\tilde\sigma$ is taken on its support); the claim of " $d$ non-zero eigenvalues" in (91) fails at $p\in\{0,1\}$ , while the entropy identity does not; and (45) needs trace preservation as well as unitality. The results are proved in the paper and, as far as the platform's catalogue shows, formalized nowhere. Eq. (68) and Eq. (45) are reusable lemmas about arbitrary states and unital channels.

Difficulty

The calculation on the page is short; the difficulty lies in what it leaves to the reader. The entropy identity (91) asks for the spectrum of a $d^2\times d^2$ matrix that is not diagonal in the computational basis, while the von Neumann entropy is defined through the matrix functional calculus, so "diagonalizing" has to be made precise. The state $\tilde\sigma$ has rank $d$ in dimension $d^2$ : the relative entropy against it is finite only because of a support inclusion the paper does not mention, and a computation that ignores the kernel of $\tilde\sigma$ does not establish the value. The upper bound needs $\tilde\sigma$ to be separable in the sense of the infimum, a finite convex combination of product density matrices, not merely diagonal. Finally, the coherent information is a difference of entropies of a partial trace and of the full Choi matrix; equating it to $\log_2 d-H(\mathbf P)$ requires both that the output marginal is maximally mixed and the entropy identity (91).

Formalization scope

Qudit indices are Fin d, with $d\ge2$ (and [NeZero d] where an instance needs it); $p$ is real with $0\le p\le1$ . $Z^m$ is a matrix power, $\omega=\exp(2\pi i/d)$ , and the channel is the published QAlgorithms.krausApply of the Kraus family $\sqrt{P_m}\,Z^m$ . The Choi matrix is the published QAlgorithms.idTensorSuperop applied to maximallyEntangledProjector d (entries $1/d$ on $|ii\rangle\langle jj|$ ), the reference being the first factor of Fin d × Fin d. Entropies are in bits with $0\log0=0$ : QAlgorithms.vnEntropy for states and a local Shannon entropy for the weights. The partial traces are QAlgorithms.traceLeft (over the reference) and QAlgorithms.traceRight (over the output). The relative entropy and $E_R$ are the published relativeEntropyBits and relativeEntanglement (Umegaki entropy divided by $\ln2$ , $+\infty$ off support, infimum over IsSeparableDensity, values in $[0,\infty]$ ). The real bound is embedded with ENNReal.ofReal; since $H(\mathbf P)\le\log_2d$ , nothing is lost.

None of the defined quantities is given by its closed form: the Choi matrix is computed from the channel, $E_R$ is the infimum over all separable states (not $S(\rho\|\tilde\sigma)$ or an infimum over diagonal states), and $I_C$ is defined from partial traces, not as $\log_2d-S(\rho_{\mathcal E})$ . This rules out the trivializing formalization in which a milestone or the goal holds by definition. The bound $\log_2d$ alone holds for every state; the goal's bound is $\log_2d-H(\mathbf P)$ .

The operational capacities $Q_2$ and $K$ of Eq. (95) are not formalized. They are defined over adaptive LOCC protocols with private-state targets, which have no substrate on the platform. The paper also does not prove the two bridges from them to the bounds: it imports $K\le\Phi$ (Eq. (2), from Pirandola et al.) and the hashing inequality (from Devetak and Winter). For the same reason, the reverse inequality $\Phi(\mathcal P_d)\ge\log_2d-H(\mathbf P)$ is not stated, since the paper obtains it only through the hashing bound. Teleportation stretching, convexity of the flux, the bosonic Gaussian channels and the erasure channel are outside this mission.

Contributions are welcome at every level: the spectrum of circulant blocks, the support calculus of the Umegaki entropy, and the separable decomposition of diagonal states are all reusable beyond this mission.

Selected references

S. Pirandola, R. Laurenza, General Benchmarks for Quantum Repeaters, arXiv preprint, v2, 2016. https://arxiv.org/abs/1512.04945v2
S. Pirandola, R. Laurenza, C. Ottaviani, L. Banchi, Fundamental limits of repeaterless quantum communications, Nature Communications 8, 15043, 2017. https://doi.org/10.1038/ncomms15043
I. Devetak, A. Winter, Distillation of secret key and entanglement from quantum states, Proc. R. Soc. A 461, 207–235, 2005. https://doi.org/10.1098/rspa.2004.1372
V. Vedral, M. B. Plenio, Entanglement measures and purification procedures, Phys. Rev. A 57, 1619, 1998. https://doi.org/10.1103/PhysRevA.57.1619

15 thms2 active usersReviewed

Quantum Information Theoretical Computer Science·Captain: mikedeng1

Improving the Security of Quantum Protocols via Commit-and-Open: After the Commit-and-Open Test, Any Dishonest Bob Is β-Benign Up to a Negligible Trace DistanceResearch Paper

Motivation

Many two-party quantum protocols, such as oblivious transfer and password-based identification, start the same way: Alice sends Bob $n$ qubits $|x\rangle_\theta$ encoding random bits $x$ in random BB84 bases $\theta\in\{+,\times\}^n$ . Their security proofs work only against a restricted Bob, for example one with bounded quantum memory (Damgård, Fehr, Salvail, Schaffner 2005). Unrestricted security is impossible for such tasks in the plain model.

Damgård, Fehr, Lunemann, Salvail and Schaffner (arXiv:0902.3918, CRYPTO 2009) proposed a generic commit-and-open compiler. Bob commits to his measurement bases $\hat\theta$ and outcomes $\hat x$ position by position. Alice opens a random fraction $\alpha$ of the commitments and checks that $x_i=\hat x_i$ wherever her basis agreed with Bob's. Their headline result, Theorem 4.2, says that the compiled protocol is computationally secure against any polynomial-time Bob. Its proof reduces everything computational to one information-theoretic statement: after the test, a dishonest Bob is β-benign (Definition 4.1), up to a negligible error. The paper's introduction presents this statement as the new tool. This mission formalizes it.

Setting

Alice holds $m$ qubits, one half of each of $m$ EPR pairs, in a register $A=\mathbb C^{\{0,1\}^m}$ . Bob holds an arbitrary finite-dimensional register $E$ . The joint state right before the test is an arbitrary unit vector $|\varphi_{AE}\rangle\in\mathcal H_A\otimes\mathcal H_E$ . This is the state after a dishonest Bob has received his halves and committed to $\hat x\in\{0,1\}^m$ and $\hat\theta\in\{+,\times\}^m$ .

The test is a pair $(T,T')$ . $T$ is a uniformly random set of $k=\lfloor\alpha m\rfloor$ positions; $T'=\{i\in T:\theta_i=\hat\theta_i\}$ for Alice's uniform bases $\theta$ is a uniform subset of $T$ . So $P_{Test}(T,T')=1/(\binom mk 2^k)$ . In the analysed version of the protocol (Fig. 4), Alice measures the positions in $T$ in Bob's bases $\hat\theta|_T$ and accepts iff $x_i=\hat x_i$ for all $i\in T'$ . She then measures the remaining $n=m-k$ positions in her bases $\theta|_{\bar T}$ , producing $X$ .

The quantities of interest are:

the min-entropy $H_\infty(X)=-\log_2\max_xP_X(x)$ and its conditional version $H_\infty(X|_I\mid X|_{\bar I}=x|_{\bar I})$ ;
the max-entropy $H_0(\rho)=\log_2\operatorname{rank}\rho$ ;
the Hamming distance $d_H$ and the relative distance $r_H=d_H/\text{length}$ ;
the trace distance $\delta(\rho,\sigma)=\tfrac12\operatorname{tr}|\rho-\sigma|$ ;
the binary entropy $h(\mu)=-(\mu\log_2\mu+(1-\mu)\log_2(1-\mu))$ .

A function $\nu(m)$ is negligible if $|\nu(m)|\le m^{-c}$ for every $c$ and all large $m$ .

The real cq state is $\rho_{TestAE}=\sum_{test}P_{Test}(test)|test\rangle\langle test|\otimes|\varphi_{AE}\rangle\langle\varphi_{AE}|$ . The set

B_{test}=\{x: r_H(x|_{\bar T},\hat x|_{\bar T})\le r_H(x|_{T'},\hat x|_{T'})+\varepsilon\}

collects the outcomes whose error rate on the unopened positions is predicted by the error rate on $T'$ .

Formalization targets

Goal: commit-and-open forces benign behaviour (§4.3, p. 12)

For every $0<\alpha<1$ and $\beta>0$ there is a negligible $\nu$ such that, for every $m$ , $\hat x$ , $\hat\theta$ , finite $E$ and unit $|\varphi_{AE}\rangle$ , there are unit vectors $|\tilde\varphi^{test}_{AE}\rangle$ with

\delta\Big(\rho_{TestAE},\ \sum_{test}P_{Test}(test)|test\rangle\langle test|\otimes|\tilde\varphi^{test}_{AE}\rangle\langle\tilde\varphi^{test}_{AE}|\Big)\le\nu(m),

and such that, in the ideal state, every branch Alice accepts satisfies the bounds (1) of Definition 4.1:

H_\infty\big(X|_I\mid X|_{\bar I}=x|_{\bar I}\big)\ge d_H(\theta|_I,\hat\theta|_I)-\beta n,\qquad H_0(\rho_{ER})\le\beta n.

No constant is hard-coded; $\beta$ is arbitrary.

Milestones

Lemma 2.3: measuring a superposition of $|J|$ product vectors loses at most $\log|J|$ bits of min-entropy, and leaves Bob's register with rank at most $|J|$ .
The trace distance of pure states, $\sqrt{1-|\langle\psi|\varphi\rangle|^2}$ .
The trace distance of two cq states over $Test$ is the $P_{Test}$ -average of the branch distances.
The classical sampling bound: $\Pr_{test}[x\notin B_{test}]$ is negligible, uniformly in $x$ .
Lemma 4.3: $\rho_{TestAE}$ is negligibly close to a state each of whose branches is supported on $B_{test}$ in Bob's basis.
The Hamming-ball bound $|\{y:d_H(y,\hat y)\le\mu n\}|\le2^{h(\mu)n}$ for $0\le\mu\le\tfrac12$ .
Corollary 4.4: on such a branch, $H_\infty\ge d_H-h(err+\varepsilon)n$ and $H_0\le h(err+\varepsilon)n$ , where $err$ is the error rate on $T'$ .

Significance

The goal is what makes the compiler work. Combined with the security of the original protocol against benign Bob, it turns any BB84-type protocol that is secure in a restricted model into one secure against arbitrary dishonest Bob in the computational setting. The paper derives oblivious transfer and password-based identification this way (§6). The same statement also preserves bounded-quantum-storage security (§5.2). Its quantitative form, $\beta=h(err+\varepsilon)$ , shows how noise tolerance enters (§5.1).

The paper's headline Theorem 4.2 is computational: it quantifies over polynomial-time quantum adversaries and simulators in the common-reference-string model, with a dual-mode commitment scheme specified in prose. That wrapper is out of scope. The unconditional core claim, closing §4.3, is a statement about finite-dimensional states, entropies and a sampling distribution. To our knowledge no machine-checked proof of it, of Lemma 4.3, or of Corollary 4.4 exists. Formalizing it also produces reusable pieces: min- and max-entropy of superpositions, trace distance of pure and cq states, and a sampling bound for random subsets.

Difficulty

The statement mixes a quantum and a classical argument, and neither carries the whole weight. The obvious attempt, applying an entropic uncertainty relation directly to Bob's state, fails: Bob's register may be entangled with all of Alice's qubits, so nothing bounds its rank a priori. The bound appears only after the real state is replaced by a nearby one, and that replacement must be uniform over Bob's register and strategy. Uniformity is the delicate point: the negligible function must not depend on $m$ , $\hat x$ , $\hat\theta$ or the state.

The sampling step concerns sampling without replacement ( $T$ of fixed size), followed by an independent subsample $T'$ that can be empty. The entropy bounds then need the Hamming-ball estimate at the real radius $(err+\varepsilon)n$ , valid only up to $\tfrac12$ .

Formalization scope

Registers are $\mathbb C^{\{0,1\}^m}$ (EuclideanSpace ℂ (Fin m → Bool)) and $\mathbb C^E$ for a finite type E. Joint states are unit vectors of the product. The joint state is pure, which the paper argues is without loss of generality: a mixed state is purified and the purifier joins $E$ .
Bits are Bool; bases are Bool with false = $+$ , true = $\times$ . Positions are 0-based Fin m.
$|T|=\lfloor\alpha m\rfloor$ and $n=m-\lfloor\alpha m\rfloor$ ; these match the paper's $\alpha m$ and $(1-\alpha)m$ whenever $\alpha m$ is an integer.
$\log=\log_2$ . $h$ is Mathlib's Real.binEntropy divided by $\ln2$ . The trace norm is the published WildeQIT.traceNorm, and the trace distance carries the factor $\tfrac12$ .
Alice's two measurements (in $\hat\theta$ on $T$ , in $\theta$ on $\bar T$ ) are encoded as one measurement in the mixed basis. Conditional min-entropies condition on $x|_T$ as well.
Bob's post-measurement state is kept unnormalized, which leaves its rank unchanged. Statements that condition on an outcome assume it has positive probability.
$r_H$ on the empty set is $0$ .
Corollary 4.4 assumes $err+\varepsilon\le\tfrac12$ . The printed $err\le\tfrac12$ is not sufficient: at $err=\varepsilon=\tfrac12$ the conclusion fails. The goal is unaffected.
The ideal vectors in the goal depend on the test only, and one $\nu$ serves all $m$ , $\hat x$ , $\hat\theta$ , $E$ and states. Neither conclusion is trivial on its own: taking the ideal state equal to the real one gives distance $0$ , and taking it to be the honest state $|\hat x\rangle_{\hat\theta}\otimes|e\rangle$ satisfies (1). The goal demands both at once.

Contributions are welcome on any milestone. The sampling bound and the pure-state and block-diagonal trace-distance identities are independent of the rest. The trace-norm lemmas and the Hamming-ball bound are useful beyond this mission.

Selected references

I. Damgård, S. Fehr, C. Lunemann, L. Salvail, C. Schaffner, Improving the Security of Quantum Protocols via Commit-and-Open, CRYPTO 2009; arXiv:0902.3918v4. https://arxiv.org/abs/0902.3918
I. Damgård, S. Fehr, L. Salvail, C. Schaffner, Cryptography in the Bounded Quantum-Storage Model, FOCS 2005. https://arxiv.org/abs/quant-ph/0508222
W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, J. Amer. Statist. Assoc. 58 (1963). https://doi.org/10.1080/01621459.1963.10500830
S. Fehr, C. Schaffner, Composing Quantum Protocols in a Classical Environment, TCC 2009. https://arxiv.org/abs/0804.1059

11 thms2 active usersReviewed

Mathematical Physics Quantum Information·Captain: mikedeng1

Information-disturbance tradeoff in quantum measurement on the uniform ensemble and on the mutually unbiased bases: the square-root dynamics is least disturbing on the uniform ensembleResearch Paper

Motivation

Measuring a quantum system disturbs it. The information–disturbance tradeoff asks how little a measurement that yields a given amount of information about an unknown state must change that state. The question underlies the security analysis of quantum key distribution, where an eavesdropper's information gain is paid for in detectable disturbance, and the design of measurements that must leave a system usable afterwards, as in sequential or weak measurement schemes.

A measurement has two separate parts: the POVM, which fixes the outcome statistics, and the instrument, which fixes the post-measurement state for each outcome. Many instruments realize the same POVM. The natural candidate for the least disturbing one is the square-root (Lüders) dynamics, which maps a state $\rho$ to $F_b^{1/2}\rho F_b^{1/2}$ on outcome $b$ . Whether this candidate is in fact optimal depends on how disturbance is averaged. H. Barnum (2002) showed that it is optimal when the average is over the uniform ensemble of pure states, and computed the resulting minimal disturbance for every POVM (arXiv:quant-ph/0205155). For general ensembles the same paper leaves optimality open (its "Possibility 4").

Setting

Fix a dimension $d\ge1$ and the Hilbert space $\mathbb C^d$ with standard basis $\{|i\rangle\}$ .

A POVM is a finite family $\{F_b\}_{b\in B}$ of positive semidefinite operators with $\sum_bF_b=I$ . Outcome $b$ occurs on state $\rho$ with probability $\operatorname{tr}\rho F_b$ .
An instrument compatible with $\{F_b\}$ is a finite family of operators $\{A_{bi}\}$ (Hellwig–Kraus, or HK, operators) with

\sum_iA_{bi}^\dagger A_{bi}=F_b\quad\text{for every }b .

The unnormalized post-measurement state on outcome $b$ is $\mathcal A_b(\rho)=\sum_iA_{bi}\rho A_{bi}^\dagger$ , and the overall operation is $\mathcal A(\rho)=\sum_{b,i}A_{bi}\rho A_{bi}^\dagger$ .

The square-root operation of the POVM is $\mathcal S(\rho)=\sum_bF_b^{1/2}\rho F_b^{1/2}$ , the instrument with the single HK operator $F_b^{1/2}$ per outcome. An instrument with one HK operator per outcome has one-term conditional dynamics.
The uniform ensemble $\Omega$ is the unitarily invariant probability measure on unit vectors of $\mathbb C^d$ , the law of $U|0\rangle$ for a Haar-random unitary $U$ .
For a pure state the fidelity with an operator $\sigma$ is $\langle\psi|\sigma|\psi\rangle$ . The average fidelity of an operation $\mathcal E$ is $\overline F(\mathcal E)=\int d\Omega_\psi\,\langle\psi|\mathcal E(|\psi\rangle\langle\psi|)|\psi\rangle$ , and its average disturbance is

D(\mathcal E)=1-\overline F(\mathcal E)=1-\int d\Omega_\psi\sum_{b,i}|\langle\psi|A_{bi}|\psi\rangle|^2\qquad(\mathcal E=\mathcal A).

The second moment of the ensemble is $\Pi=\int d\Omega_\psi\,|\psi\rangle\langle\psi|\otimes|\psi\rangle\langle\psi|$ .

Formalization targets

The goal and the numbered milestones below are from Barnum, pp. 9–13, arXiv:quant-ph/0205155v1.

Goal: Theorem 5

For every POVM $\{F_b\}$ and every finite instrument $\{A_{bi}\}$ compatible with it,

D(\mathcal S)\;\le\;D(\mathcal A).

The instrument may have several HK operators per outcome; this is what distinguishes Theorem 5 from Theorem 8.

Milestones

Eq. (31) (Jones): for unit vectors $a,b$ , $\int d\Omega_\psi|\langle\psi|a\rangle|^2|\langle\psi|b\rangle|^2=\dfrac{1+|\langle a|b\rangle|^2}{d(d+1)}$ .
Lemma 9: $\Pi=\dfrac{1}{d(d+1)}\sum_{i,j}\big(|i\rangle\langle i|\otimes|j\rangle\langle j|+|i\rangle\langle j|\otimes|j\rangle\langle i|\big)$ .
Eq. (32): $\int d\Omega_\psi\langle\psi|A|\psi\rangle\langle\psi|B|\psi\rangle=\operatorname{tr}\Pi(A\otimes B)=\frac{1}{d(d+1)}\sum_{ij}\big(\langle i|A|i\rangle\langle j|B|j\rangle+\langle i|A|j\rangle\langle j|B|i\rangle\big)$ .
Eq. (33): $\overline F\big(\rho\mapsto\sum_kA_k\rho A_k^\dagger\big)=\frac{1}{d(d+1)}\sum_k\big(|\operatorname{tr}A_k|^2+\operatorname{tr}A_kA_k^\dagger\big)$ .
Trace bound (p. 13, cited from von Neumann): for $A\ge0$ , $\max_{V\text{ unitary}}|\operatorname{tr}VA|$ is attained where $VA=\sqrt{A^\dagger A}$ .
Theorem 8: for one-term instruments, $\sum_b\overline F_b\le\frac{1}{d(d+1)}\big(d+\sum_b(\operatorname{tr}F_b^{1/2})^2\big)$ , with equality for the square-root dynamics.
Theorem 7 (Ando): $(A,B)\mapsto A^t\otimes B^{1-t}$ is jointly concave for $0\le t\le1$ .
Proposition 6: $\langle\psi|P_1|\psi\rangle^2+\langle\psi|P_2|\psi\rangle^2\le\langle\psi|\sqrt{P_1^2+P_2^2}|\psi\rangle^2$ for positive $P_1,P_2$ .
Coarse-graining (p. 10): $\sum_j\langle\psi|P_j|\psi\rangle^2\le\langle\psi|\sqrt{\sum_jP_j^2}|\psi\rangle^2$ .

Significance

Theorem 5 together with Theorem 8 gives a closed form for the minimal disturbance on the uniform ensemble of every POVM: $\overline D_{\min}=1-\frac{1}{d(d+1)}\big(d+\sum_b(\operatorname{tr}F_b^{1/2})^2\big)$ (Eqs. (34)–(35)). For rank-one POVMs this is $(d-1)/(d+1)$ , one endpoint of the information–disturbance frontier that the rest of the paper studies. The result also shows that on this ensemble, extra Kraus operators per outcome never reduce disturbance, so the frontier may be computed over square-root instruments alone.

The milestones are of independent use. Lemma 9 and Eq. (32) are the standard second-moment formula for Haar-random pure states (the 2-design property). Eq. (33) is the Kraus-operator form of the average fidelity that appears throughout quantum channel benchmarking. Ando's concavity theorem is equivalent to Lieb's concavity theorem.

The results are proved in the paper (2002). This mission formalizes them; to the extent known, none of the paper's statements has a machine-checked proof. The platform already has the uniform ensemble and the average fidelity as published definitions, and Nielsen's formula relating average and entanglement fidelity, which is a different statement.

Difficulty

The polar-decomposition step suggests a pointwise argument: write $A_{bi}=U_{bi}P_{bi}$ and replace $U_{bi}$ by $I$ . That fails. For a fixed $\psi$ , $|\langle\psi|UP|\psi\rangle|^2$ can exceed $\langle\psi|P|\psi\rangle^2$ (take $d=2$ , $P=|0\rangle\langle0|$ , $\psi=(|0\rangle+|1\rangle)/\sqrt2$ , $U|0\rangle=\psi$ ). The replacement is valid only after averaging over $\Omega$ , through the explicit fourth-moment computation of Lemma 9. The second obstacle is merging several HK operators of one outcome into one, which needs Proposition 6. Proposition 6 is an inequality between non-commuting operators. The commuting case is elementary, but the general case rests on Ando's joint concavity, an operator-concavity theorem of Lieb's type that is not in Mathlib.

Formalization scope

Operators are Matrix (Fin d) (Fin d) ℂ and vectors EuclideanSpace ℂ (Fin d), with 0 < d. The uniform ensemble is the published QAlgorithms.QuditFidelity.haarPureStateLaw d hd, the image of normalized Haar measure on the unitary group under $U\mapsto U|0\rangle$ . The average fidelity is the published averageFidelity d hd, whose integrand is $\operatorname{Re}\operatorname{tr}\big(|\psi\rangle\langle\psi|\,\mathcal E(|\psi\rangle\langle\psi|)\big)$ . Disturbance is 1 - averageFidelity. POVMs are QAlgorithms.IsPOVM on a finite outcome type. An instrument is A : B → I → Matrix with one finite Kraus index type I for every outcome. Outcomes with fewer operators are padded with zeros, which changes neither the compatibility condition nor the operation. The square root is cfc Real.sqrt. Real powers in Theorem 7 use cfc of Real.rpow, so $X^0=I$ . Real-valued quadratic forms and traces of positive operators are taken as real parts. $\Pi$ is defined entrywise.

The goal must not be read with I = Unit. That would be Theorem 8's one-term case, and the goal quantifies over every finite I. The ensemble is the Haar image itself, not a measure assumed to have the second moment of Lemma 9.

The wrapper disturbance accepts a raw superoperator, for which an integral need not exist. Every theorem here applies it only to a finite Kraus map, whose integrand is continuous and integrable on the Haar ensemble. A complete development needs Haar moment integrals on the unitary group (reusable for any unitary-design argument), the polar decomposition and the trace inequality for matrices, and an operator-concavity theorem (Ando/Lieb). Contributions of any of these, or of the commuting-case proof of Proposition 6 as a stepping stone, are welcome.

Selected references

H. Barnum, Information-disturbance tradeoff in quantum measurement on the uniform ensemble, preprint, 2002. arXiv:quant-ph/0205155
T. Ando, Concavity of certain maps on positive definite matrices and applications to Hadamard products, Linear Algebra Appl. 26 (1979) 203–241. doi:10.1016/0024-3795(79)90179-4
E. H. Lieb, Convex trace functions and the Wigner–Yanase–Dyson conjecture, Adv. Math. 11 (1973) 267–288. doi:10.1016/0001-8708(73)90011-X
M. A. Nielsen, A simple formula for the average gate fidelity of a quantum dynamical operation, Phys. Lett. A 303 (2002) 249–252. arXiv:quant-ph/0205035

12 thms2 active usersReviewed

Mathematical Physics Quantum Information·Captain: mikedeng1

Capacities of Quantum Channels for Massive Bosons and Fermions: Under Average Energy and Particle-Number Constraints the Capacity Is the Grand-Canonical Entropy, Attained by Fock StatesResearch Paper

Motivation

Classical information can be sent by choosing a quantum state, transmitting it, and asking a receiver to measure it. An ideal noiseless channel seems to have no finite information limit if its carrier can occupy arbitrarily many quantum states. A physical carrier, however, has a limited average energy, and a channel carrying massive particles also has a limited average particle number. Sen(De), Sen, Gromek, Bruß, and Lewenstein ask for the greatest information transfer compatible with both constraints. Their answer connects the channel's information capacity to the entropy of the grand-canonical ensemble familiar from statistical mechanics. Sen(De) et al., pp. 1–2.

The paper also studies how capacities of Bose and Fermi systems respond to condensation and pairing. This mission concerns the result that supports those comparisons: the capacity formula for an ideal, noiseless channel under fixed average energy and particle number. Its finite-dimensional form gives a precise setting in which the optimization and its attaining ensemble can both be stated. Sen(De) et al., pp. 2–4.

Setting

The carrier has a finite-dimensional complex state space. Its Hamiltonian $\mathcal H$ assigns energy, and its number operator $\hat N$ counts particles. The two Hermitian operators commute, so the system has an orthonormal basis of states with definite energy and particle number. These are the Fock states used as signals. For inverse temperature $\beta$ and chemical potential $\mu$ , the grand-canonical state is

\rho_{\mathrm{GCE}}=\frac{\exp[-\beta(\mathcal H-\mu\hat N)]}{Z}, \qquad Z=\operatorname{tr}\exp[-\beta(\mathcal H-\mu\hat N)].

A sender chooses one state $\rho_i$ from a finite ensemble $\mathcal E=\{(p_i,\rho_i)\}$ with probability $p_i$ . Each state may be mixed. The mean state is $\bar\rho=\sum_i p_i\rho_i$ . A receiver chooses a finite quantum measurement and observes its outcome. The accessible information $I_{\mathrm{acc}}(\mathcal E)$ is the largest mutual information between the sender's label and the receiver's outcome among these measurements. The Holevo quantity is $\chi(\mathcal E)=S(\bar\rho)-\sum_i p_iS(\rho_i)$ , where $S$ is von Neumann entropy. All information and entropy values use base-two logarithms, so their units are bits. Sen(De) et al., p. 1.

Fix $E$ and $N$ . An ensemble is admissible when its mean state obeys the two exact constraints $\operatorname{tr}(\bar\rho\mathcal H)=E$ and $\operatorname{tr}(\bar\rho\hat N)=N$ . The paper defines $C_{E,N}$ as the maximum accessible information among admissible ensembles. For the theorem here, $E$ and $N$ are the expectations of $\mathcal H$ and $\hat N$ in $\rho_{\mathrm{GCE}}$ ; no claim of a global inverse from $(E,N)$ to $(\beta,\mu)$ is needed. Sen(De) et al., p. 2.

Formalization targets

The first targets are the paper's entropy bounds: the Holevo bound $I_{\mathrm{acc}}(\mathcal E)\leq\chi(\mathcal E)$ and $\chi(\mathcal E)\leq S(\bar\rho)$ . The grand-canonical variational principle says that, under the two fixed expectations, no state has greater entropy than $\rho_{\mathrm{GCE}}$ . The first and third targets correspond to existing Open platform statements; the second is drafted here. Sen(De) et al., pp. 1–2.

The goal combines the value of the capacity with its attainment:

C_{E,N}=S(\rho_{\mathrm{GCE}}), \qquad I_{\mathrm{acc}}(\mathcal E_{\mathrm{Fock}})=C_{E,N},

where $\mathcal E_{\mathrm{Fock}}$ consists of joint energy and number eigenstates with probabilities supplied by $\rho_{\mathrm{GCE}}$ . Two further milestones record that this ensemble has mean $\rho_{\mathrm{GCE}}$ and that orthogonal pure signals make their classical label information accessible to a measurement. The goal includes an actual maximizing ensemble; an equality involving a supremum alone would leave the paper's attainment claim unstated. Sen(De) et al., p. 2 and abstract.

Significance

The result turns a channel optimization over encodings and measurements into a thermodynamic quantity, while specifying signals that reach the bound. The second constraint matters: energy by itself selects a canonical ensemble, whereas fixed average energy together with fixed average particle number selects a grand-canonical ensemble in the paper's setting. This is the connection the authors use when comparing massive Bose and Fermi carriers. Sen(De) et al., pp. 1–2.

A formalization would add a reusable statement linking three kinds of objects: operational accessible information, entropy maximization with conserved quantities, and a concrete optimal ensemble. The shared quantum definitions already exist on the platform; the Holevo and grand-canonical variational statements are Open goals, rather than machine-checked results claimed by this mission. The present draft has compile-checked statements, not proofs of the capacity theorem or those Open goals.

Difficulty

The accessible information is itself an optimization over measurements, while capacity optimizes it again over every admissible ensemble. Merely diagonalizing the grand-canonical state does not establish that no other ensemble, including an ensemble of mixed or noncommuting states, carries more accessible information. The matching attainment assertion also needs an ensemble of the paper's Fock states that obeys both average constraints. The comparison must use the same bit-valued entropy convention throughout, even though one existing grand-canonical platform theorem states its variational principle using natural logarithms.

Formalization scope

Lean represents states and observables by complex matrices indexed by a finite nonempty type, with $\mathcal H$ and $\hat N$ Hermitian and commuting. The grand-canonical state uses the published Gibbs-state definition. Expected values are real parts of traces, and both constraints are equalities. The finite-dimensional model is exact for finitely many fermionic levels; it is a truncation of the unbounded bosonic Fock space, so this mission does not claim the paper's infinite-dimensional bosonic formula. The theorem permits every real $\beta$ and $\mu$ , with $E$ and $N$ defined from the resulting state.

The capacity domain includes all finite ensemble sizes and arbitrary mixed density matrices, and accessible information optimizes over all finite POVMs. Restricting the ensemble to Fock-diagonal or pure states, fixing its label type to the Fock basis, or fixing the measurement would turn the capacity claim into a different problem. The maximum is expressed as a greatest element of the value set, which records membership and hence attainment. The reusable work includes the ensemble entropy bound, the joint-eigenbasis interface, and the link between orthogonal signals and accessible information. Contributions that establish these links for the stated definitions or connect the existing Open reference theorems to this interface fit the mission. The paper's separately labelled comparison theorem for bosons and fermions, its asymptotic expansions, and its numerical figures are outside this mission.

Selected references

A. Sen(De), U. Sen, B. Gromek, D. Bruß, and M. Lewenstein, Capacities of Quantum Channels for Massive Bosons and Fermions, Physical Review Letters 2005; pinned preprint arXiv:quant-ph/0505028v2, 2006. arXiv

12 thms2 active usersReviewed

Quantum Information·Captain: mikedeng1

Quantum Uncertainty Relation Using Coherence: For Every Qubit State, the Relative Entropies of Coherence in Two Measurement Bases Sum to at Least a Bound Set by Purity and Maximal OverlapResearch Paper

Motivation

An uncertainty relation bounds how sharply two incompatible measurements can both be predicted on one quantum state. The entropic form of Maassen and Uffink (1988), $H(X) + H(Z) \ge -\log_2 c_{\max}$ , measures unpredictability by the Shannon entropies of the outcomes of two measurement bases $\mathbb X$ and $\mathbb Z$ , and incompatibility by their maximal overlap $c_{\max}$ . It underlies security proofs in quantum key distribution and entanglement witnesses, and it has been sharpened repeatedly, for example by Berta et al. (2010) with quantum memory.

The resource theory of quantum coherence (Baumgratz, Cramer and Plenio, 2014) quantifies how far a state is from being diagonal in a fixed basis. Coherence is basis dependent, so a state cannot be incoherent in two incompatible bases at once. Yuan, Bai, Peng and Ma (arXiv:1612.02573v2, 2017) turn this into quantitative quantum uncertainty relations: lower bounds on the sum of the coherences of one state in two bases. For the relative entropy of coherence on a qubit, their Theorem 2 gives a bound depending on the purity of the state and the overlap of the bases, which they show numerically to improve on bounds obtained from the Maassen–Uffink and Sánchez-Ruiz relations.

Setting

A qubit state is a $2\times 2$ complex positive semidefinite matrix $\rho$ with $\operatorname{Tr}\rho = 1$ . A measurement basis $\mathbb X = \{|x_0\rangle, |x_1\rangle\}$ is an orthonormal basis of $\mathbb C^2$ , recorded as the unitary matrix $U$ whose columns are $|x_0\rangle, |x_1\rangle$ . Measuring $\rho$ in $\mathbb X$ gives outcome $i$ with probability $p_i = \langle x_i|\rho|x_i\rangle$ ; the outcome entropy is $H(X) = -\sum_i p_i\log_2 p_i$ .

The dephased state $\rho_{\mathrm{diag}} = \sum_i \langle x_i|\rho|x_i\rangle\,|x_i\rangle\langle x_i|$ is $\rho$ with its off-diagonal part (in $\mathbb X$ ) removed. The relative entropy of coherence is

C^{\mathbb X}_{\mathrm{RE}}(\rho) = H(\rho_{\mathrm{diag}}) - H(\rho),

where $H(\rho) = -\sum_\lambda \lambda\log_2\lambda$ (over the eigenvalues of $\rho$ ) is the von Neumann entropy. All logarithms are base $2$ , and $0\log 0 = 0$ .

The purity of $\rho$ is $P = \operatorname{Tr}[\rho^2] \in [1/2, 1]$ , equal to $1$ exactly for pure states. For two bases $\mathbb X$ and $\mathbb Z$ , the maximal overlap is $c = c_{\max}(\mathbb X, \mathbb Z) = \max_{|x\rangle\in\mathbb X,\,|z\rangle\in\mathbb Z}|\langle x|z\rangle|^2$ , and $c_{\min}$ is the corresponding minimum. On a scalar $t\in[0,1]$ , $H(t) = -t\log_2 t - (1-t)\log_2(1-t)$ is the binary entropy. In the proof the authors use $f(x) = H(xp + (1-x)(1-p))$ , where $p$ is an eigenvalue of $\rho$ .

Formalization targets

Goal: Theorem 2 (p. 8, Eq. (14))

For every qubit state $\rho$ and every pair of measurement bases $\mathbb X, \mathbb Z$ of $\mathbb C^2$ ,

C^{\mathbb X}_{\mathrm{RE}}(\rho) + C^{\mathbb Z}_{\mathrm{RE}}(\rho) \ \ge\ H\!\left(\frac{\sqrt{2P-1}\,(2\sqrt c - 1) + 1}{2}\right) - H(\rho).

Milestones

In the paper's order:

$C^{\mathbb X}_{\mathrm{RE}}(\rho) = H(X) - H(\rho)$ (p. 8), the step from (14) to the conventional form (15).
The spectral form (16): with $\rho = p|r\rangle\langle r| + (1-p)|r_\perp\rangle\langle r_\perp|$ and $a = |\langle r|x\rangle|^2$ , $H(X) = H(ap + (1-a)(1-p))$ . Also $P = 2p^2 - 2p + 1$ and $H(\rho) = H(p)$ .
Lemma 1, Eq. (17): for unit vectors in $\mathbb C^d$ , $a + b \le 1 + \sqrt c$ and $|a-b| \le \sqrt{1-c}$ .
Lemma 1, Eq. (18): in $\mathbb C^2$ , $1 - \sqrt c \le a + b$ .
Eq. (22): $f$ is concave on $[0,1]$ and $f(x) = f(1-x)$ .
For qubit bases, $c = 1 - c_{\min}$ and $c \ge 1/2$ (pp. 8, 11).
Eq. (25): $|\sqrt c - \tfrac12| \ge |\sqrt{1-c} - \tfrac12|$ for $c \ge 1/2$ , hence $f(\sqrt c) \le f(\sqrt{1-c})$ .
The minimum of $g = f(a) + f(b)$ over the region cut out by Lemma 1 is $f(0) + f(\sqrt c)$ (pp. 11–12).

Significance

The result. Theorem 2 is a state-dependent uncertainty relation for coherence. Through milestone 1 it is equivalent to the entropic relation $H(X) + H(Z) \ge H\big((\sqrt{2P-1}(2\sqrt c-1)+1)/2\big) + H(\rho)$ (Eq. (15)), which involves the state only through its purity and entropy. The bound is attained by the maximally mixed state. It reduces to a pure-state relation when $P = 1$ , and it is compared numerically with earlier entropic bounds in §IV of the paper. Lemma 1 is a self-contained inequality on three unit vectors in $\mathbb C^d$ that can be reused in other overlap arguments.

Formalizing it. The theorem has a pen-and-paper proof in the paper; no machine-checked version of it or of any entropic uncertainty relation is known on Prove2Me or in Mathlib. The mission yields a checked proof together with a reusable qubit layer: dephasing in an arbitrary basis, the relative entropy of coherence in bits, outcome entropies, purity and basis overlaps, built on the published von Neumann entropy and binary entropy definitions. The proof in the paper also contains a printed slip on p. 11, where $f(\sqrt c)$ is written as $H(p\sqrt c + (1-p)\sqrt c)$ ; a formal proof settles the correct expression.

Difficulty

There are three separate obstacles.

Matrices and entropies. The relative entropy of coherence is defined through eigenvalues of the dephased matrix. Relating it to outcome probabilities means identifying the spectrum of $U\operatorname{diag}(p_0,p_1)U^\dagger$ through Mathlib's IsHermitian.eigenvalues, which are given only up to an unspecified ordering.
Lemma 1. The lemma is a statement about three unit vectors in arbitrary dimension, with a separate lower bound (18) that holds only in dimension 2. It fails in $\mathbb C^3$ : three orthonormal vectors give $a = b = c = 0$ .
Non-convex minimization. The final minimization is of a concave function over a polygon. A concave function attains its minimum at extreme points, so local or first-order arguments do not apply; the extreme points of the region must be identified and compared, which is the role of Eq. (25) and $c \ge 1/2$ .

Formalization scope

States, bases and entropies. States are Matrix (Fin 2) (Fin 2) ℂ with PosSemidef and trace $1$ . Bases are elements of Matrix.unitaryGroup (Fin 2) ℂ, whose columns are the basis vectors; this covers every orthonormal basis of $\mathbb C^2$ , and global phases of the columns change no quantity. Entropies are in bits through Real.logb 2, with $0\log 0 = 0$ . The von Neumann entropy is the published ShadowTomography.QuantumLB.vnEntropy and the binary entropy is the published WildeQIT.binaryEntropy.
Coherence and overlaps. $C^{\mathbb X}_{\mathrm{RE}}$ is defined from the dephased matrix, as in Eq. (6), and not by the closed form $H(X) - H(\rho)$ ; using that closed form as the definition would make milestone 1 true by unfolding. $c$ is a maximum over all four pairs of basis vectors and $c_{\min}$ the corresponding minimum.
Domains. Lemma 1, Eq. (17), is stated on EuclideanSpace ℂ (Fin d) for every $d$ , and Eq. (18) on $\mathbb C^2$ only. Statements that vary the argument of $f$ restrict $a, b, c, p$ to the intervals the paper uses, because the binary-entropy formula has no meaning outside $[0,1]$ .
No added hypotheses. The goal assumes nothing beyond "a qubit state" and "two measurement bases". On these objects $2P - 1 \ge 0$ and $c \le 1$ , so no square root is evaluated at a negative number.

A complete development needs spectral facts for $2\times 2$ Hermitian matrices, concavity of the binary entropy in bits, and an extreme-point argument for concave functions on a polygon. The qubit layer and Lemma 1 are reusable beyond this mission. Proofs of any milestone, and alternative proofs of the goal, are welcome.

Selected references

X. Yuan, G. Bai, T. Peng, X. Ma, Quantum uncertainty relation using coherence, arXiv:1612.02573v2, 2017; Phys. Rev. A 96, 032313 (2017). https://arxiv.org/abs/1612.02573v2, https://doi.org/10.1103/PhysRevA.96.032313
T. Baumgratz, M. Cramer, M. B. Plenio, Quantifying coherence, Phys. Rev. Lett. 113, 140401 (2014). https://arxiv.org/abs/1311.0275
H. Maassen, J. B. M. Uffink, Generalized entropic uncertainty relations, Phys. Rev. Lett. 60, 1103 (1988). https://doi.org/10.1103/PhysRevLett.60.1103
M. Berta, M. Christandl, R. Colbeck, J. M. Renes, R. Renner, The uncertainty principle in the presence of quantum memory, Nature Physics 6, 659 (2010). https://arxiv.org/abs/0909.0950

12 thms2 active usersReviewed

Probability Quantum Error Correction·Captain: mikedeng1

Quantum Tanner Codes 2: A Random Dual Tensor Code Is Δ^{3/2−ε}-Robust with Δ^γ-Resistance to Puncturing with Probability Tending to 1Research Paper

Motivation

Quantum error correction needs families of codes that protect a growing number of logical qubits while using checks that touch few physical qubits. In a quantum Tanner code, the local constraints come from two smaller binary codes. The distance analysis requires those local codes to satisfy a geometric condition called robustness: a low-weight word in a certain sum code must occupy only a controlled number of complete rows and columns. The deterministic distance theorem in Leverrier and Zémor's Quantum Tanner codes assumes this condition; their Theorem 9 supplies it for randomly chosen component codes. Establishing that random codes satisfy the assumption makes the later existence result meaningful rather than conditional on a property with no known examples.

The appendix follows the approach of Panteleev and Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, with a separate treatment of puncturing. The historical relation here is limited: this mission formalizes Leverrier and Zémor's Theorem 9 and its own numbered supporting results, with their hypotheses and constants.

Setting

Fix two coordinate sets $A$ and $B$ , each of cardinality $\Delta$ . A binary linear code $C_A\subseteq\mathbb F_2^A$ is a vector subspace; similarly $C_B\subseteq\mathbb F_2^B$ . Regard a word on $A\times B$ as a matrix $x=(x_{ab})$ . The column code contains matrices whose column at every $b\in B$ belongs to $C_A$ . The row code contains matrices whose row at every $a\in A$ belongs to $C_B$ . Their intersection is the tensor code $C_A\otimes C_B$ ; their sum is the dual tensor code $C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B$ . The Hamming weight $|x|$ counts its nonzero entries. These conventions are those of §3.5 of the source paper.

Write $d_A,d_B$ for the actual minimum distances of the two component codes. The dual tensor code is $w$ -robust if every codeword $x$ with $|x|\le w$ vanishes outside the union of some set of at most $|x|/d_B$ rows and some set of at most $|x|/d_A$ columns. Thus a low-weight word cannot be spread thinly across many rows and columns. For retained coordinate sets $A'\subseteq A$ and $B'\subseteq B$ , the punctured codes $C_{A'}$ and $C_{B'}$ are the images under restriction. Robustness has $p$ -resistance to puncturing when the corresponding dual tensor code remains $w$ -robust for every pair $A',B'$ of equal size obtained by removing at most $p$ coordinates from each side. These are Definitions 5 and 8 on pp. 15–16 of the paper.

A uniform generator matrix with $r$ rows and $\Delta$ columns is sampled uniformly from all binary matrices of that shape. Its row span is $C_A$ . Independently, a uniform parity-check matrix with $s$ rows and $\Delta$ columns defines $C_B$ as its kernel. Probability is the fraction of matrices, or matrix pairs, satisfying an event. In the asymptotic statement, $\Delta$ tends through natural numbers to infinity.

Formalization targets

Random robustness and resistance

For $0<\rho_A,\rho_B<1$ , $0<\varepsilon<1/2$ , and $1/2+\varepsilon<\gamma<1$ , sample $C_A$ and $C_B$ from the matrix models above, using $\lfloor\rho_A\Delta\rfloor$ generator rows and $\lceil(1-\rho_B)\Delta\rceil$ parity-check rows. The goal, Theorem 9, is

\Pr\!\left[C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B\text{ is }\Delta^{3/2-\varepsilon}\text{-robust with }\Delta^\gamma\text{-resistance}\right]\longrightarrow 1.

The milestones are the paper's numbered appendix statements: Lemma 31 converts concentration on few rows and columns into Definition 5's sharper weight-based bounds; Lemmas 24–29 address ranks and probabilities for random kernels and punctured kernels; Theorem 30 gives the quantitative high-probability alternative used before the final limit. The goal fixes the exponents and quantifies over the whole uniform matrix experiment.

Significance

Theorem 9 certifies that the robustness hypothesis needed by the paper's distance construction occurs with asymptotic probability one. It covers all allowed puncturings at once, which matters because a later distance argument deletes coordinates selected by the codeword under study. A statement about one fixed puncturing would not provide that guarantee. The result is proved in the 2022 paper; this mission poses its statements for machine-checked proofs and does not claim that those proofs already exist.

Formalizing the result produces reusable finite probability statements for random linear codes, a parity-check treatment of puncturing, and rank bounds for sparse binary matrices. Those ingredients are independent of the group complex used in the paper's other mission. They can support later formalizations of random coding arguments where a union over many coordinate restrictions is necessary.

Difficulty

The evident first check is that one fixed low-weight matrix probably does not belong to a random dual tensor code. That alone does not establish robustness: the statement ranges over all such matrices and, for resistance, over every pair of large retained coordinate sets. The paper's intermediate results control this whole collection using rank information about sparse matrices and the exact probability that independent vectors lie in a random kernel. A further issue is that puncturing a parity-check code does not simply delete columns from its defining matrix; the discarded columns contribute a random subspace. The quantitative event in Theorem 30 and the simultaneous limit in Theorem 9 both have to survive these ranges.

Formalization scope

Lean uses ZMod 2 for $\mathbb F_2$ , Fin \Delta for each coordinate set, and functions on $A\times B$ for matrices. Rows are indexed by $A$ and belong to $C_B$ ; columns are indexed by $B$ and belong to $C_A$ . The published TillichZemor.HGP.Setting supplies the parity-check kernel and the extended-natural minimum distance, whose value is infinity for the zero code. CodingTheory is a published prerequisite. Local definitions give the row and column codes, their sum, puncturing, robustness, uniform finite probability, generator row span, and binary entropy in bits.

The printed matrix sizes $\rho_A\Delta$ and $(1-\rho_B)\Delta$ need integer values. The chosen floor and ceiling keep their respective dimensions within the bounds used in the appendix. Every logarithm in the formalized appendix bounds means $\log_2$ , including occurrences printed simply as $\log$ . Theorem 30 includes an explicit sufficiently-large- $\Delta$ threshold, as its proof's asymptotic count requires, and carries the appendix's preceding entropy condition $\delta<h^{-1}(1-\rho)$ as $\delta<1/2$ and $h_2(\delta)<1-\rho$ . Lemmas 25, 26, and 29 use the preceding condition $d>2\alpha\Delta$ ; the symbol beside $\Delta$ in the scan is ambiguous, and the argument on p. 29 determines this reading. These choices are recorded for audit in MODERATION_NOTES.md.

The probability space is all matrices of each stated size, with the two matrices in Theorem 9 sampled independently. There is no conditioning on a favorable code or an assumed version of Theorem 30 in the goal. The mission does not formalize the later quantum Tanner code construction or the cited Gilbert–Varshamov result as an additional item. Contributions proving the goal, the numbered milestones, or reusable rank and finite-probability facts are within scope.

Selected references

Anthony Leverrier and Gilles Zémor, Quantum Tanner codes, arXiv:2202.13641v3, 2022. Preprint.
Pavel Panteleev and Gleb Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, arXiv:2111.03654, 2021. Preprint.

13 thms2 active usersReviewed

Linear algebra Quantum Error Correction Quantum Information·Captain: mikedeng1

Reversing quantum dynamics with near-optimal quantum and classical fidelity I: The Reversal Operation Attains at Least the Square of the Optimal Average Entanglement FidelityResearch Paper

Motivation

Quantum error correction and quantum communication both ask the same question: after a known noise process $\mathcal A$ has acted on a quantum system, how well can its effect be undone? For a given noise model the best recovery is the solution of a semidefinite program, which gives a number but no structure and no formula. Barnum and Knill showed in 2000 that a single, explicit recovery map, built from $\mathcal A$ and the input state alone, is always close to the best one: its fidelity is at least the square of the optimal fidelity (arXiv:quant-ph/0004088). The map they use is now usually called the Petz recovery map or transpose channel; Petz had introduced it in operator-algebraic work on sufficiency (Petz 1986; Petz 1988). Near-optimality results of this kind underlie approximate quantum error correction and the later theory of recoverability in quantum information.

Timeline.

1986–1988, D. Petz: the map $\rho^{1/2}\mathcal A^\dagger(\mathcal A(\rho)^{-1/2}\,\cdot\,\mathcal A(\rho)^{-1/2})\rho^{1/2}$ characterizes when a channel can be reversed exactly on a family of states.
2002, Barnum and Knill (J. Math. Phys. 43, 2097; doi:10.1063/1.1459754): in the published version, the reversal operation achieves at least the square of the optimal entanglement fidelity for a single input state.
arXiv v2 of the same paper (the source of this mission): the published Eq. (34) had dropped the ensemble weights; with that corrected, the bound holds for the average entanglement fidelity of any ensemble of commuting density matrices (Acknowledgments, p. 14).

Setting

A finite-dimensional quantum system is described by complex $n\times n$ matrices; $X^\dagger$ is the conjugate transpose, and a density matrix is a positive semidefinite matrix of trace one. A completely positive map $\mathcal A$ is given by a finite decomposition $\mathcal A\sim\{A_i\}_i$ of matrices and acts by

\mathcal A(X)=\sum_iA_iXA_i^\dagger .

It is trace-preserving if $\sum_iA_i^\dagger A_i=I$ and trace-nonincreasing if $\sum_iA_i^\dagger A_i\le I$ in the Loewner order. The composite $\mathcal R\mathcal A$ has decomposition $\{R_kA_i\}_{(k,i)}$ .

For a state $\rho$ the paper defines the reversal operation

\mathcal R_{\mathcal A,\rho}\sim\{\rho^{1/2}A_i^\dagger\,\mathcal A(\rho)^{-1/2}\}_i,

under the standing assumption that $\mathcal A(\rho)$ has full support. Here $X^{-1/2}$ is the generalized inverse square root: invert the square roots of the non-zero eigenvalues and keep the zero eigenvalues.

Fidelities are measured by the entanglement fidelity $F_e(\rho,\mathcal K)=\sum_k|\operatorname{tr}K_k\rho|^2$ of a map $\mathcal K\sim\{K_k\}_k$ and, for an ensemble $E=\{p_l,\rho_l\}_l$ (weights $p_l\ge0$ summing to one, density matrices $\rho_l$ ), by the average entanglement fidelity

\bar F_e(E,\mathcal K)=\sum_lp_lF_e(\rho_l,\mathcal K).

When $\rho=\sum_ip_i|i\rangle\langle i|$ in an orthonormal eigenbasis, the classical fidelity is $F_{\mathrm{cl}}(\rho,\mathcal K)=\sum_ip_i\langle i|\mathcal K(|i\rangle\langle i|)|i\rangle$ , the average entanglement fidelity of the ensemble of eigenstates.

Formalization targets

Goal: Theorem 3 (p. 7)

Let $\mathcal A$ be trace-preserving, $E=\{p_l,\rho_l\}_l$ an ensemble of pairwise commuting density matrices, $\rho=\sum_lp_l\rho_l$ , and assume $\mathcal A(\rho)$ has full support. Then for every trace-preserving completely positive $\mathcal R$ ,

\bar F_e(E,\mathcal R_{\mathcal A,\rho}\mathcal A)\;\ge\;\bar F_e(E,\mathcal R\mathcal A)^2 .

Milestones

The milestones follow the paper's proof:

Lemma 1 (p. 7): $\mathcal R_{\mathcal A,\rho}$ depends only on the map $\mathcal A$ , not on its decomposition.
(14)–(15) (p. 7): after replacing $R_k$ by $P_CR_k$ ( $P_C$ the support projector of $\rho$ ), which leaves $\bar F_e$ unchanged and makes $\mathcal R$ trace-nonincreasing, each $R_k=\rho^{1/2}B_k^\dagger\mathcal A(\rho)^{-1/2}$ , and $\mathcal B(\rho)\le\mathcal A(\rho)$ .
(28)–(32) (p. 9): $\sum_lp_l\sum_i|\operatorname{tr}\rho_lR^l_iB^l_i|^2\le\sum_lp_l\sum_{i,j}\operatorname{tr}R^l_iB^l_j\rho_lB_j^{l\dagger}R_i^{l\dagger}$ .
(33)–(34) (p. 9): that sum equals $\operatorname{tr}\mathcal R(\mathcal B(\rho))\le\operatorname{tr}\mathcal R(\mathcal A(\rho))\le1$ .

Two companions are also posed: Proposition 2, $\mathcal R_{\mathcal A,\rho}(\mathcal A(\rho))=\rho$ , and Corollary 4, $F_{\mathrm{cl}}(\rho,\mathcal R\mathcal A)\le\sqrt{F_{\mathrm{cl}}(\rho,\mathcal R_{\mathcal A,\rho}\mathcal A)}$ and $F_e(\rho,\mathcal R\mathcal A)\le\sqrt{F_e(\rho,\mathcal R_{\mathcal A,\rho}\mathcal A)}$ .

Significance

The result. Theorem 3 says that the error $1-\bar F_e$ of the reversal operation is at most twice the optimal error, since $(1-\eta)^2\ge1-2\eta$ . It gives a closed-form recovery whose performance is within a factor two in error of the semidefinite optimum, for every noise process and every commuting ensemble. Taking the ensemble of eigenstates of $\rho$ (Corollary 4) gives the same guarantee for classical information sent through a quantum channel; the companion mission (II of this series) applies the construction to state discrimination, where the reversal operation is the pretty good measurement.

Formalizing it. The result is proved on paper; none of it has a machine-checked proof that we know of. The mission asks for the full argument: the decomposition independence of the reversal map, the reduction to the support of $\rho$ , the singular-value change of decomposition (17)–(18), the chain (19)–(26) of Cauchy–Schwarz inequalities, and the normalization (27)–(34). It also fixes in Lean the arXiv v2 statement (commuting ensembles), which is stronger than the published one.

Difficulty

The obvious approach is to compare $\mathcal R_{\mathcal A,\rho}$ with an optimal $\mathcal R$ term by term. That fails: the fidelity of $\mathcal R\mathcal A$ is a sum of squared traces mixing the decompositions of $\mathcal R$ and $\mathcal A$ , and no termwise inequality relates it to the fidelity of $\mathcal R_{\mathcal A,\rho}\mathcal A$ . The paper first rewrites every recovery in the shape of the reversal map, then chooses, for each ensemble member separately, new decompositions of $\mathcal A$ and $\mathcal B$ that diagonalize a coefficient matrix; making that choice legitimate needs the unitary freedom of Kraus decompositions, which Mathlib does not have. The commutation $[\rho,\rho_l]=0$ is used to move fractional powers of $\rho$ and $\rho_l$ past each other inside traces; without commutation the authors do not know whether the theorem holds (p. 10).

Formalization scope

Matrices are Matrix n n ℂ over a finite type n with decidable equality; Loewner order, square roots and functional calculus come from Mathlib (open scoped MatrixOrder). The map $X\mapsto\sum_iA_iXA_i^\dagger$ is the published PeresTerno.krausUpdate, referenced, not redefined.
Maps are unbundled Kraus families over arbitrary finite index types. The recovery $\mathcal R$ in Theorem 3 ranges over every finite family with $\sum_kR_k^\dagger R_k=I$ .
$X^{-1/2}$ is cfc (fun x => (Real.sqrt x)⁻¹) X, the generalized inverse; Mathlib's junk matrix inverse is not used. The support projector is the functional calculus of the indicator of $x\ne0$ .
$F_e$ is defined by the formula (8), which the paper derives from its purification definition. $F_{\mathrm{cl}}$ takes an orthonormal eigenbasis and weights as data, with $\rho=\sum_ip_i|i\rangle\langle i|$ as a hypothesis.
Standing hypotheses, all from the paper: $\mathcal A$ trace-preserving (§II's noise model); $\mathcal A(\rho)$ positive definite (full support, p. 7); the ensemble is a probability vector of pairwise commuting density matrices with $\rho=\sum_lp_l\rho_l$ .
In (34) the page prints $\operatorname{tr}\mathcal R(\mathcal A(\rho))=1$ ; after the replacement $R_k\mapsto P_CR_k$ the map is only trace-nonincreasing, so the milestone states $\le1$ .
Trivializing encodings are ruled out: the reversal family is the literal formula (12) for the given $\mathcal A$ and the ensemble's own $\rho$ , and the fidelity of a composite map is (8) applied to the composite decomposition $\{R_kA_i\}$ , never the right-hand side of the proof's chain.
Infrastructure a complete development needs, reusable beyond this mission: the unitary freedom of Kraus decompositions, the singular value decomposition of a complex square matrix, the trace Cauchy–Schwarz inequality for Hilbert–Schmidt products, and functional-calculus identities such as $\rho^{1/2}\rho^{-1/2}=P_C$ . Contributions of any of these as separate theorems are welcome. The pure-state, measurement form $P_{\mathrm{opt}}^2\le P_{\mathrm{PGM}}\le P_{\mathrm{opt}}$ is already posed on the platform as QAlgorithms.Arunachalam.barnumKnill and is not repeated here.

Selected references

H. Barnum, E. Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, arXiv:quant-ph/0004088v2. https://arxiv.org/abs/quant-ph/0004088
H. Barnum, E. Knill, same title, J. Math. Phys. 43, 2097 (2002). https://doi.org/10.1063/1.1459754
D. Petz, Sufficient subalgebras and the relative entropy of states of a von Neumann algebra, Commun. Math. Phys. 105, 123–131 (1986). https://doi.org/10.1007/BF01212345
D. Petz, Sufficiency of channels over von Neumann algebras, Quart. J. Math. 39, 97–108 (1988). https://doi.org/10.1093/qmath/39.1.97
B. Schumacher, Sending entanglement through noisy quantum channels, Phys. Rev. A 54, 2614 (1996). https://doi.org/10.1103/PhysRevA.54.2614
R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press (1985), §7.3. https://doi.org/10.1017/CBO9780511810817

7 thms2 active usersReviewed

Linear algebra Quantum Error Correction·Captain: mikedeng1

Quantum LDPC Codes with Positive Rate and Minimum Distance Proportional to n^{1/2}: The Hypergraph Product of a Full-Rank [n,k,d] Parity-Check Matrix with Itself Is an [[n²+(n−k)², k², d]] CSS CodeResearch Paper

Motivation

Quantum computers need error correction, and the codes that are cheapest to run in hardware are quantum low-density parity-check (LDPC) codes: every check involves a bounded number of qubits, and every qubit takes part in a bounded number of checks. For a long time the only well-understood quantum LDPC codes were surface codes such as Kitaev's toric code, whose minimum distance grows like the square root of the length but which encode a fixed number of qubits, so their rate tends to zero. Tillich and Zémor (arXiv:0903.0566; IEEE Transactions on Information Theory, 2014; preliminary version ISIT 2009) gave the first general construction of quantum LDPC codes with positive rate and minimum distance proportional to $\sqrt N$ , from any classical LDPC code. Their hypergraph product became the standard building block of the field.

Timeline.

1996: Calderbank–Shor and Steane introduce CSS codes, quantum codes built from two classical binary codes (quant-ph/9512032, quant-ph/9601029).
1997: Kitaev's toric code: LDPC, distance $\Theta(\sqrt N)$ , dimension 2 (quant-ph/9707021).
2009: Tillich and Zémor: the hypergraph product, with positive rate and distance $\Theta(\sqrt N)$ (this mission).
2020–2021: distance beyond $\sqrt N$ for quantum LDPC codes: $\sqrt N\log N$ by Evra, Kaufman and Zémor (arXiv:2004.07935); $N^{3/5}$ up to polylogarithmic factors by Hastings, Haah and O'Donnell (arXiv:2009.03921).
2022: Panteleev and Kalachev construct asymptotically good quantum LDPC codes, using lifted products that generalize the hypergraph product (arXiv:2111.03654).

Setting

All codes are binary linear codes, subspaces of $\mathbb F_2^{\iota}$ for a finite coordinate set $\iota$ . The Hamming weight $|x|$ of $x$ is its number of nonzero coordinates. The minimum distance $d(\mathcal C)$ of a code is the least weight of a nonzero codeword, with the convention $d(\{0\})=\infty$ .

A Tanner graph $\mathcal G=\mathcal T(V,C,E)$ is the bipartite graph of a parity-check matrix $H\in\mathbb F_2^{C\times V}$ : the variable nodes $V$ index the columns, the check nodes $C$ index the rows, and $c\sim v$ iff $H_{cv}=1$ . Its code is $\mathcal C=\ker H$ . The transpose Tanner graph $\mathcal G^T$ is that of $H^T$ , and its code $\mathcal C^T=\ker H^T$ is the transpose code. It depends on the matrix $H$ , not only on $\mathcal C$ .

A CSS code is a pair $(\mathcal C_X,\mathcal C_Z)$ of codes of the same length $N$ with $\mathcal C_Z^\perp\subseteq\mathcal C_X$ . Its quantum dimension and quantum minimum distance are

k_Q=\dim(\mathcal C_X/\mathcal C_Z^\perp),\qquad d_Q=\min(d_X,d_Z),\quad d_X=\min\{|x|:x\in\mathcal C_X\setminus\mathcal C_Z^\perp\},

with $d_Z$ defined symmetrically and $\min\emptyset=\infty$ .

Given $H_1\in\mathbb F_2^{C_1\times V_1}$ and $H_2\in\mathbb F_2^{C_2\times V_2}$ with Tanner graphs $\mathcal G_1,\mathcal G_2$ , the code $\mathcal Q(\mathcal G_1\times\mathcal G_2)$ has qubits $(V_1\times V_2)\sqcup(C_1\times C_2)$ and check matrices

H_X=\big(H_1\otimes I_{V_2}\ \big|\ I_{C_1}\otimes H_2^T\big),\qquad H_Z=\big(I_{V_1}\otimes H_2\ \big|\ H_1^T\otimes I_{C_2}\big),

with $\mathcal C_X=\ker H_X$ and $\mathcal C_Z=\ker H_Z$ . Write $k_i=\dim\mathcal C_i$ , $k_i^T=\dim\mathcal C_i^T$ , $d_i=d(\mathcal C_i)$ and $d_i^T=d(\mathcal C_i^T)$ .

Formalization targets

Goal: Theorem 1 (p. 3)

Let $H$ be a full-rank $(n-k)\times n$ parity-check matrix of an $[n,k,d]$ code. The code $\mathcal Q(\mathcal G\times\mathcal G)$ built from two copies of its Tanner graph is a CSS code with

N=n^2+(n-k)^2,\qquad k_Q=k^2,\qquad d_Q=d,

and each row of $H_X$ and $H_Z$ has weight $i+j$ , with $i$ a row weight and $j$ a column weight of $H$ .

General results

Proposition 14 (dimension): $k_Q=k_1k_2+k_1^Tk_2^T$ for any two Tanner graphs.
Theorem 15 (distance): $d_Q\ge m:=\min(d_1,d_2,d_1^T,d_2^T)$ , with $d_Q=m$ whenever $d_i=m$ and $d_{3-i}\ne\infty$ , or $d_i^T=m$ and $d_{3-i}^T\ne\infty$ , for some $i\in\{1,2\}$ .

The milestones follow the paper. They are Proposition 4 (validity), eq. (4), Fact 12 and Propositions 9, 10, 13 (product codes and transposes), which lead to Proposition 14. Then come eq. (17), the weight claim and Lemma 16 (lower bound), and the two claims of p. 17 and Lemma 17 (upper bound), which lead to Theorem 15. The degree count of p. 11 gives the row weights.

Significance

The result. The construction needs no orthogonality between the input codes: any two parity-check matrices give a valid CSS code. Its parameters are read off the classical inputs. A family of classical LDPC codes with fixed rate and linear distance therefore gives quantum LDPC codes with fixed rate and distance $\Theta(\sqrt N)$ , and sparse inputs give sparse stabilizers. The toric code is the special case where both inputs are cycle graphs. The hypergraph product is also the base case of the later homological and lifted-product constructions, and the source of the standard decoding and fault-tolerance results for these codes.

Formalizing it. The theorem is proved in the paper; what is missing is a machine-checked proof. The platform holds the toric code's distance and dimension (ToricCode.toric_distance, ToricCode.toric_homologyRank), but over its own chain complex, not over a general construction. This mission produces a reusable layer: Tanner graphs as binary matrices, CSS dimension and distance with the $\infty$ convention, product codes, and the parameters of the hypergraph product for arbitrary finite index sets.

Difficulty

The dimension count is linear algebra once the codes $\ker H_X^T$ and $\ker H_Z^T$ have been identified with product codes. The obstacle is the distance. Lower bounds on the minimum weights of $\mathcal C_X$ and $\mathcal C_Z$ themselves are useless: $\mathcal C_Z^\perp\subseteq\mathcal C_X$ contains the rows of $H_Z$ , which have constant weight, so the minimum weight of $\mathcal C_X$ is bounded by a constant. Any bound of order $\min(d_1,d_2,d_1^T,d_2^T)$ must use the definition of $d_X$ over $\mathcal C_X\setminus\mathcal C_Z^\perp$ and show that every low-weight codeword of $\mathcal C_X$ is degenerate, i.e. lies in $\mathcal C_Z^\perp$ . The upper bound needs an explicit codeword of $\mathcal C_X$ outside $\mathcal C_Z^\perp$ , and showing that it is not in $\mathcal C_Z^\perp$ requires an argument of its own.

Formalization scope

Lean represents a Tanner graph by its matrix H : Matrix C V (ZMod 2) over arbitrary finite index types. The code is ker H, the transpose code is ker Hᵀ, and the dual code is CodingTheory.dualCode from the published definition CodingTheory. Hamming weight is Mathlib's hammingNorm. Minimum distances live in ℕ∞, where the empty infimum is ⊤, the paper's $\infty$ . $k_Q$ is the dimension of the quotient of $\mathcal C_X$ by $\mathcal C_Z^\perp\cap\mathcal C_X$ . In $H_X$ and $H_Z$ the qubits are ordered $(V_1\times V_2)\sqcup(C_1\times C_2)$ , as on p. 18. A product code is a set of $\iota_1\times\iota_2$ matrices whose columns (fixed second coordinate) lie in the first code. The general results are stated without nonemptiness assumptions; they hold for empty index sets.

Theorem 1 has two disclosed differences from the page:

It adds the hypothesis $k\le n$ , which is implicit in " $[n,k,d]$ ". Without it the matrix has no rows and the dimension claim fails.
It drops the word "LDPC", a property of families of codes. Its finite content is the row-weight clause, which is kept.

"There is a construction" is formalized as the paper's construction, the hypergraph product of $H$ with itself.

Several encodings would trivialize the statements and are excluded: an $\mathbb N$ -valued minimum distance that is $0$ on the zero code; $d_X$ taken over $\mathcal C_X\setminus\{0\}$ instead of $\mathcal C_X\setminus\mathcal C_Z^\perp$ ; $k_Q$ computed by truncated natural subtraction; an existential "there is a code with these parameters"; and the transpose code replaced by the dual code.

A complete development needs ranks and kernels of Kronecker products over $\mathbb F_2$ , dimensions of product codes (Proposition 9, not in Mathlib), and the restriction of Tanner graphs to induced subgraphs. The product-code and CSS layers are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for Proposition 14 via the Künneth formula.

Selected references

J.-P. Tillich and G. Zémor, Quantum LDPC codes with positive rate and minimum distance proportional to the square root of the blocklength, IEEE Transactions on Information Theory 60(2), 2014; preprint arXiv:0903.0566v2. https://arxiv.org/abs/0903.0566 , https://doi.org/10.1109/TIT.2013.2292061
A. R. Calderbank and P. W. Shor, Good quantum error-correcting codes exist, Physical Review A 54, 1996. https://arxiv.org/abs/quant-ph/9512032
A. M. Steane, Multiple particle interference and quantum error correction, Proceedings of the Royal Society A 452, 1996. https://arxiv.org/abs/quant-ph/9601029
A. Yu. Kitaev, Fault-tolerant quantum computation by anyons, Annals of Physics 303, 2003. https://arxiv.org/abs/quant-ph/9707021
F. J. MacWilliams and N. J. A. Sloane, The Theory of Error-Correcting Codes, North-Holland, 1977, Ch. 18 §2 (product codes).
S. Evra, T. Kaufman and G. Zémor, Decodable quantum LDPC codes beyond the √n distance barrier using high-dimensional expanders, FOCS 2020. https://arxiv.org/abs/2004.07935
M. B. Hastings, J. Haah and R. O'Donnell, Fiber bundle codes: breaking the N^{1/2} polylog(N) barrier for quantum LDPC codes, STOC 2021. https://arxiv.org/abs/2009.03921
P. Panteleev and G. Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, STOC 2022. https://arxiv.org/abs/2111.03654
N. P. Breuckmann and J. N. Eberhardt, Quantum low-density parity-check codes, PRX Quantum 2, 2021. https://arxiv.org/abs/2103.06309

18 thms2 active usersReviewed

Algebra Combinatorics Discrete Geometry·Captain: mikedeng1

A Large Family of Maximum Scattered Linear Sets of PG(1, q^n) and Their Associated MRD Codes 2: For Odd q = p^r and t > 4, a Lower Bound on the Number of PΓL-Classes of the Linear Sets L_{h,t}Research Paper

Motivation

A linear set of the projective line $\mathrm{PG}(1, q^n)$ is the set of points $\langle u\rangle_{\mathbb F_{q^n}}$ spanned by the nonzero vectors $u$ of an $\mathbb F_q$ -subspace $U \subseteq \mathbb F_{q^n}^2$ . The extremal ones, the maximum scattered linear sets, are given by scattered polynomials $f$ over $\mathbb F_{q^n}$ , and each such $f$ also gives an $\mathbb F_{q^n}$ -linear maximum rank-distance (MRD) code $\mathcal C_f = \{ax + bf(x) : a, b \in \mathbb F_{q^n}\}$ of minimum distance $n-1$ (Sheekey, Adv. Math. Commun. 10, 2016). Rank-distance codes are used in network coding, and linear sets appear in the study of semifields, blocking sets and two-intersection sets.

Linear sets and codes are classified up to equivalence: two linear sets are the same object if a collineation of the line, an element of $\mathrm{P\Gamma L}(2, q^n)$ , maps one onto the other. The question is therefore not only whether new scattered polynomials exist but how many inequivalent linear sets they produce.

2000–2001. The monomials $x^{q^s}$ , $\gcd(s,n) = 1$ (Blokhuis–Lavrauw 2000), all give a single linear set of $\mathrm{PG}(1,q^n)$ (pseudoregulus type); the binomials $\delta x^{q^s} + x^{q^{n-s}}$ (Lunardon–Polverino 2001) give at most $\varphi(n)$ times a function of $q$ classes.
2018. Csajbók, Marino and Polverino (J. Combin. Theory Ser. A 157, 2018) develop the equivalence theory of linear sets of $\mathrm{PG}(1, q^n)$ , including coefficient identities that two $q$ -polynomials defining the same linear set must satisfy.
2021. Longobardi and Zanella (J. Algebraic Combin. 2021) give a third family, again with at most $\varphi(n)/2$ classes.
2021. Longobardi, Marino, Trombetti and Zhou (arXiv:2102.08287v3) construct the family $\psi_{h,t}$ (Theorem 3.1, the companion mission) and show (Theorem 5.1) that it contains a number of $\mathrm{P\Gamma L}$ -classes growing exponentially in $n$ . This mission formalizes that count.

Setting

Let $p$ be an odd prime, $r \ge 1$ , $q = p^r$ , $t \ge 1$ , $n = 2t$ , and let $F = \mathbb F_{q^n}$ be the finite field of order $q^{2t}$ . Its subfield $\mathbb F_q$ is $\{c : c^q = c\}$ .

A $q$ -polynomial is a map $f(x) = \sum_{i=0}^{n-1} \alpha_i x^{q^i}$ with $\alpha_i \in F$ (qpoly). It is scattered (IsScatteredPoly) if for all $z, y \in F^*$ , $f(z)/z = f(y)/y$ forces $z = cy$ with $c \in \mathbb F_q$ .

The graph of $f$ is $U_f = \{(x, f(x)) : x \in F\} \subseteq F^2$ (graph). A point $\langle v \rangle_{\mathbb F_{q^n}}$ of $\mathrm{PG}(1, q^n)$ is the set of all $F$ -multiples of a nonzero $v \in F^2$ (point), and the linear set of $f$ is the point set

L_f = \{\langle (x, f(x))\rangle_{\mathbb F_{q^n}} : x \in F^*\} \quad (\texttt{linSet}).

For a field automorphism $\sigma$ and an invertible $2 \times 2$ matrix $A$ over $F$ , the map $v \mapsto A v^\sigma$ ( $\sigma$ acting on coordinates, act) is an element of $\Gamma\mathrm L(2, q^n)$ ; with $\sigma = \mathrm{id}$ it is in $\mathrm{GL}(2, q^n)$ . Two subsets $U, W \subseteq F^2$ are GL- or ΓL-equivalent (GLEquiv, GammaLEquiv) if such a map sends $U$ onto $W$ . Two point sets are PGL- or PΓL-equivalent (PGLEquiv, PGammaLEquiv) if the induced map on points, $P \mapsto \{A v^\sigma : v \in P\}$ , sends one onto the other.

The family. For $h \in F$ ,

\psi_{h,t}(x) = x^q + x^{q^{t-1}} - h^{1-q^{t+1}} x^{q^{t+1}} + h^{1-q^{2t-1}} x^{q^{2t-1}} \quad (\texttt{psi}),

$H = \{h \in F : h^{q^t+1} = -1\}$ (hSet), $U_h = U_{\psi_{h,t}}$ and $L_{h,t} = L_{\psi_{h,t}}$ . For $t \ge 3$ and $h \in H \setminus \mathbb F_{q^t}$ , $\psi_{h,t}$ is scattered and $L_{h,t}$ is a maximum scattered linear set (Theorem 3.1).

Formalization targets

Goal: Theorem 5.1

For $t > 4$ , the number $M$ of $\mathrm{P\Gamma L}(2,q^n)$ -classes met by the sets $L_{h,t}$ , $h \in H$ , satisfies

M \ge \begin{cases} \left\lfloor \dfrac{q^t+1}{8rt} \right\rfloor, & t \not\equiv 2 \pmod 4,\\[1.5ex] \left\lfloor \dfrac{q^t+1}{4rt(q^2+1)} \right\rfloor, & t \equiv 2 \pmod 4.\end{cases}

It is stated as: some $S \subseteq H$ of at least that size has pairwise $\mathrm{P\Gamma L}$ -inequivalent $L_{h,t}$ . The goal fixes the paper's constants; the proof on p. 26 in fact counts classes exactly in terms of class sizes, so a sharper bound is a natural follow-up.

Milestones

Proposition 3.2 (p. 7): $h \in H \Rightarrow h^{q^2+1} \ne 1$ and $h^{q^{t-2}} \ne -h$ .
$|H| = q^t + 1$ (p. 26).
Display (29) (p. 16): for $h, k \in H$ , $U_h \sim_{\mathrm{GL}} U_k$ iff $h = \pm k$ ( $t \not\equiv 2$ ) or $h = \ell k$ with $\ell^{q^2+1} = 1$ ( $t \equiv 2 \bmod 4$ ).
Theorem 4.2 (a)–(b) (p. 16), in the $U_h$ form: $U_h \sim_{\Gamma\mathrm L} U_k$ iff $h = \pm k^\rho$ (resp. $\ell k^\rho$ ) for some $\rho \in \mathrm{Aut}(\mathbb F_{q^n})$ .
Proof of Corollary 4.3 (p. 18): the GL-class of $U_h$ in the family has $\xi_h = 2$ (resp. $q^2+1$ ) members, and its ΓL-class at most $nr\xi_h$ .
Lemma 2.2 (p. 5, from Csajbók–Marino–Polverino): $L_f = L_g$ forces $\alpha_0 = \beta_0$ and two families of coefficient identities.
Display (37) (pp. 20–21): PGL-equivalence of $L_f, L_g$ as an equality of sets of quotients.
The case $b = 0$ of (37) (p. 21): $c = 0$ .
Lemma 5.2 (p. 21): the case $b = 0$ for $\psi_{h,t}, \psi_{k,t}$ gives $(h/k)^{q^2+1} = 1$ and $U_h \sim_{\Gamma\mathrm L} U_k$ .
Lemma 5.3 (p. 22): the case $b = 1$ , with its three conclusions.

Significance

The result. Theorem 5.1 shows that maximum scattered linear sets of $\mathrm{PG}(1, q^n)$ , and hence $\mathbb F_{q^n}$ -linear MRD codes, exist in numbers exponential in $n$ up to equivalence, whereas each previously known infinite family yields at most $\varphi(n)$ times a function of $q$ classes (Table 1, p. 3). Remark 5.4 draws the consequence that the family is new. Its intermediate results, the classification of the $\mathrm{GL}$ - and $\Gamma\mathrm L$ -equivalences between the $U_h$ (Theorem 4.2) and the reduction of $\mathrm{PGL}$ -equivalence to sets of quotients, are the standard tools for any later classification of this family.

Formalizing it. The theorem has a complete published proof; none of it is machine-checked. The platform has no action of $\mathrm{GL}(2, q^n)$ or $\Gamma\mathrm L(2, q^n)$ on the projective line, no linear sets of $\mathrm{PG}(1,q^n)$ as point sets, and no coefficient identities for $q$ -polynomials defining the same linear set. The mission produces these, then the class counts. Lemma 2.2 is a result of an earlier paper (Csajbók–Marino–Polverino 2018) cited without proof, so formalizing it means formalizing part of that paper too.

Difficulty

Equality of two linear sets is equality of sets of points, which says nothing directly about the polynomials: different $q$ -polynomials can define the same linear set (all $x^{q^s}$ with $\gcd(s,n)=1$ do). The obvious idea, that $\mathrm{P\Gamma L}$ -equivalent linear sets come from $\Gamma\mathrm L$ -equivalent subspaces $U_h$ , fails in general (p. 3), so the count cannot be read off Theorem 4.2. The step that needs the restriction $t > 4$ is the comparison of coefficients in the $q$ -polynomial identities, which for $t = 3, 4$ is open (Remark 5.5). A second difficulty is bookkeeping: the exponents $q^{t\pm1}$ , $q^{2t-1}$ , the negative powers of $h$ and the case split on $t \bmod 4$ must all be tracked through every identity.

Formalization scope

Field. $F$ is a finite field with CharP F p, p prime, Odd p (" $q$ odd"), q = p ^ r with 0 < r, and Fintype.card F = q ^ (2 * t). $r$ is the exponent of $q = p^r$ , as in Theorem 5.1, so $|\mathrm{Aut}(\mathbb F_{q^n})| = rn$ . Lemma 2.2, (37) and the $b = 0$ step are stated for general $n \ge 1$ and Fintype.card F = q ^ n, without " $q$ odd", as printed.
Exponents. $x^{q^i}$ is x ^ q ^ i; negative powers of $h$ are field quotients (h / h ^ q ^ (t+1) for $h^{1-q^{t+1}}$ ), exact since $h \ne 0$ on $H$ . Natural-number subtractions $t-1$ , $2t-1$ , $3t-2$ , $n-k$ , $q^i - 1$ are exact in the stated ranges.
Geometry. The plane is Fin 2 → F; points are sets of scalar multiples; linear sets are sets of points. Equivalences are stated as images of sets under $v \mapsto A v^\sigma$ with $\det A$ a unit and $\sigma : F \simeq F$ a ring automorphism.
Pinned readings.
1. "Scattered" is the p. 2 quotient definition with $\mathbb F_q = \{c : c^q = c\}$ .
2. Proposition 3.2's $h^{q^{t-2}}$ is read as $h^{q^{3t-2}}$ (equal for $t \ge 2$ ), and " $q$ odd" is added.
3. Theorem 4.2 (a)–(b), stated for codes $\mathcal C_{h,t}$ , is formalized as the $\Gamma\mathrm L$ -equivalence of $U_h, U_k$ , which the proof establishes and which is the code equivalence by Theorem 2.1 (from Sheekey 2016). The automorphism-group sentence is omitted.
4. Lemma 5.3's hypothesis "(41) holds" is read in the setting of p. 21: $b = 1$ , $\bar c = c - da \ne 0$ , $\bar g = \sum \gamma_i y^{q^i}$ inverse to $x \mapsto ax + g(x)$ (47), and $d + \bar c\gamma_0 = 0$ (40).
5. In (37), $ax + bg(x) \ne 0$ for $x \ne 0$ is part of the condition (stated on p. 21 for $b = 1$ ).
6. "The total number $M$ of inequivalent $L_{h,t}$ " is the number of classes met by $\{L_{h,t} : h \in H\}$ , formalized through a pairwise-inequivalent subset of $H$ . $H$ is not restricted to $h \notin \mathbb F_{q^t}$ , as in the count $|H| = q^t+1$ of p. 26; "maximum scattered" is descriptive.
Trivializing formalizations ruled out. Equivalence is stated on point sets, never on quotient sets $\{f(x)/x\}$ , where Lean's $y/0 = 0$ could merge inequivalent sets; the goal requires pairwise inequivalence, not distinctness of the parameters $h$ (note $\psi_{-h,t} = \psi_{h,t}$ ); and the hypotheses are satisfiable, with bound $\lfloor 244/40 \rfloor = 6$ at $q = 3$ , $t = 5$ .
Citation basis. All indices and pages refer to arXiv:2102.08287v3 (printed page = PDF page). The Combinatorica version is not used.
Welcome contributions. The $\Gamma\mathrm L(2,q^n)$ action on $F^2$ and on point sets, the cardinality of $\{h : h^{q^t+1} = -1\}$ , and Lemma 2.2 are reusable beyond this mission. Proofs of any milestone, and of Theorem 3.1 in the companion mission, are welcome.

Selected references

G. Longobardi, G. Marino, R. Trombetti, Y. Zhou, A large family of maximum scattered linear sets of PG(1, q^n) and their associated MRD codes, arXiv:2102.08287v3, 2021 (Combinatorica 43, 2023). https://arxiv.org/abs/2102.08287v3
B. Csajbók, G. Marino, O. Polverino, Classes and equivalence of linear sets in PG(1, q^n), J. Combin. Theory Ser. A 157, 402–426, 2018.
J. Sheekey, A new family of linear maximum rank distance codes, Adv. Math. Commun. 10(3), 475–488, 2016.
G. Longobardi, C. Zanella, Linear sets and MRD-codes arising from a class of scattered linearized polynomials, J. Algebraic Combin., 2021. https://doi.org/10.1007/s10801-020-01011-9
A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geometriae Dedicata 81(1), 231–243, 2000.
G. Lunardon, O. Polverino, Blocking sets and derivable partial spreads, J. Algebraic Combin. 14(1), 49–56, 2001.
B. Csajbók, C. Zanella, On the equivalence of linear sets, Des. Codes Cryptogr. 81(2), 269–281, 2016.

13 thms2 active usersReviewed

Probability Quantum Information·Captain: mikedeng1

Semidefinite Programming Hierarchies for Constrained Bilinear Optimization II: De Finetti Without Symmetry — Random Subsystems Are 3k^{3/2}d_B³ log d_B/√(n−k+1)-Close to Product in ExpectationResearch Paper

Motivation

Quantum information often describes a system through a state shared among many small registers. One would like to replace the state on a few registers by a product of their individual states, because product states are easier to estimate and optimize over. The usual finite quantum de Finetti theorems obtain such approximations from permutation symmetry. A physical preparation, however, need not be symmetric. Berta, Borderi, Fawzi and Scholz give a quantitative statement that instead selects the retained registers at random and conditions on measurements of other registers. Their Theorem 2.5 is the target here.

The authors place this result alongside their hierarchy for constrained bilinear optimization, but the theorem without symmetry is independent of the hierarchy. In §2.6 they compare its polynomial dependence on the local dimension and the number of retained registers with the earlier no-symmetry approximation discussed in their reference [12]. The result identifies exactly what random selection and measurement can supply when a global permutation-invariance hypothesis is unavailable.

Setting

Let $B$ be a quantum system of dimension $d_B$ , and let $\rho$ be an arbitrary density operator on $n$ copies of $B$ . Choose a uniformly random permutation of these copies. Its first $k$ positions form an ordered tuple $\vec i=(i_1,\ldots,i_k)$ of systems to retain; the remaining $r=n-k$ positions form an ordered tuple $\vec j=(j_1,\ldots,j_r)$ available for measurement. There is no symmetry condition on $\rho$ .

A measurement on $B$ has finitely many outcomes $z$ and positive operators $M_z$ whose sum is the identity. Measure the first $m$ systems $j_1,\ldots,j_m$ , where $0\le m\le r$ , and condition the retained state on the observed outcomes. Write $\rho_{\vec i\mid z}$ for that conditional state and $\rho_{i_s\mid z}$ for its marginal on the $s$ th retained system. The trace norm $\|X\|_1=\operatorname{Tr}\sqrt{X^\dagger X}$ measures the error between $\rho_{\vec i\mid z}$ and $\rho_{i_1\mid z}\otimes\cdots\otimes\rho_{i_k\mid z}$ . The expectation is over the uniform permutation and the measurement outcomes, with their Born-rule probabilities.

The distortion with side information of a fixed measurement is the largest ratio between an input trace norm and the norm left after measuring only its $B$ factor. The input ranges over Hermitian operators on $A\otimes B$ , over every finite-dimensional side system $A$ , with zero partial trace on both $A$ and $B$ . The paper's $f(B\mid\cdot)$ is the infimum of this distortion over all measurements on $B$ equation (10). A state two-design is a finite family of rank-one projectors whose average second tensor power is the projector onto the symmetric subspace with the normalization in Lemma D.1. The projectors give an explicit measurement with distortion at most $d_B^2(d_B+1)$ .

Formalization targets

The principal target is the explicit form of Theorem 2.5. For $1\le k\le n$ , put $r=n-k$ . With the two-design measurement, some $m\in\{0,\ldots,r\}$ satisfies

\mathbb E_{\vec i,\vec j,z}\left\|\rho_{\vec i\mid z}-\bigotimes_{s=1}^k\rho_{i_s\mid z}\right\|_1 \le k d_B^2(d_B+1)\sqrt{\frac{(2\ln 2)(k-1)\log_2 d_B}{r+1}} \le \frac{3k^{3/2}d_B^3\log_2 d_B}{\sqrt{r+1}}.

Here the $z$ in the expectation is the outcome string for the first $m$ members of $\vec j$ . The same $m$ is chosen before taking that expectation. This rate is stated with its constants and its two consecutive inequalities; an existence assertion without the error bound would lose the theorem's content.

The milestone path also states the telescoping trace-norm inequality of equation (12), the measurement estimate of Lemma D.1, and the final averaged inequality on p. 11. A companion milestone treats any fixed POVM with its own distortion. That formulation captures the proof's arbitrary-measurement step without treating the infimum $f(B\mid\cdot)$ as if every measurement attained it.

Significance

For an arbitrary multipartite state, random ordering and conditioning give one measured prefix length at which the selected registers have small expected distance from a product. The explicit rate is polynomial in $d_B$ and $k$ and decays as $1/\sqrt{n-k+1}$ . It therefore gives a quantitative approximation guarantee under a selection rule that can be applied without first establishing exchangeability Berta et al., §2.6.

The theorem is proved in the paper; the work here is to express its state, measurement, conditional distribution, and norm bound in Lean and to connect the estimate to reusable finite-dimensional quantum-information definitions. The local statements are currently proof obligations, not machine-checked proofs. The published density-operator, trace-norm, and partial-trace definitions are reused. Once proved, the statements can serve as a precise interface for subsequent formal work on randomized subsystem selection and information-theoretic decoupling.

Difficulty

Randomly choosing systems does not turn the original state into a product state. A direct bound on the distance to a product can be large even when each one-system marginal is simple, because correlations among the retained systems remain. Equation (12) breaks the total error into successive correlation terms; the paper controls their average by measuring other systems and using information-theoretic estimates. A second difficulty is that a measurement can erase distinctions between different input operators. The two-design estimate supplies a dimension-dependent bound on that loss, uniformly over the size of a side system.

The printed theorem leaves the measurement $M_B$ unspecified while using the minimum distortion over all measurements. A trivial measurement cannot satisfy that reading. The proof explicitly permits the measurement built from a state two-design, with $d_B^2(d_B+1)$ replacing $f(B\mid\cdot)$ ; that is the measurement used in the goal proof of Theorem 2.5, p. 10.

Formalization scope

The $B$ system has basis Fin dB; $n$ copies have basis Fin n → Fin dB. The formalization writes $n=k+r$ , assumes $k\ge1$ , and ranges over $m\le r$ . A state is a positive semidefinite complex matrix with trace one. Permutations act on the copy coordinates, and their finite uniform average models the paper's random ordered tuples. Measurement outcomes are finite words; the conditional state divides the unnormalized post-measurement state by its probability. A zero-probability outcome uses Lean's zero inverse and contributes zero to the weighted expectation. The existence of a state and of a nonempty two-design rules out zero-dimensional and empty-outcome instances in the goal.

The fixed-measurement distortion and $f(B\mid\cdot)$ take values in extended nonnegative reals, so a measurement that destroys a nonzero operator has infinite distortion. The logarithm is base two except for $\ln 2$ . The definitions use the paper's unnormalized trace norm, with no factor $1/2$ . No mutual-information estimate or Pinsker inequality is assumed in the goal: both belong to possible proofs. Contributions proving the stated milestones, the positivity and normalization of the conditional states, or reusable trace-norm facts for finite tensor products all advance the target.

Selected references

M. Berta, F. Borderi, O. Fawzi and V. B. Scholz, Semidefinite programming hierarchies for constrained bilinear optimization, Mathematical Programming, 2021; arXiv:1810.12197v3.

12 thms2 active usersReviewed

Convex Optimization Optimization Quantum Information·Captain: mikedeng1

Semidefinite Programming Hierarchies for Constrained Bilinear Optimization I: The Linearly Constrained de Finetti SDP Hierarchy Satisfies Q ≤ SDPₙ ≤ Q + ‖G‖∞·d_B²(d_B+1)·√((2 ln 2) log d_A / n)Research Paper

Motivation

Many problems in quantum information theory ask for the maximum of a linear functional over pairs of quantum states, one on each of two systems, subject to linear constraints on each state. The best success probability of an approximate quantum error-correcting code of given size is of this form: the encoder and the decoder are quantum channels, their Choi matrices are states with fixed marginals, and the objective is bilinear in the two (Berta, Borderi, Fawzi & Scholz, arXiv:1810.12197, §4). Such constrained bilinear programs are nonconvex. Seesaw methods give lower bounds that often converge in practice, but they offer no guarantee of global optimality. What is needed is a hierarchy of efficiently computable outer bounds that converges to the optimum, with an explicit rate.

For the unconstrained problem, the optimisation over separable states, such a hierarchy is classical: the Doherty–Parrilo–Spedalieri hierarchy of $n$ -extendible states, whose convergence follows from finite quantum de Finetti theorems (Christandl, König, Mitchison & Renner 2007; Brandão & Harrow 2013). The standard de Finetti approximant is, however, a mixture of product states that need not satisfy the linear constraints, so it says nothing about the constrained problem. The paper proves a de Finetti theorem with linear constraints (Theorem 2.3) and derives from it a semidefinite hierarchy for constrained bilinear programs with a convergence guarantee (Theorem 3.1).

Setting

A $d$ -dimensional quantum system has operator space $\mathcal S=\mathbb C^{d\times d}$ ; a state is a positive semidefinite $W\in\mathcal S$ with $\mathrm{Tr}\,W=1$ . Let $A$ and $B$ be systems of dimensions $d_A$ and $d_B$ . The data are an objective $G_{AB}\in\mathcal S_A\otimes\mathcal S_B$ , arbitrary linear maps $\Lambda_{A\to C_A}:\mathcal S_A\to\mathcal S_{C_A}$ and $\Gamma_{B\to C_B}:\mathcal S_B\to\mathcal S_{C_B}$ , and matrices $X_{C_A}$ , $Y_{C_B}$ . The constrained bilinear program is

Q=\max\ \mathrm{Tr}[G_{AB}(W_A\otimes W_B)]\quad\text{s.t. } W_A,W_B\ \text{states},\quad \Lambda_{A\to C_A}(W_A)=X_{C_A},\quad \Gamma_{B\to C_B}(W_B)=Y_{C_B}.

For $n\ge1$ let $B_1,\dots,B_n$ be copies of $B$ . A state $W_{AB_1^n}$ on $A\otimes B_1\cdots B_n$ is symmetric with respect to $A$ if it is invariant under every permutation $\mathcal U^\pi_{B_1^n}$ of the copies $B_1,\dots,B_n$ , $\pi\in\mathfrak S_n$ . Write $W_{B_1^n}=\mathrm{Tr}_A W_{AB_1^n}$ , $W_{B_1^{n-1}}=\mathrm{Tr}_{B_n}W_{B_1^n}$ and $W_{AB_1}=\mathrm{Tr}_{B_2^n}W_{AB_1^n}$ . The level- $n$ program is

\mathrm{SDP}_n=\max\ \mathrm{Tr}[G_{AB}W_{AB_1}]\quad\text{s.t. } W_{AB_1^n}\ \text{a state, symmetric with respect to } A,

(\Lambda_{A\to C_A}\otimes\mathcal I_{B_1^n})(W_{AB_1^n})=X_{C_A}\otimes W_{B_1^n},\qquad (\mathcal I_{B_1^{n-1}}\otimes\Gamma_{B_n\to C_B})(W_{B_1^n})=W_{B_1^{n-1}}\otimes Y_{C_B}.

It is a semidefinite program of size polynomial in $d_A$ and $d_B^n$ .

The rate involves the trace norm $\|X\|_1=\mathrm{Tr}|X|$ , the Schatten $\infty$ -norm $\|G\|_\infty$ (largest singular value), and the minimal distortion with side information of $B$ ,

f(B|\cdot)=\inf_{\mathcal M_B}\ \sup_{\substack{\xi_{AB}^\dagger=\xi_{AB}\\ \xi_A=0,\ \xi_B=0}}\frac{\|\xi_{AB}\|_1}{\|(\mathcal I_A\otimes\mathcal M_B)(\xi_{AB})\|_1},

the infimum over measurements $\mathcal M_B$ on $B$ and the supremum over all finite-dimensional $A$ ; $f(A,B)$ is the analogue with product measurements $\mathcal M_A\otimes\mathcal M_B$ . Throughout, $\log$ is base 2.

Formalization targets

Goal: Theorem 3.1 with its explicit rate

Q\ \le\ \mathrm{SDP}_n\ \le\ Q+\|G_{AB}\|_\infty\,d_B^2(d_B+1)\sqrt{\frac{(2\ln2)\log d_A}{n}}\quad(n\ge1),\qquad Q=\lim_{n\to\infty}\mathrm{SDP}_n.

The page states $0\le\mathrm{SDP}_n-Q\le\mathrm{poly}(d)/\sqrt n$ with $d=\max\{d_A,d_B\}$ . The goal makes explicit the rate the proof gives.

Milestones, in attack order

Lemma 2.1 (p. 6): for a permutation-invariant classical-quantum state $\rho_{AZ_1^n}$ there is $0\le m<n$ with $\mathbf E_{z_1^m}\|\rho_{AZ_{m+1}|z_1^m}-\rho_{A|z_1^m}\otimes\rho_{Z_{m+1}|z_1^m}\|_1^2\le(2\ln2)\log d_A/n$ .
Lemma D.1 (p. 29): for a state two-design $\{P_z\}$ and $\mathcal M_B$ with effects $\frac{d_B}{t}P_z$ , $\|(\mathcal I_A\otimes\mathcal M_B)(\xi_{AB})\|_1\ge\|\xi_{AB}\|_1/(d_B^2(d_B+1))$ for every Hermitian $\xi_{AB}$ .
Existence of state two-designs in every dimension (p. 29).
$f(B|\cdot)\le d_B^2(d_B+1)$ (p. 6).
Conditional constraints (p. 8): the states obtained by measuring $B_1,\dots,B_m$ and conditioning satisfy $\Lambda(\rho_{A|z_1^m})=X_{C_A}$ and $\Gamma(\rho_{B_{m+1}|z_1^m})=Y_{C_B}$ .
Theorem 2.3 (p. 7): under the constraints of $\mathrm{SDP}_n$ , $\|\rho_{AB}-\sum_ip_i\sigma^i_A\otimes\omega^i_B\|_1\le\min\{f(A,B),f(B|\cdot)\}\sqrt{(2\ln2)\log d_A/n}$ with states $\Lambda(\sigma^i_A)=X_{C_A}$ , $\Gamma(\omega^i_B)=Y_{C_B}$ .
Eq. (3) (p. 2): $Q$ equals the maximum over mixtures of feasible product states.
Hölder step (p. 11): $\mathrm{Tr}[GW]\le\mathrm{Tr}[GV]+\|G\|_\infty\|W-V\|_1$ .
$0\le\mathrm{SDP}_n-Q$ (p. 11).

Significance

Theorem 3.1 turns a nonconvex problem into a sequence of semidefinite programs whose values decrease to the optimum at rate $O(1/\sqrt n)$ , with a constant that depends polynomially on $d_B$ and logarithmically on $d_A$ . Every level is a certified upper bound; together with any feasible point it brackets $Q$ . The same argument applied to channel fidelities gives converging outer bounds on the success probability of approximate quantum error correction (§4 of the paper), and the constrained de Finetti theorem is the key step there as well. Theorem 2.3 is of independent interest: it is the first finite de Finetti theorem in which the approximating separable state inherits linear constraints of the extension.

The results are proved in the paper; none of them has been machine-checked. A complete formalization requires the quantum relative entropy and mutual information with their chain rule, the quantum Pinsker inequality, state two-designs and their existence, and a weighted Hölder inequality for Schatten norms; most of this is absent from Mathlib, and each piece is reusable beyond this mission.

Difficulty

The obvious route measures every copy $B_i$ with a fixed informationally complete measurement and uses the resulting classical de Finetti statement. This approximates $\rho_{AB}$ by a mixture of product states, but the states in the mixture need not satisfy $\Gamma(\omega^i)=Y$ , and projecting them onto the constraint set destroys the error bound. The paper instead conditions on the outcomes of only $m$ copies and keeps $B_{m+1}$ quantum; the constraint on $B_n$ then transfers to the conditional state of $B_{m+1}$ by symmetry. Making this rigorous needs the chain rule of conditional mutual information with classical conditioning, and the distortion of the measurement must be bounded independently of the side system $A$ , which is what Lemma D.1 provides. The Schatten-norm estimate there is elementary but requires a weighted Hölder inequality and a careful choice of weight.

Formalization scope

Systems are finite index types: $A\otimes B_1\cdots B_N$ is indexed by Fin dA × (Fin N → Fin dB), $\otimes$ is Mathlib's Kronecker product, and the permutation action permutes the word in Fin N → Fin dB. States, trace norm and partial traces are the published definitions WildeQIT_IsDensityOperator, WildeQIT_traceNorm and WildeQIT_partialTrace. The linear maps $\Lambda$ , $\Gamma$ are arbitrary $\mathbb C$ -linear maps (not assumed positive or trace preserving), applied blockwise to one tensor factor. The objective is the real part of $\mathrm{Tr}[G\,W]$ , equal to $\mathrm{Tr}[G\,W]$ for Hermitian $G$ . Each "max" is the supremum of the set of objective values over the feasible set, never over all matrices. Wherever the page has $n\ge1$ copies of $B$ , the Lean has n + 1: SDPval … n is the page's $\mathrm{SDP}_{n+1}$ , and the bounds have denominator $n+1$ . The distortions $f(A,B)$ and $f(B|\cdot)$ take values in $[0,\infty]$ ; the standalone bound on $f(B|\cdot)$ assumes $d_B\ge1$ .

No feasibility hypothesis is added to the goal. The feasible sets of $Q$ and of every level are empty or nonempty together, and the empty case reads $0\le0\le0+\dots$ . The goal mentions only $Q$ , $\mathrm{SDP}_n$ , $G$ , $d_A$ , $d_B$ and $n$ ; a formalization in which $Q$ or $\mathrm{SDP}_n$ were free real numbers, or in which the de Finetti mixture was not required to satisfy the constraints, would be a different and much weaker statement.

Contributions are welcome at every milestone, and especially in the reusable infrastructure: quantum relative entropy and mutual information on matrices, the quantum Pinsker inequality, unitary and state designs, and Hölder inequalities for Schatten norms.

Selected references

M. Berta, F. Borderi, O. Fawzi, V. B. Scholz, Semidefinite programming hierarchies for constrained bilinear optimization, Mathematical Programming, 2021; arXiv:1810.12197v3. https://arxiv.org/abs/1810.12197
F. G. S. L. Brandão, A. W. Harrow, Quantum de Finetti theorems under local measurements with applications, STOC 2013. https://arxiv.org/abs/1210.6367
M. Christandl, R. König, G. Mitchison, R. Renner, One-and-a-half quantum de Finetti theorems, Communications in Mathematical Physics 273, 2007. https://arxiv.org/abs/quant-ph/0602130
A. C. Doherty, P. A. Parrilo, F. M. Spedalieri, Complete family of separability criteria, Physical Review A 69, 2004. https://arxiv.org/abs/quant-ph/0308032

17 thms2 active usersReviewed

Bandit Algorithms Machine Learning Operations Research·Captain: mikedeng1

Regret in Online Combinatorial Optimization II: Under Bandit Feedback Every Strategy Has Minimax Regret at Least 0.02 m√(dn) on Some Set of Actions with m OnesResearch Paper

Why bandit feedback matters

An online player repeatedly chooses a subset of coordinates and pays the sum of their losses. In many applications the player sees only that sum, not the losses of the selected coordinates. This bandit feedback makes it harder to identify which coordinate within each chosen subset is responsible for a favorable or unfavorable outcome. Audibert, Bubeck and Lugosi studied how this information limit changes regret in online combinatorial optimization. Their Theorem 5 establishes a lower bound that scales linearly with the number of selected coordinates and with the square root of the ambient dimension and horizon. Audibert, Bubeck and Lugosi, 2013, pp. 13–14

The result is part of a comparison among full-information, semi-bandit and bandit feedback in the same action model. Under full information the player sees the complete loss vector after each round; under semi-bandit feedback the player sees losses at selected coordinates; under bandit feedback the player sees only one scalar. The paper proves upper bounds for semi-bandit play and a bandit lower bound. The latter is the target of this mission. Audibert, Bubeck and Lugosi, 2013, pp. 2–3, 14

The game and its regret

Fix a dimension $d$ , a horizon $n$ , and a finite nonempty set $\mathcal A\subseteq\{0,1\}^d$ . Each action $a\in\mathcal A$ has exactly $m$ entries equal to one. At round $t$ , the player selects a probability distribution on $\mathcal A$ , draws an action $a_t$ , and simultaneously an adversary selects a loss vector $z_t\in[0,1]^d$ . The player pays the scalar $a_t^\mathsf Tz_t$ . In the bandit protocol, that scalar is the only new information made available for the next round. A player strategy can use every previous action and observed scalar loss, and can randomize at every round. Audibert, Bubeck and Lugosi, 2013, pp. 2–3

The paper measures performance by pseudo-regret against the best fixed action in expectation:

R_n=\mathbb E\sum_{t=1}^{n}a_t^\mathsf Tz_t- \min_{a\in\mathcal A}\mathbb E\sum_{t=1}^{n}a^\mathsf Tz_t.

The expectation covers the player's randomization and, when present, the adversary's randomization. This benchmark chooses one action for the whole horizon after comparing expected cumulative losses. It is the sole notion of regret used in the paper. Audibert, Bubeck and Lugosi, 2013, p. 2 and footnote 1

For the lower bound, the appendix arranges the $d$ coordinates as $m$ parallel games with $k=d/m$ choices per game. An action selects one coordinate from each game. The adversary can associate a favoured choice $\alpha$ with each game and assign independent Bernoulli losses whose means are $1/2-\epsilon$ at the favoured coordinates and $1/2$ elsewhere. The player still sees only the sum of the $m$ selected losses. These are the $\alpha$ -adversaries that underlie the milestone statements. Audibert, Bubeck and Lugosi, 2013, pp. 16–17

Formalization targets

The goal is Theorem 5 with the divisibility condition used by its appendix construction. For $n\ge d\ge2m$ and $m\mid d$ , there is an action set $\mathcal A$ such that every bandit strategy faces some bounded loss law with

R_n\ge0.02\,m\sqrt{dn}.

The order of the choices is part of the claim: the action set is fixed first; then each player strategy may face its own adversary. The lower bound retains the paper's explicit constant $0.02$ . Audibert, Bubeck and Lugosi, 2013, p. 14, Theorem 5; p. 16

The milestones follow the appendix's stated results: Lemma 5 bounds a logarithm; Lemma 4 and its corrected second case bound the divergence between sums of independent Bernoulli variables; the one-round observation bound and the horizon bound control information revealed by bandit feedback. Equations (9), (10), and (11) connect that information to expected regret and symmetry. The final averaged bound on the chance of selecting a favoured choice closes the path to the goal. The milestones are stated for deterministic players, as in the first three steps of the appendix; the passage to randomized players (the appendix's fourth step) is part of the goal's proof and is not a separate milestone. Audibert, Bubeck and Lugosi, 2013, pp. 17–18, 20–21

What the result establishes

The theorem prevents a uniform regret guarantee of smaller order than $m\sqrt{dn}$ for this bandit action model. It shows that aggregating $m$ selected losses into a single observation imposes a cost beyond what a player can avoid by choosing a different randomized strategy. In particular, the quantifier over every strategy makes the claim about the feedback model, rather than about one named algorithm. The paper proves the result in Appendix B, with the Bernoulli-sum estimate in Appendix C. Audibert, Bubeck and Lugosi, 2013, pp. 14, 16–18, 20–21

The formalization work is to prove the existing paper result in Lean from a finite protocol that represents all behavioural player strategies, together with the finite laws of the appendix's adversaries. The resulting definitions of action paths, scalar observations, finite probability laws, and divergence estimates can support other finite-horizon bandit lower bounds. These statements are drafted as open Lean theorems; compilation checks their types, while proofs remain for solvers. The paper's mathematical proof does not itself constitute a machine-checked proof.

Where the difficulty lies

A scalar bandit observation sums losses from several games. The player cannot separate the contribution of the favoured coordinate in one game from the other selected losses by inspecting that observation. A bound for the divergence of a single Bernoulli variable therefore does not directly bound the information available to the player. The appendix's central estimate concerns sums of independent Bernoulli variables, followed by the law of the whole sequence of scalar observations. Audibert, Bubeck and Lugosi, 2013, pp. 16, 18, 20

There is also a correction to make explicit. Lemma 4 is false for some parameters allowed by its printed statement: taking $n=\ell=1$ , $p=q=1/2$ , and $p'=0.001$ violates the displayed bound. The error is in the second case of its proof, which applies Lemma 5 outside its range when $p'<p$ . The mission states Lemma 4 with the additional condition $p(1-p')\le2p'(1-p)$ , which holds whenever $p\le p'$ , and states the corrected second case separately: for $q=p>p'$ , $\mathrm{KL}(\mathcal B,\mathcal B')\le(p'-p)^2/((1-p)p'(n+2))$ . Through the corrected case, the one-round bound used by the goal holds for the full range $0<\epsilon<1/2$ , so Theorem 5 and its constant are unaffected. Audibert, Bubeck and Lugosi, 2013, pp. 20–21, Lemmas 4–5

Formalization scope

Actions are functions $\mathrm{Fin}(d)\to\mathbb R$ constrained to zero or one, with coordinate sum $m$ . Coordinates and rounds are indexed from zero. A behavioural strategy maps every history of chosen actions and real-valued observed losses to a probability distribution on the finite action set. Its domain includes every real history, even though the appendix's particular Bernoulli adversaries generate integer observations. The strategy may randomize; restricting the goal to deterministic players or allowing it to inspect an unobserved loss vector would change the game.

The goal's exhibited adversary is an oblivious, finitely supported probability law on loss sequences in $[0,1]^{n\times d}$ . It belongs to the broader adversary class of the paper, so this existential formulation is stronger. All expectations are finite sums. The regret comparator is a minimum over the nonempty action set, not a default value assigned to an empty set. The action set has binary entries and equal coordinate sums, and every loss lies in the unit interval; these clauses rule out trivial lower bounds from malformed actions or unbounded losses.

The hypothesis $m\mid d$ is added to the printed theorem because Appendix B assumes it to partition coordinates into equally sized games. When $m=0$ , it forces $d=0$ and the claimed lower bound is zero. The milestone model uses functions $\mathrm{Fin}(m)\to\mathrm{Fin}(k)$ with $d=mk$ , deterministic players, finite Bernoulli product laws, and a finite real KL sum. Its log ratios are meaningful on the common support ensured by the stated parameter bounds. Reusable contributions include the finite bandit protocol and observation laws, as well as proofs of the KL and averaging milestones.

Selected references

Jean-Yves Audibert, Sébastien Bubeck and Gábor Lugosi, Regret in Online Combinatorial Optimization, Mathematics of Operations Research 39(1), 2014. arXiv:1204.4710v2; DOI:10.1287/moor.2013.0598.

13 thms2 active usersReviewed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

Data-Based Dynamic Pricing and Inventory Control with Censored Demand and Limited Price Changes 2: Any Policy with at Most m Price Changes Has Regret at Least KT^(1/(m+1)) on a Bernoulli InstanceResearch Paper

Why limited price changes matter

A seller learning a demand curve normally adjusts prices as new observations arrive. A price-change limit prevents that continual adjustment: a price may have to be chosen before the seller knows which demand curve it faces, then held through a block of sales. This matters when repricing is operationally costly, constrained by contracts, or visible to customers. Chen, Chao and Wang study pricing jointly with inventory replenishment under censored demand. Their Theorem 2 asks how much regret is unavoidable when the seller can change price at most $m$ times, regardless of the learning policy it uses (SSRN revision, pp. 10–11, 35–42).

The lower bound is paired with their Theorem 1: in the well-separated setting an algorithm attains regret proportional to $T^{1/(m+1)}$ for large horizons, while Theorem 2 asserts the same exponent cannot be improved uniformly over admissible policies (SSRN revision, p. 10). The paper appeared as an Operations Research technical note in 2020 (DOI 10.1287/opre.2020.1993); this mission cites the authors' SSRN revision dated 2020-02-10, whose page and result numbers are used throughout.

Bernoulli pricing setting

The horizon has $T$ periods. At each period the seller posts a price $p_t\in[1,6]$ and replenishes inventory to one unit. Demand $d_t$ is either zero or one, so all demand can be served and the observed sale equals demand. The unknown scalar parameter $z$ belongs to $[1/6,5/6]$ . Conditional on the posted price, the probability of one unit of demand is

\nu(p,z)=\max\{0,1-pz/2\}.

Holding and shortage costs are zero. Hence expected one-period revenue is $r_z(p)=p\nu(p,z)$ . The clairvoyant benchmark is $G^*(z)=1/(2z)$ : it is attained by the feasible price $p^*=1/z$ . The local Lean sanity check proves this maximum property, so the benchmark does not rely on a default value of a supremum. The model is the explicit Bernoulli construction in the proof of Theorem 2 (SSRN revision, p. 35).

An admissible randomized policy may draw random bits and use past posted prices and observed sales when choosing its next price. Its action cannot depend on future demand or on the unknown parameter. Every realized seed and demand path must satisfy the price-change constraint

\sum_{t=1}^{T-1}\mathbf 1\{p_t\ne p_{t+1}\}\le m,\qquad m\ge1.

The regret $R_\pi(T,z)$ is the expected sum of $G^*(z)-r_z(p_t)$ under the policy and the demand law at parameter $z$ . The paper's admissibility and change constraint are stated on pp. 5–6; its randomized policy factorization is displayed in (49) on p. 35 (SSRN revision).

Formalization targets

The goal is the minimax reading of Theorem 2. For each fixed $m\ge1$ , there is a positive constant $K_7$ and a horizon threshold $T_0$ , independent of the policy and the horizon, such that

\forall T\ge T_0\;\forall\pi\text{ admissible with at most }m\text{ changes},\quad \exists z\in[1/6,5/6]:\ R_\pi(T,z)\ge K_7T^{1/(m+1)}.

The parameter is selected after the policy. The proof's objective (56) is a worst-case parameter choice for each policy (SSRN revision, p. 37). The printed theorem sentence can also be read as one fixed instance defeating every algorithm; that order is false because a policy supplied with that instance's $z$ can post $1/z$ in every period.

Five milestones expose the source's quantitative ingredients. The hierarchy (50) constructs parameters $z_\zeta$ from signs $\zeta\in\{\pm1\}^{m+1}$ and scales $\varepsilon_\ell=T^{-\ell/[2(m+1)]}$ . Its parameters lie in $[1/6,5/6]$ for large $T$ . Different signs are separated at scale $\varepsilon_\ell/8$ . Lemma 1 bounds one-period regret by the squared error in a nearest-instance selection. The pointwise inequality underlying (57) gives a cost of at least $10^{-4}\varepsilon_\ell^2$ for a wrong sign. A corrected Lemma 2 supplies a quadratic Bernoulli relative-entropy bound under an explicit interior condition (SSRN revision, pp. 36–37).

What the result establishes

The exponent $1/(m+1)$ quantifies the cost of the change budget: fixing $m$ leaves a polynomial regret floor even though the Bernoulli demand law is one-dimensional and observed without censoring. Since the constructed instance fixes inventory at a level that serves every demand, a lower bound here also applies to policies in the joint pricing and inventory setting whenever that instance is admitted. It identifies the information loss caused by limited repricing, independently of lost sales and censoring.

The paper states the lower bound and gives a proof, but its printed Lemma 2 is false at prices where $\nu(p,z)=0$ . The subsequent Lemma 3 applies that unrestricted bound. Therefore the source proof does not, as printed, establish the minimax claim for every admissible price policy. The Lean goal is an open target; the four elementary milestones and corrected information bound are also open Lean statements. Formalizing this mission requires an argument that handles prices at the zero-demand kink, or a different route to the lower bound. No machine-checked proof of this specific result is claimed here.

Where the argument is difficult

The natural comparison of two nearby parameters uses the relative entropy between their observed demand laws. Away from the kink, this information is quadratic in the parameter difference. At a price that makes demand impossible under one parameter but possible under the other, the divergence in the printed direction can be linear in that difference. The unrestricted $108|z-z'|^2$ bound of Lemma 2 therefore fails at exactly the prices an arbitrary policy may choose. Restricting the policy's prices would change the target. A faithful proof must retain those prices while still controlling the policy's information and regret (SSRN revision, Lemmas 2–3, pp. 36–40).

Formalization scope

Lean represents the horizon by Fin T; its index zero is period one in the paper. Bernoulli demand paths have type Fin T → Bool. A policy's price at a period depends on a random seed and only the earlier demand bits; with inventory level one, these bits are exactly the observed sales. A probability measure on the seed models adaptive randomization, including a pre-sampled stream of random choices. Prices are measurable functions of the seed for each finite history. The budget holds on every seed and path, not only on average.

Path probabilities are finite products of conditional Bernoulli probabilities. Regret is a finite sum of nonnegative gaps integrated over the seed with lintegral, so it cannot become zero through non-integrability of a real-valued expectation. The exponent of $T$ and the scales $\varepsilon_\ell$ use real division. The arg-min in (51) is any genuine nearest-instance selection; a local proof checks that one exists. The hierarchy's validity and separation statements require a large-horizon threshold, which the unqualified printed prose omits. The corrected Lemma 2 adds $pz\le11/6$ to keep the Bernoulli probabilities in the interior. Its verbatim milestone retains the printed statement, and its formal statement and note disclose the correction. Lemma 3 is not stated because its printed proof relies on Lemma 2 outside that interior region.

The named Bernoulli family strengthens the theorem's existential instance wording, while also exposing a limitation: at $p\ge2/z$ it violates the positive-mean and identifiability conditions stated earlier in the paper. That discrepancy is recorded rather than hidden in an assumption. Definitions for randomized adapted policies, finite path laws, the parameter hierarchy, and Bernoulli relative entropy are reusable; contributions that establish the open goal or repair the information comparison are in scope.

Selected references

B. Chen, X. Chao, and Y. Wang, Data-Based Dynamic Pricing and Inventory Control with Censored Demand and Limited Price Changes, SSRN 2700747, revision of 2020-02-10. Preprint.
B. Chen, X. Chao, and Y. Wang, Technical Note—Data-Based Dynamic Pricing and Inventory Control with Censored Demand and Limited Price Changes, Operations Research, 2020. DOI 10.1287/opre.2020.1993.

10 thms2 active usersReviewed

Probability Random Matrix Theory Statistics·Captain: mikedeng1

Universality in Polytope Phase Transitions and Message Passing Algorithms 2: State Evolution, Empirical Averages of Polynomial AMP Iterates Converge to Gaussian ExpectationsResearch Paper

Motivation

Approximate message passing (AMP) is an iterative method for large systems with random matrices. At each step, every coordinate receives a weighted combination of nonlinear messages from all other coordinates, together with a correction for dependence created by earlier steps. For symmetric random matrices, the correction makes a simple description of the high-dimensional iterates possible: a finite collection of covariance matrices predicts their limiting distributions. Bayati, Lelarge and Montanari prove this state evolution statement for polynomial AMP on a broad class of independent sub-Gaussian matrix entries, rather than only Gaussian entries (paper, §§1.2–1.3). It gives a precise distributional account of an algorithm whose coordinates are coupled at every iteration.

The paper has three distinct headline results. Its Theorem 3 compares AMP moments under two matrix laws with equal entry variances, and its Theorem 2 concerns projected cross-polytopes. This mission targets Theorem 4, which identifies the limit of empirical averages of AMP iterates with a Gaussian expectation. The companion missions address the other results; the statements here use their own copy of the paper's AMP model because draft definitions cannot yet be imported across proposals (paper, pp. 5, 8–9).

Setting

For each size $N$ , let $A(N)$ be a random symmetric $N\times N$ matrix with zero diagonal. Its entries above the diagonal are independent, centered, and sub-Gaussian at scale $C/N$ . Each coordinate $i$ carries a polynomial map $f^i(\cdot;t):\mathbb R^q\to\mathbb R^q$ at iteration $t$ and an initial vector $x_i^0$ . Their coefficients have degree at most $d$ and a uniform bound $C$ . The AMP orbit is

x_i^{t+1}=\sum_j A_{ij}f^j(x_j^t;t) -\sum_j A_{ij}^{2}Jf^j(x_j^t;t)f^i(x_i^{t-1};t-1).

The second sum is the Onsager memory term; it is absent at $t=0$ . Here $Jf^j$ is the Jacobian, so its product with the preceding $q$ -vector is another $q$ -vector. The initial vectors obey an exponential bound on their squared Euclidean norms. These assumptions form the paper's $(C,d)$ -regularity condition (Definitions 2–4, pp. 6–7).

A converging sequence has a fixed finite set of classes $a\in[k]$ . Coordinate $i$ belongs to $C_a^N$ for one class $a$ , whose proportion approaches $c_a\in(0,1)$ . A symmetric nonnegative matrix $W$ specifies entry variances: if $i\in C_a^N$ and $j\in C_b^N$ , then $\mathbb E A_{ij}^2=W_{ab}/N$ . Independent labels $Y(i)$ have class-dependent laws $P_a$ , each a finite mixture of Gaussian laws that may be degenerate. The polynomial maps have the common form $f^i(x;t)=g(x,Y(i),a,t)$ for $i\in C_a^N$ (Definition 5, pp. 8–9).

The empirical second moments of $g(x_i^0,Y(i),a,0)$ converge in probability to a prescribed positive semidefinite matrix $\widehat\Sigma_a^0$ . For $t\ge1$ , state evolution defines

\Sigma_a^t=\sum_b c_bW_{ab}\widehat\Sigma_b^{t-1},\qquad \widehat\Sigma_a^t=\mathbb E\big[g(Z_a^t,Y_a,a,t)g(Z_a^t,Y_a,a,t)^{\mathsf T}\big],

where $Z_a^t\sim\mathcal N(0,\Sigma_a^t)$ is independent of $Y_a\sim P_a$ . The index $t-1$ in the first formula and $t$ in the second are essential (equations (1.9)–(1.11), p. 9).

Formalization targets

Coordinate moments and concentration

For a nonnegative multi-index $m$ and a coordinate sequence eventually in class $a$ , Proposition 4 identifies the Gaussian limit of each moment. Proposition 5 says the variance of the class-average monomial tends to zero:

\mathbb E[(x_{i(N)}^t)^m]\longrightarrow\mathbb E[(Z_a^t)^m],\qquad \operatorname{Var}\!\left(\frac1{|C_a^N|}\sum_{i\in C_a^N}(x_i^t)^m\right)\longrightarrow0.

The diagonal two-time identity (4.4) is another milestone: $\Sigma_a^{t,t}$ has four blocks, each equal to $\Sigma_a^t$ . These are the paper's stated intermediate targets (pp. 15, 30, 32).

Main goal: Theorem 4

For $t\ge1$ , class $a$ , and every locally Lipschitz function $\psi$ with $|\psi(x,y)|\le K(1+\|x\|_2^2+\|y\|_2^2)^K$ for some $K$ , prove convergence in probability:

\frac1{|C_a^N|}\sum_{j\in C_a^N}\psi(x_j^t,Y(j)) \longrightarrow \mathbb E[\psi(Z_a^t,Y_a)].

The target covers polynomial-growth test functions, including functions beyond monomials. The expectation on the right is under the product law of the Gaussian state and the independent class label (Theorem 4, p. 9).

Significance

The theorem assigns a computable asymptotic distribution to each class of AMP coordinates at every fixed positive iteration time. It can be used to evaluate empirical observables without tracking the full coupled $N$ -dimensional random trajectory. The class weights and variance profile permit heterogeneous coordinates, while the sub-Gaussian assumption covers more matrix laws than a Gaussian-only statement (paper, Introduction and Theorem 4).

The paper proves this result. The mission's Lean statements are compilation-checked targets, with proofs still to be formalized. A completed development would establish the measure-theoretic meaning of the covariance recursion and its Gaussian expectations, as well as the moment and concentration claims needed for the empirical limit. The polynomial representation, random-matrix regularity predicate, and Gaussian transport are reusable for other AMP results from the same paper.

Difficulty

The matrix $A(N)$ is reused at every AMP iteration, so a new coordinate is correlated with earlier coordinates and with the matrix entries that produced them. A direct independent-summand argument for its Gaussian limit is unavailable. The memory term is tuned to this dependence, and any formal proof must account for its exact Jacobian and squared-entry form. Passing from individual moments to empirical averages also requires control of correlations between different coordinates. The target allows locally Lipschitz functions with polynomial growth, so convergence for a fixed monomial alone does not finish the job (paper, §4.7).

Formalization scope

Vectors in $\mathbb R^q$ are functions Fin q → ℝ; squared Euclidean norms are explicit sums of coordinate squares. Polynomials use bounded real coefficient arrays as in (4.10), with an explicit Jacobian. Fin N uses zero-based indices. The orbit stores the current and preceding iterates and omits the memory term at $t=0$ . A single probability space carries all sizes; matrix entries, labels, coefficients, and initial vectors have explicit measurability and independence conditions.

The paper's displayed sub-Gaussian formula conflicts with its stated $C/N$ scale, so the model uses the scale required by its moment estimates and imposes the moment-generating bound for all real arguments. Its initial exponential bound is read almost surely at every size, which ensures the expectations used by the paper are well-defined. Label-dependent polynomial coefficients are measurable. The full label vector is independent of the matrix and initial vectors; this makes explicit the independence needed for Theorem 4's Gaussian-label product law. Independence of the induced polynomial coefficients alone would not imply it when $g$ ignores part of a label. The initial covariance limit is entrywise convergence in probability; finite-dimensional equivalence makes this the same matrix convergence. Class averages divide by the class cardinality, even though that expression has Lean's default value at an empty class for a small $N$ . Positive limiting class fractions make those finite exceptions irrelevant.

Gaussian laws live on Mathlib's Euclidean space and are transported to coordinate vectors. Theorems explicitly assert positive semidefiniteness or integrability where a non-PSD covariance, non-integrable expectation, or non-square-integrable variance could otherwise give a default value. The source's $Y(i)$ in (1.12) is read as $Y(j)$ , its summation index, and its final covariance as $\Sigma_a^t$ . The Gaussian covariance is computed by the recursion above; it is not defined from the proposed limit. Contributions establishing moment bounds, covariance positivity, Gaussian integrability, the three milestones, or the full Theorem 4 are within scope.

Selected references

M. Bayati, M. Lelarge and A. Montanari, Universality in polytope phase transitions and message passing algorithms, Annals of Applied Probability 25(2), 2015, 753–822. arXiv:1207.7321v2; DOI:10.1214/14-AAP1010.

12 thms2 active usersReviewed

Probability Random Matrix Theory·Captain: mikedeng1

Universality in Polytope Phase Transitions and Message Passing Algorithms 1: Polynomial AMP Iterates Have the Same Asymptotic Moments for All Sub-Gaussian Matrices with Equal Entry VariancesResearch Paper

Motivation

Approximate message passing (AMP) is a family of iterative algorithms driven by a large random matrix. It was introduced for compressed sensing by Donoho, Maleki and Montanari (PNAS 2009), and it is also used for low-rank matrix estimation, regression and spin-glass optimization. Its main appeal is that, for Gaussian random matrices, the empirical distribution of its iterates is tracked exactly in the large-dimensional limit by a scalar or low-dimensional recursion called state evolution. Bolthausen (CMP 2014) and Bayati and Montanari (IEEE Trans. Inf. Theory 2011) proved this for Gaussian matrices. Those proofs condition on the matrix through linear observations, and that conditioning argument works only for Gaussian entries.

In practice, and in the compressed-sensing phase transition that motivates the paper, the matrices are not Gaussian: Bernoulli, Rademacher and other sub-Gaussian ensembles are used. Bayati, Lelarge and Montanari (arXiv:1207.7321, Ann. Appl. Probab. 25(2), 2015) prove that the asymptotic behaviour of AMP with polynomial nonlinearities is universal: it depends on the law of the matrix entries only through their variances. This mission formalizes that universality theorem, Theorem 3 of the paper, together with the main steps of its proof.

Setting

Fix a dimension $q \ge 1$ and a degree bound $d \ge 0$ . For each $N$ , an AMP instance consists of three objects:

a symmetric matrix $A \in \mathbb R^{N\times N}$ with $A_{ii} = 0$ ;
polynomial maps $f^j(\cdot\,; t):\mathbb R^q\to\mathbb R^q$ of degree at most $d$ , one for each $j\in[N]$ and each time $t\ge 0$ ;
an initial condition $x^0 = (x^0_1,\dots,x^0_N)$ with $x^0_i \in \mathbb R^q$ .

The AMP orbit is

x^{t+1}_i \;=\; \sum_{j} A_{ij}\, f^j(x^t_j; t) \;-\; \sum_{j} A_{ij}^2\, \frac{\partial f^j}{\partial x}(x^t_j; t)\, f^i(x^{t-1}_i; t-1),

where $\partial f^j/\partial x$ is the $q\times q$ Jacobian. The second term, the memory or Onsager term, is absent at $t=0$ . A sequence of random instances indexed by $N$ is $(C,d)$ -regular if it satisfies the following conditions:

the entries $A_{ij}$ , $i<j$ , are independent and centered, and each is sub-Gaussian with scale factor $C/N$ , that is, $\mathbb E e^{\lambda A_{ij}}\le e^{C\lambda^2/(2N)}$ for all real $\lambda$ ;
all coefficients of the polynomials are bounded by $C$ ;
the matrix, the polynomials and the initial condition are mutually independent;
$\sum_i \exp(\|x^0_i\|_2^2/C)\le NC$ .

The proof also uses an auxiliary message-passing iteration. It consists of messages $z^t_{i\to j}\in\mathbb R^q$ with $z^0_{i\to j}=x^0_i$ and

z^{t+1}_{i\to j}(r)=\sum_{\ell\neq j} A_{\ell i}\, f^\ell_r(z^t_{\ell\to i};t),\qquad z^{t+1}_{i}(r)=\sum_{\ell} A_{\ell i}\, f^\ell_r(z^t_{\ell\to i};t).

Monomials are written $x^m=\prod_r x(r)^{m(r)}$ for $m\in\mathbb N^q$ .

Formalization targets

Goal: Theorem 3 (p. 8)

Let $(A(N),\mathcal F_N,x^{0,N})$ and $(\tilde A(N),\mathcal F_N,x^{0,N})$ be two $(C,d)$ -regular sequences. They share the polynomials and the initial condition, and $\mathbb E A_{ij}^2=\mathbb E\tilde A_{ij}^2$ for all $i<j$ . Then for every $t$ and every family of polynomials $p_{N,i}:\mathbb R^q\to\mathbb R$ of degree at most $d$ with coefficients bounded by $B$ ,

\lim_{N\to\infty}\frac1N\sum_{i=1}^N\Big\{\mathbb E\,p_{N,i}(x^t_i)-\mathbb E\,p_{N,i}(\tilde x^t_i)\Big\}=0 .

Milestones

Lemma 12 (p. 70): $x^s\le (s/e)^s e^x$ for $s,x>0$ .
(4.15) (p. 20): a sub-Gaussian variable with scale factor $C/N$ satisfies $\mathbb E|X|^s\le 2C^{s/2}(s/e)^{s/2}N^{-s/2}$ .
Proposition 1 (p. 16): $|\mathbb E(z^t_i)^m-\mathbb E(\tilde z^t_i)^m|\le KN^{-1/2}$ for $t\ge1$ .
Lemma 2, uniform bounds (pp. 22–23): $|\mathbb E z^t_i(r)^m|\le K$ and $|\mathbb E z^t_{i\to j}(r)^m|\le K$ .
Proposition 3 (p. 17), averaged over coordinates: $\frac1N\sum_i|\mathbb E(x^t_i)^m-\mathbb E(z^t_i)^m|\le KN^{-1/2}$ for $t\ge1$ . The page states the bound for each $i$ ; that form fails when one coordinate of $x^{0,N}$ grows like $\sqrt{\log N}$ , which Definition 4(3) permits, and the averaged form is what Theorem 3 needs.

In each milestone $K$ depends only on $C,d,q,t,m$ , as Note 2 of the paper specifies.

Significance

Theorem 3 lets results proved for Gaussian matrices be transferred to every sub-Gaussian ensemble with the same variance profile. In the paper, it is the first link of a chain:

Theorem 3 gives state evolution for general matrices (Theorem 4, the second mission of this series);
state evolution, together with an analysis of AMP as a solver of $\ell_1$ minimization, gives the universality of the Donoho–Tanner phase transition for random projections of the cross-polytope (Theorem 2, the third mission).

The universality of the weak-neighborliness threshold for non-Gaussian matrices, observed numerically by Donoho and Tanner (Phil. Trans. R. Soc. A 2009), is a consequence of this chain.

The result has been proved since 2012. No machine-checked proof of it, or of any AMP state-evolution statement, is known to exist. The mission asks for a formalization of the published proof, or of any other argument. Two pieces of the proof are useful elsewhere: the absolute-moment bound for sub-Gaussian variables and the moment comparison of the message-passing iteration.

Difficulty

The first idea is a Lindeberg-type swap: replace the entries of $A$ by those of $\tilde A$ one at a time and bound each change. This does not work directly. Every iterate $x^t_i$ depends on all $N(N-1)/2$ entries through $t$ nested polynomial layers. The memory term also couples consecutive iterates through the squares $A_{ij}^2$ . A single swap therefore changes every coordinate of every later iterate, and the per-swap errors have to be summed over $\Theta(N^2)$ swaps with a total error of $o(1)$ .

Two features of the statement make it delicate. Only second moments of the entries are matched, so every contribution of higher moments of the entries must be shown to vanish in the limit. In addition, the AMP orbit is not itself a message-passing iteration: its moments match those of $z^t$ (Proposition 3) only because of the memory term, and without that term they do not. A formal proof also has to establish finiteness of all the moments involved, which the paper takes for granted.

Formalization scope

Vectors in $\mathbb R^q$ are Fin q → ℝ, and indices are 0-based. A polynomial is given by its coefficient vector over the exponent vectors of total degree at most $d$ , as in (4.10) of the paper. This keeps random polynomials in a measurable space. The Jacobian is the explicit sum of formal partial derivatives. A sorry-free sanity file checks it against the analytic derivative on an example and checks the memory term on a small instance.

The orbit is computed by recursion on $(x^t,x^{t-1})$ , with no memory term at $t=0$ . The memory term uses $A_{ij}^2$ itself, not its expectation $1/N$ . All random objects live on one probability space. The two sequences of Theorem 3 share one coefficient process and one initial condition.

Three readings of the printed Definition 4 are disclosed:

sub-Gaussianity is required for all real $\lambda$ (Mathlib's HasSubgaussianMGF), not only for $\lambda > 0$ ;
the scale factor is $C/N$ , as the proof uses. The printed bracket $(C\lambda)^2/(2N^2)$ would rule out every ensemble with variance $1/N$ once $N > C^2$ , which would make the theorem vacuous;
the initial-condition bound holds almost surely for every $N$ , not "with probability converging to one".

Every expectation appearing in a target is also asserted to be finite. Without that, a bound or a limit could hold only because Lean assigns the value $0$ to the integral of a non-integrable function. Squared Euclidean norms are written as sums of squares, never as the sup norm that Mathlib puts on Fin q → ℝ. The deterministic identities of the tree expansion (Lemma 1, Lemma 3) and the first claim of Lemma 2 are not posed, because they need the labelled-tree families of Definition 6. Contributions of that tree machinery are welcome. Moment bounds for sub-Gaussian variables and polynomial moment estimates for sums of independent variables are reusable well beyond this mission.

Selected references

M. Bayati, M. Lelarge, A. Montanari, Universality in polytope phase transitions and message passing algorithms, Ann. Appl. Probab. 25(2):753–822, 2015. arXiv:1207.7321v2, DOI
D. L. Donoho, A. Maleki, A. Montanari, Message-passing algorithms for compressed sensing, PNAS 106(45):18914–18919, 2009. DOI
M. Bayati, A. Montanari, The dynamics of message passing on dense graphs, with applications to compressed sensing, IEEE Trans. Inf. Theory 57(2):764–785, 2011. DOI
E. Bolthausen, An iterative construction of solutions of the TAP equations for the Sherrington–Kirkpatrick model, Comm. Math. Phys. 325:333–366, 2014. DOI
D. L. Donoho, J. Tanner, Observed universality of phase transitions in high-dimensional geometry, Phil. Trans. R. Soc. A 367:4273–4293, 2009. DOI

9 thms2 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Bootstrap Robust Prescriptive Analytics 3: Any Distance Exceeding the Bootstrap Distance Near Some D Loses the Disappointment Rate −rResearch Paper

Motivation

Data-driven decision making estimates the cost of a decision from training data and then optimizes that estimate. The optimized estimate is biased downwards: the decision that looks best on the training data tends to disappoint on fresh data. Distributionally robust optimization counters this by optimizing the worst case of the estimate over all distributions within a radius $r$ of the empirical distribution, measured by a chosen distance function $R$ . Many distance functions are in use (φ-divergences, Wasserstein distances, moment sets), and the choice is usually justified by tractability.

Bertsimas and Van Parys, Bootstrap robust prescriptive analytics (arXiv:1711.09974v2), measure disappointment on bootstrap data: resamples drawn with replacement from the training data. Their Theorem 6 shows that with the entropic bootstrap distance $B$ the bootstrap disappointment decays exponentially in the sample size at rate at least $r$ . Proposition 1, the subject of this mission, is the converse: $B$ is the smallest distance function with this guarantee. Any distance that is strictly larger than $B$ near some distribution admits a nominal formulation whose disappointment decays strictly slower than $e^{-nr}$ . The result is in the spirit of Van Parys, Esfahani and Kuhn (arXiv:1704.04118), where the relative entropy is shown to be the optimal ambiguity set for i.i.d. data.

Setting

The distinct training points form a finite set $\Omega_n$ , written $\iota$ in Lean. A distribution on it is a vector $D\in\mathbb R^\iota$ with nonnegative entries summing to one; the simplex of all such vectors is $\mathcal D_n$ . The training data have the empirical distribution $D_{\rm tr}\in\mathcal D_n$ , which gives positive weight to every point of $\Omega_n$ .

The bootstrap distance (Definition 6, Eq. (27)) is the relative entropy

B(D,D')=\sum_{i\in\iota}D_i\log\frac{D_i}{D'_i},

with $0\log0=0$ and $B(D,D')=+\infty$ if some $D_i>0=D'_i$ .

A distribution distance function (Definition 4) is a map $R:\mathcal D_n\times\mathcal D_n\to(-\infty,+\infty]$ that is nonnegative, vanishes exactly on the diagonal ( $R(D',D)=0$ iff $D'=D$ ), and is convex in its first argument. $B$ is one.

A bootstrap sample of size $n$ is $n$ independent draws from $D_{\rm tr}$ (Eq. (14)); its law is the product $D_{\rm tr}^n$ , and its empirical distribution is $D_{{\rm bs}[n]}$ , the frequency of each point of $\iota$ among the $n$ draws.

A nominal formulation here is a loss $G:\iota\to\mathbb R_+$ with cost estimator $\mathbb E_D[G]=\sum_iD_iG_i$ . Its robust counterpart (Eq. (24)) replaces the estimate by $\sup\{\mathbb E_{D'}[G]: D'\in\mathcal D_n,\ R(D',D_{\rm tr})\le r\}$ , and its disappointment set is

\mathcal R=\Big\{D\in\mathcal D_n:\ \mathbb E_D[G]>\sup_{D'\in\mathcal D_n,\ R(D',D_{\rm tr})\le r}\mathbb E_{D'}[G]\Big\},

the bootstrap distributions on which the realized cost exceeds the robust budget.

Formalization targets

Goal: Proposition 1 (p. 16)

Let $R$ be a distribution distance function, $D\in\mathcal D_n$ with $B(D,D_{\rm tr})=r$ , and $\mathcal N\subseteq\mathcal D_n$ a neighbourhood of $D$ , open in $\mathcal D_n$ , on which $R(\cdot,D_{\rm tr})>r$ . Then there is a loss $G\ge0$ whose disappointment set satisfies

-r<\liminf_{n\to\infty}\frac1n\log D^\infty_{\rm tr}\big[D_{{\rm bs}[n]}\in\mathcal R\big],

stated in Lean in the equivalent form: for some $\varepsilon>0$ , eventually $D^n_{\rm tr}[D_{{\rm bs}[n]}\in\mathcal R]\ge e^{-n(r-\varepsilon)}$ .

Milestones (Appendix B.2, p. 27, and Eq. (31), p. 16)

Separation. The $R$ -ball $\{R(\cdot,D_{\rm tr})\le r\}$ and a convex open $\mathcal N$ on which $R>r$ are separated by a linear functional: $\mathbb E_D[G]\le a<\mathbb E_{D'}[G]$ .
Inclusion. For such $G$ and $a$ , ${\rm int}\,\mathcal N=\mathcal N\subseteq\mathcal R$ .
Sanov's lower bound (31). $-\inf_{D\in{\rm int}\,\mathcal C}B(D,D_{\rm tr})\le\liminf_n\frac1n\log D^\infty_{\rm tr}[D_{{\rm bs}[n]}\in\mathcal C]$ for every set $\mathcal C$ .
Convexity step. $B(\lambda D+(1-\lambda)D_{\rm tr},D_{\rm tr})\le\lambda B(D,D_{\rm tr})+(1-\lambda)B(D_{\rm tr},D_{\rm tr})<r$ for $\lambda\in(0,1)$ .
Infimum below $r$ . $\inf_{D'\in\mathcal N}B(D',D_{\rm tr})<r$ .

Significance

Proposition 1 turns Theorem 6 from a sufficient condition into a characterization. Theorem 6 says the bootstrap distance guarantees disappointment rate $r$ ; Proposition 1 says no distance function that is larger than $B$ on an open set does, for some nominal formulation. A practitioner who wants the bootstrap guarantee with the least conservative ambiguity set therefore has no better choice than $B$ in this sense. The result is one instance of a pattern in data-driven optimization, where large-deviation rate functions appear as the optimal ambiguity sets.

The paper's proof is a short combination of three standard facts: strict separation of convex sets, Sanov's theorem, and convexity of relative entropy. None of the three is available on the platform in the form needed. Sanov's theorem for empirical distributions on a finite alphabet has no machine-checked proof in Mathlib or on the platform; the lower bound (31) is a self-contained, reusable result of independent interest. The separation step needs strict separation inside the affine hull of the simplex, which Mathlib provides only in the ambient vector space. The result is proved on paper; none of it is formalized.

Difficulty

The separation and convexity steps are routine once the relative topology of the simplex is handled. The central difficulty is the lower bound (31), a large-deviation lower bound for the empirical distribution of i.i.d. draws. The bootstrap probability of an event is a sum of multinomial probabilities over the empirical distributions with denominator $n$ that fall in the event, and the bound must hold for every point of the relative interior, including points on the boundary of the simplex, where some coordinates vanish and the distance $B$ is not differentiable. An argument that only treats distributions of full support, or only open sets of $\mathbb R^\iota$ , does not cover these points.

A second difficulty is bookkeeping between the three topologies in play: the ambient space $\mathbb R^\iota$ , the simplex $\mathcal D_n$ , and the affine hull in which separation takes place.

Formalization scope

$\Omega_n$ is a finite type $\iota$ with decidable equality; distributions are stdSimplex ℝ ι. Covariates, responses, neighbourhood weights and the decision $z$ are abstracted away: the nominal formulation is the estimator $D\mapsto\sum_iD_iG_i$ (the estimator (18) with $k=n$ and unit weights), so the robust prescription $z^r_{\rm tr}(x_0)$ plays no role.
$D_{\rm tr}$ has all coordinates positive (the support convention of the paper).
$B$ and $R$ are EReal-valued; convexity of $R$ is written out in EReal. The supremum defining $\mathcal R$ is an EReal supremum. It is never empty, because $D_{\rm tr}$ lies in the $R$ -ball, so $\mathcal R$ cannot collapse to all of $\mathcal D_n$ .
The bootstrap law is the $n$ -fold product Measure.pi of $\sum_iD_{{\rm tr},i}\,\delta_i$ , with $D_{\rm tr}$ fixed while $n\to\infty$ .
"Open" and "int" are relative to $\mathcal D_n$ . With the ambient topology, no nonempty subset of the simplex is open and every interior is empty, which would make Proposition 1 and (31) vacuous; this formalization rules that out, as it rules out a junk real logarithm ( $\log0=0$ ) by using the explicit- $\varepsilon$ form of every rate statement.
Disclosed additions: the separation milestone assumes $\mathcal N$ is convex, nonempty and inside the relative interior of the simplex; the infimum milestone assumes $r>0$ , which holds in Proposition 1.

A complete development needs the method of types on a finite alphabet, strict separation in an affine subspace, and the convexity of relative entropy. The method-of-types lower bound is reusable well beyond this mission (hypothesis testing, large deviations of empirical measures). Proofs of any milestone, and alternative proofs of (31), are welcome.

Selected references

D. Bertsimas, B. Van Parys, Bootstrap robust prescriptive analytics, arXiv:1711.09974v2, 2021; Mathematical Programming, 2021. https://arxiv.org/abs/1711.09974
A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 2009 (Theorem 6.2.10, Sanov's theorem). https://doi.org/10.1007/978-3-642-03311-7
B. Van Parys, P. Mohajerin Esfahani, D. Kuhn, From data to decisions: distributionally robust optimization is optimal, Management Science 67(6), 2021. https://arxiv.org/abs/1704.04118
I. Csiszár, The method of types, IEEE Transactions on Information Theory 44(6), 1998. https://doi.org/10.1109/18.720546
B. Efron, The Jackknife, the Bootstrap and Other Resampling Plans, SIAM, 1982. https://doi.org/10.1137/1.9781611970319

8 thms2 active usersReviewed

Completed

Probability·Captain: marwahaha

The exact reconstruction threshold for the three-state symmetric channelOpen Problem

Motivation

Broadcasting a label through noisy tree edges models how information decays with distance. The source studies when observations far from the root retain information about its three-state label. The source is OpenAI's September 2026 manuscript.

Setting

The symmetric channel preserves the input with probability $(1+2\lambda)/3$ and sends it to each other state with probability $(1-\lambda)/3$ . Reconstruction advantage is the expected total variation between the posterior root law and the uniform prior.

Formalization targets

b\ge2,\quad-1/2\le\lambda\le1,\quad b\lambda^2>1\quad\Longrightarrow\quad\operatorname{Advantage}_n\to L>0.

For every natural number b ≥ 2 and every real λ that is admissible, meaning −1/2 ≤ λ ≤ 1, if b·λ² > 1 then the sequence of regular-tree advantages reconstructs. Here a three-state spin (an element of Fin 3) is passed through a symmetric channel that keeps the spin with probability (1+2λ)/3 and moves to each other spin with probability (1−λ)/3. The observation at depth 0 is the root spin, and the observation at depth n+1 is a multiset of depth-n observations, one for each of the offspring of the root, where the offspring count is the constant b (the regular case) and each child spin is obtained by passing the parent spin through the channel and then observed recursively. With a uniformly random root spin, the posterior of each spin given an observation is its conditional probability, defaulting to 1/3 when the observation has probability zero. The advantage of a family of laws indexed by the root spin is the sum over observations y of the marginal probability of y times half the sum over spins i of |posterior(y,i) − 1/3|. The regular advantage at depth n is this advantage for the regular b-ary observation law. Reconstructs means that this sequence in n converges to some limit L > 0. The statement is an admitted theorem, with its proof left as sorry.

The goal is OAI.ThreeState.regular_supercritical. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

Significance

The selected goal is the regular-tree supercritical direction. Supporting published targets give Poisson reconstruction and equivalent supercritical formulations in a second definition group. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The observation contains the full nested collection of descendants, and the posterior depends on correlated information inherited from their common ancestor. A single root-to-leaf correlation is insufficient to describe reconstruction.

Formalization scope

Observations are nested multisets with a uniform three-state root. The attached targets establish reconstruction above the displayed threshold; non-reconstruction at or below equality and stochastic-block-model recovery are outside this draft’s formal scope.

The shared definitions are supplied by ThreeStateSupercritical, ThreeStateTreeClauses. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

OpenAI, The exact reconstruction threshold for the three-state symmetric channel, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

48 thms2 active usersReviewed

Completed

Quantum Information·Captain: wurtle

Classical capacity and entropy inequalities for generalized amplitude dampingResearch Paper

Motivation: the classical capacity of a thermal qubit channel

A quantum channel models how a physical system, used to carry information, is corrupted by its environment. The classical capacity of a channel is the largest rate, in bits per use, at which classical messages can be sent with vanishing error when the sender may encode into arbitrary — possibly entangled — states of many uses and the receiver may measure all outputs jointly. The Holevo–Schumacher–Westmoreland coding theorem (Holevo 1998; Schumacher–Westmoreland 1997) expresses this capacity as a regularized limit of the Holevo information over ever larger blocks of uses. Since Holevo information is not additive in general (Hastings 2009), computing the capacity of any specific channel requires a channel-specific additivity argument, and exact formulas are known only for a few families.

Generalized amplitude damping is the standard model of a qubit relaxing toward a thermal state: it loses or gains an excitation with probabilities set by a damping strength $\gamma$ and a stationary excited population $\nu$ , and its coherences decay. It is one of the basic noise models of quantum information theory.

Background timeline

1996–1998 — Coding theorems for pure and mixed signals establish the regularized capacity formula (Hausladen et al. 1996; Schumacher–Westmoreland 1997; Holevo 1998).
2002 — Additivity for unital qubit channels (King 2002) and for entanglement-breaking channels (Shor 2002) settles some parameter regions of the family; Bennett, Shor, Smolin and Thapliyal describe the two-signal optimization for ordinary amplitude damping (BSST 2002).
2005 — Giovannetti and Fazio derive the optimized one-use expression for ordinary amplitude damping (Giovannetti–Fazio 2005); Berry studies qubit channels achieving capacity with two states (Berry 2005).
2007 — Hou and Fang characterize the one-use Holevo optimum of the generalized channel (Hou–Fang 2007).
2009 — Hastings shows that Holevo information is not additive in general (Hastings 2009).
2018 — Leditzky, Kaur, Datta and Wilde note that the unrestricted classical capacity of amplitude damping had not been determined (LKDW 2018).
2020 — Khatri, Sharma and Wilde collect upper bounds for the generalized family (KSW 2020).
2026 — Tang, Zhu, Bai and Wang prove additivity for qubit channels with a pure output, including ordinary amplitude damping (arXiv:2609.28592); Fang gives a close converse bound for the generalized family (arXiv:2609.14621).
2026 — An OpenAI preprint, Classical capacity and entropy inequalities for generalized amplitude damping (OpenAI Math Release, September 24, 2026), claims the capacity for all $(\gamma,\nu)\in[0,1]^2$ . The preprint has not been peer reviewed, and its results are not formally verified.

Setting

For $\gamma,\nu\in[0,1]$ the generalized amplitude-damping channel acts on a qubit density matrix by

\mathcal A_{\gamma,\nu}\begin{pmatrix}1-q&z\\\bar z&q\end{pmatrix}=\begin{pmatrix}1-t&\sqrt{1-\gamma}\,z\\\sqrt{1-\gamma}\,\bar z&t\end{pmatrix},\qquad t=(1-\gamma)q+\gamma\nu,

and $n$ independent uses act as $\mathcal A_{\gamma,\nu}^{\otimes n}$ on $2^n\times2^n$ matrices. With $S(P)=-\operatorname{Tr}P\ln P$ , the Holevo information in bits is

\chi(\mathcal N)=\frac1{\ln2}\sup_{\{q_a,\rho_a\}}\Bigl\{S\Bigl(\sum_aq_a\mathcal N(\rho_a)\Bigr)-\sum_aq_aS(\mathcal N(\rho_a))\Bigr\},

over all finite ensembles of input states (entangled across uses when $\mathcal N=\mathcal A^{\otimes n}$ ). The classical capacity $C(\mathcal N)$ is the supremum of rates $R$ for which there are $n$ -use codes — arbitrary input states for each of $M_n$ equiprobable messages and one joint measurement of all outputs — with average error tending to zero and $\liminf_n n^{-1}\log_2M_n\ge R$ ; there is no shared entanglement or feedback. Write $h$ for binary entropy in nats, $g(u)=h\bigl((1+\sqrt{1-4u})/2\bigr)$ and $v_{\gamma,\nu}(p)=\gamma\nu(1-\nu)+\gamma(1-\gamma)(p-\nu)^2$ .

Formalization targets

Goal: additivity and capacity formula (Theorem 1.1)

For all $\gamma,\nu\in[0,1]$ and every $n\ge1$ ,

\chi(\mathcal A_{\gamma,\nu}^{\otimes n})=n\,\chi(\mathcal A_{\gamma,\nu})=\frac n{\ln 2}\max_{0\le p\le1}\bigl\{h((1-\gamma)p+\gamma\nu)-g(v_{\gamma,\nu}(p))\bigr\},

the maximum is attained, $C(\mathcal A_{\gamma,\nu})=\chi(\mathcal A_{\gamma,\nu})$ , and for every maximizer $p$ the equiprobable independent products of the two signals $\phi_\pm=\sqrt{1-p}\,|0\rangle\pm\sqrt p\,|1\rangle$ attain $\chi(\mathcal A_{\gamma,\nu}^{\otimes n})$ at every block length. The goal is published on the platform with status Open.

Significance

The result itself. The theorem gives a closed one-variable formula for the classical capacity of every generalized amplitude-damping channel, removing the regularization over block lengths: entangled input signals across uses give no advantage, and a simple product code with two signals per use is optimal. This settles the ordinary amplitude-damping case listed as open by LKDW 2018 and extends beyond the pure-output criterion of Tang et al. to the thermal regime, where the channel has no pure output. The source further proves additivity of Holevo capacity, minimum output entropy and classical capacity when the channel is used in parallel with any finite-dimensional partner channel (Corollary 1.2); that corollary is not part of this goal.

Formalizing it. The goal ties together an operational capacity (codes and error probabilities), an entropic quantity (a supremum over unrestricted ensembles on $2^n$ -dimensional matrices), and a scalar optimization. A machine-checked proof would certify both the matrix entropy inequality at the heart of the argument and the converse direction of the coding theorem. Mathlib does not currently contain quantum channel capacity theory, so the definitions here are new infrastructure.

Difficulty

Optimizing a single use gives a lower bound on capacity; the difficulty is the matching upper bound for all $n$ simultaneously, where an input may be entangled across all uses. Holevo additivity is false for general channels, so no abstract argument applies, and for interior thermal occupation $0<\nu<1$ with $\gamma>0$ the channel has no pure output, which rules out the recent pure-output criterion. The proof needs a lower bound on the entropy of the output of an arbitrary entangled block input, i.e. a matrix entropy inequality for $2\times2$ block-structured states that is tight on product inputs. Identifying the capacity with the regularized Holevo quantity also requires the full coding theorem and a Fano-type converse.

Formalization scope

Matrices are indexed by Fin n → Fin 2; the $n$ -use channel is given by tensor products of the four standard Kraus operators of generalized amplitude damping, which reproduce the displayed action exactly.
Entropy is Tr (cfc negMulLog P) (nats, $0\ln0=0$ ); Holevo values are divided by $\ln 2$ (bits). holevo γ ν n is the sSup over all finite ensembles of arbitrary $2^n$ -dimensional states, with no product or purity restriction.
capacity is the sSup of operationally achievable rates: codes with any positive number of messages, arbitrary state encodings, an arbitrary POVM decoder, average error tending to $0$ , and the liminf rate condition. It is defined operationally, not by regularization, so the identity $C=\chi$ includes the coding theorem.
The scalar objective uses Real.binEntropy (nats); the maximizer is over $p\in[0,1]$ . The final clause also asserts that the phase-product signals are states.
Parameters range over the closed square $[0,1]^2$ , including boundary cases (identity channel at $\gamma=0$ , full replacement at $\gamma=1$ ).
Needed infrastructure: matrix entropy and its concavity, CPTP maps and Kraus representations, Holevo's bound, Fano's inequality, the HSW coding theorem for finite ensembles, and Fekete-type superadditivity. These are reusable for any quantum Shannon-theory mission.

Selected references

P. Hausladen, R. Jozsa, B. Schumacher, M. Westmoreland, W. K. Wootters, Classical information capacity of a quantum channel, Phys. Rev. A 54 (1996), 1869–1876. https://doi.org/10.1103/PhysRevA.54.1869
B. Schumacher and M. D. Westmoreland, Sending classical information via noisy quantum channels, Phys. Rev. A 56 (1997), 131–138. https://doi.org/10.1103/PhysRevA.56.131
A. S. Holevo, The capacity of the quantum channel with general signal states, IEEE Trans. Inf. Theory 44 (1998), 269–273. https://doi.org/10.1109/18.651037
C. King, Additivity for unital qubit channels, J. Math. Phys. 43 (2002), 4641–4653. https://doi.org/10.1063/1.1500791
P. W. Shor, Additivity of the classical capacity of entanglement-breaking quantum channels, J. Math. Phys. 43 (2002), 4334–4340. https://doi.org/10.1063/1.1498000
C. H. Bennett, P. W. Shor, J. A. Smolin, A. V. Thapliyal, Entanglement-assisted capacity of a quantum channel and the reverse Shannon theorem, IEEE Trans. Inf. Theory 48 (2002), 2637–2655. https://doi.org/10.1109/TIT.2002.802612
V. Giovannetti and R. Fazio, Information-capacity description of spin-chain correlations, Phys. Rev. A 71 (2005), 032314. https://doi.org/10.1103/PhysRevA.71.032314
D. W. Berry, Qubit channels that achieve capacity with two states, Phys. Rev. A 71 (2005), 032334. https://doi.org/10.1103/PhysRevA.71.032334
L.-Z. Hou and M.-F. Fang, The Holevo capacity of a generalized amplitude-damping channel, Chinese Physics 16 (2007), 1843–1847. https://doi.org/10.1088/1009-1963/16/7/006
M. B. Hastings, Superadditivity of communication capacity using entangled inputs, Nature Physics 5 (2009), 255–257. https://doi.org/10.1038/nphys1224
F. Leditzky, E. Kaur, N. Datta, M. M. Wilde, Approaches for approximate additivity of the Holevo information of quantum channels, Phys. Rev. A 97 (2018), 012332. https://doi.org/10.1103/PhysRevA.97.012332
S. Khatri, K. Sharma, M. M. Wilde, Information-theoretic aspects of the generalized amplitude-damping channel, Phys. Rev. A 102 (2020), 012401. https://doi.org/10.1103/PhysRevA.102.012401
Z. Tang, C. Zhu, G. Bai, X. Wang, Classical capacity and entanglement cost of the amplitude damping channel, arXiv:2609.28592 (2026). https://arxiv.org/abs/2609.28592v1
K. Fang, A pretty-tight converse on the classical capacity of generalized amplitude-damping channels, arXiv:2609.14621 (2026). https://arxiv.org/abs/2609.14621v1
OpenAI, Classical capacity and entropy inequalities for generalized amplitude damping, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 3). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026/paper.pdf

37 thms2 active usersReviewed

Completed

Probability Theoretical Computer Science·Captain: wurtle

Localization costs and information growth for exact Gaussian observationsResearch Paper

Motivation

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

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

Background

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

Setting

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

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

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

Formalization targets

Goal: Theorem 3.2 (Repeated localization), `repeated_localization`

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

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

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

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

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

Milestones (results from the paper's other routes)

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

5 thms2 active usersReviewed

Information Theory

Missions

Shadow Tomography of Quantum States 2: Even the Classical Special Case Needs Ω(min{D, log M}/ε²) CopiesResearch Paper

Why the copy count matters

States, measurements, and estimates

Formalization targets

Classical special-case lower bound

Supporting targets

What the result supplies

Where the argument is delicate

Formalization scope

Selected references

Conditional and Dynamic Convex Risk Measures II: The Conditional Entropic Risk Measure and Conditional Relative EntropyResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 5.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Free Energy Principle II: expected free energy, Markov blankets, Gaussian variational free energy, and Bayesian model reductionResearch Paper

Free Energy Principle II: expected free energy, Markov blankets, Gaussian variational free energy, and Bayesian model reduction

Motivation

Setting

Formalization targets

Goal: expected free energy decomposes into risk plus ambiguity

Gaussian variational free energy in closed form

Odds recursion of Bayesian model reduction

Native Markov blanket conditional independence

Significance

Difficulty

Formalization scope

Selected references

Boltzmann Constant: Kinetic Theory, Boltzmann Factors and EntropyTextbook

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

An Intuitive Proof of the Data Processing Inequality: Conditional von Neumann Entropy Cannot Increase Under Partial Trace, via the Smooth Min-Entropy DPI and the Quantum AEPResearch Paper

Motivation

Setting

Formalization targets

Goal: the von Neumann entropy DPI (Theorem 3)

The smooth min-entropy DPI (Theorem 1)

The QAEP (Theorem 2)

Significance

Difficulty

Formalization scope

Selected references

Entropy and Optimal Decompositions of States Relative to a Maximal Commutative Subalgebra: Equivalent Characterizations of a Symmetric Optimal Pair for Transposition-Invariant Rank-Two StatesResearch Paper

Motivation

Setting

Formalization targets

Goal: equivalent rank two conditions

Significance

Difficulty

Formalization scope

Selected references

General Benchmarks for Quantum Repeaters: For the Qudit Dephasing Channel the Entanglement-Flux Upper Bound Meets the Coherent Information, log₂ d − H(P)Research Paper

Motivation

Setting

Formalization targets

Goal (Eqs. (94)–(95), p. 11)

Milestones (in attack order)

Significance

Difficulty

Formalization scope

Selected references

Improving the Security of Quantum Protocols via Commit-and-Open: After the Commit-and-Open Test, Any Dishonest Bob Is β-Benign Up to a Negligible Trace DistanceResearch Paper

Motivation

Setting

Formalization targets

Goal: commit-and-open forces benign behaviour (§4.3, p. 12)

Milestones

Significance