Quantum Information

Motivation

This mission develops Chapter 2 of An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation by Daniel Gottesman. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

An $[[n,k,d]]$ code is a subspace $C$ of $(\mathbb C^2)^{\otimes n}$ of dimension $2^k$ such that every operator $E$ acting on at most $d-1$ qubits satisfies $\langle\psi|E|\psi\rangle=c'(E)$ for all unit vectors $|\psi\rangle\in C$, with $c'(E)$ independent of $|\psi\rangle$ (eq. (34)); that is, $C$ has distance at least $d$. Put $t=\lfloor (d-1)/2\rfloor$. The code is nondegenerate if, for every unit vector $|\psi\rangle\in C$, the Gram matrix $\big(\langle\psi|P_a^\dagger P_b|\psi\rangle\big)_{a,b}$ over the phase-free Pauli operators $P_a$ of weight at most $t$ is nonsingular. Let $H(x)=-x\log_2x-(1-x)\log_2(1-x)$.

1. (Quantum Gilbert–Varshamov bound.) If $d\ge1$ and

$$\Big(\sum_{j=0}^{d-1}3^j\binom nj\Big)2^k\le 2^n,$$

then an $[[n,k,d]]$ code exists. 2. (Quantum Hamming bound.) Every nondegenerate $[[n,k,d]]$ code satisfies

$$\Big(\sum_{j=0}^{t}3^j\binom nj\Big)2^k\le 2^n.$$

3. (Asymptotic rates.) Let $0<p<1/2$ and $\varepsilon>0$. There is $N$ such that for every $n\ge N$:
   • every nondegenerate $[[n,k,d]]$ code with $d\ge 2pn$ has $k/n\le 1-p\log_2 3-H(p)+\varepsilon$;
   • if $1-2p\log_2 3-H(2p)>0$, there is a nondegenerate $[[n,k,d]]$ code with $d\ge 2pn$ and $k/n\ge 1-2p\log_2 3-H(2p)-\varepsilon$.

The first two bounds are counting arguments. The third gives the rate window, eq. (37), between which the best nondegenerate codes lie.

Formalization Note The source's 'distance $d$' is read as distance at least $d$, so existence is meaningful also for $k=0$. The hypothesis $d\ge1$ excludes $d=0$, where (36) is an empty sum and the claim would demand a $2^k$-dimensional code for every $k$. The asymptotic clause is read as an $\varepsilon$–$N$ statement. The lower rate bound is asserted only when it is positive.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Theorem 1: No-Cloning: no quantum operation copies every state.
• Theorem 2: Correctable errors are closed under linear combinations; weight-t Pauli errors give all t-qubit errors.
• Theorem 3: Knill–Laflamme condition for quantum error correction.
• Theorem 4: Quantum Gilbert–Varshamov, quantum Hamming, and asymptotic rate bounds.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Daniel Gottesman, An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation, 2009, v1. https://arxiv.org/pdf/0904.2557v1.

Motivation

This mission develops Chapter 7 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

Fix constants $C_0 \in \mathbb{R}$ and $c_0 \in \mathbb{N}$ (those of the assumption $p = \widetilde{O}(1)$). There are constants $C > 0$ and $c \in \mathbb{N}$ such that the following holds. Let $q, p \in \mathbb{N}$, $d = 2^q$, $\xi > 0$, write $L = \log(2+d) + \log(2+1/\xi)$, and assume $p \le C_0 L^{c_0}$. Then there exist

1. a QRAM (Def. 5.39) with $2^b$ addresses and words of $r$ bits, of size $2^b r \le C d^2 (p+1) L^c$;
2. a straight-line real-arithmetic program of at most $C d^2 L^c$ operations ($+, -, \times, \div, \sqrt{\cdot}, \arccos$, complex argument, rational constants) and an addressing map, which compute the QRAM contents from the entries of the matrix;
3. a quantum circuit $\mathcal{V}$ on $w + q$ qubits with $w \le C (q+1) L^c$, making at most $C L^c$ uncontrolled calls to the QRAM (or its inverse) and using at most $C L^c$ two-qubit gates,

all independent of the matrix, such that for every $A \in \mathbb{C}^{d\times d}$ whose entries satisfy $|\operatorname{Re} a_{ij}|, |\operatorname{Im} a_{ij}| \le 2^p$, the unitary $\mathcal{V}(U_{\mathrm{QRAM}}(A))$ obtained with the QRAM loaded by the program is an $(\|A\|_F, w, \xi)$-block-encoding of $A$:

$$\bigl\| \|A\|_F\,(\langle 0|_w \otimes I)\,\mathcal{V}\,(|0\rangle_w \otimes I) - A \bigr\| \le \xi .$$

This is the data-structure route to block-encodings of classically stored dense matrices, with subnormalization the Frobenius norm and only polylogarithmic quantum cost.

Formalization Note Corrected statement. The source gives no cost model for classical arithmetic, does not say in which parameters $p$ is polylogarithmic, and does not say how the costs depend on $\xi$. Here classical cost is the length of a straight-line real-arithmetic program (the model of the Cor. 5.45 chunk), $p = \widetilde{O}(1)$ means $p \le C_0 L^{c_0}$ for arbitrary $C_0, c_0$, all $\widetilde{O}$ bounds are polylogarithmic in $d$ and $1/\xi$, and the QRAM size is $\widetilde{O}(d^2 p)$ rather than $O(d^2 p)$ because the word size must grow with $\log(1/\xi)$. A $p$-bit entry is modelled by the magnitude bound $2^p$ on its real and imaginary parts.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Proposition 7.9: Iterative refinement reaches residual ϵ in O(log 1/ϵ) iterations.
• Proposition 7.14: Product of block-encodings (error term corrected).
• Proposition 7.18: Linear combination of block-encodings (error term corrected for α < 1).
• Lemma 7.20: Block-encoding of the diagonal matrix of inner products ⟨ϕ_j|ψ_j⟩.
• Proposition 7.21: Block-encoding from sparse-access oracles (rotation cost and entry encoding made explicit).
• Lemma 7.37: A bounded polynomial of degree Õ(β) approximating exp(2βx)/4 on [−1, 0].
• Lemma 7.39: Block-encoding a density matrix from a unitary preparing its purification.
• Proposition 7.41: One-copy trace estimator: a random variable with bias ≤ θ/4 for Tr(Aρ) and constant variance.
• Proposition 7.38: Gibbs-state preparation from a block-encoding of H, for the polynomial of Lemma 7.37 made explicit.
• Proposition 7.29: A (‖A‖_F, Õ(q), ξ)-block-encoding of a classical matrix from QRAM, with an explicit cost model.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Giacomo Nannicini, Quantum algorithms for optimizers, 2025, v5; notes dated 9 July 2025. https://arxiv.org/pdf/2408.07086v5.

Motivation

This mission develops Chapter 4 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

Let $f : \{0,1\}^n \to \mathbb{Z}$ take values of bit width $b$, i.e. $|f(j)| < 2^b$ for all $j$, and let $U_f : |j\rangle|k\rangle \mapsto |j\rangle|k \oplus f(j)\rangle$ evaluate $f$ in binary. Algorithm 2 with budget $T$ starts from a uniformly random incumbent $\ell$ and repeatedly runs Algorithm 1 (search with an unknown number of marked items) with the marking unitary $U_m : |j\rangle|y\rangle \mapsto |j\rangle|y \oplus \mathbb{I}(f(j) < f(\ell))\rangle$, replacing $\ell$ by the returned index $k$ whenever $f(k) < f(\ell)$; a call of Algorithm 1 that would exceed the budget is interrupted at the $T$-th application of $U_f$, and the algorithm then returns $\ell$. Each application of $U_m$ counts as one application of $U_f$ and is charged $3n + 2b + 1$ additional gates; each round of Algorithm 1 with $m$ qubits of precision is charged $m + m(m+1)/2$ further gates (Hadamards and the inverse QFT).

There are absolute constants $c, C > 0$ such that for every $n$, $b$, every such $f$ and every $\delta \in (0,1)$ the following holds. Run Algorithm 2 independently $k = \lceil \log_3(1/\delta) \rceil$ times with budget $T = \lceil c\sqrt{2^n} \rceil$ and output an $f$-minimal one of the $k$ returned indices. Then:

1. with probability at least $1 - \delta$ the output is a global minimizer of $f$;
2. on every outcome, the total number of applications of $U_f$ (including the $k$ evaluations used to select the output) is at most

$$C\sqrt{2^n}\,\bigl(1 + \log(1/\delta)\bigr),$$

and the number of additional gates is at most $C\sqrt{2^n}\,(n + b + 1)\,(1 + \log(1/\delta))$.

This is the quadratic quantum speedup for unstructured minimization, the basis of the optimization applications of Grover search.

Formalization Note The source's $\tilde O(\sqrt{2^n})$ gate bound is stated with the suppressed polylogarithmic factors $n + b + 1$ and $1 + \log(1/\delta)$ explicit, the interruption rule for the budget is made explicit, and $T$, $k$ are the choices of the source's proof. Algorithm 1 is the shared formalization of the earlier corollary; the outcome law is a weight on (returned index, applications of $U_f$, gates).

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Theorem 4.6: Amplitude amplification: overlap 2/3 with the good state using O(1/√p) applications of S and R.
• Corollary 4.9: Search with a known number of marked elements in O(√(2^n/|M|)) oracle calls.
• Corollary 4.10: Finding all marked elements with O(√(|M| 2^n)) oracle calls.
• Lemma 4.11: Oblivious amplitude amplification: the partner state Ψ⊥ is orthogonal to |0⟩|ψ⟩ and has no flag-0 support.
• Theorem 4.12: Oblivious amplitude amplification: each iteration rotates by 2θ.
• Proposition 4.15: Eigenstates of the Grover operator in amplitude estimation.
• Proposition 4.19: Angle error to probability error for sin².
• Proposition 4.21: Error bound of amplitude estimation with m qubits.
• Corollary 4.22: Amplitude estimation to additive error ε with O(log 1/ε) qubits and O(1/ε) queries.
• Lemma 4.28: Near-orthogonality of the two amplitude-estimation output states.
• Theorem 4.29: Quantum search without knowing the number of marked items: O(1/θ) expected queries.
• Corollary 4.30: Search without knowing |M| with O(√(2^n/|M|)) expected oracle calls.
• Theorem 4.31: Quantum minimum finding (Dürr–Høyer), with explicit bit width, interruption and gate model.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Giacomo Nannicini, Quantum algorithms for optimizers, 2025, v5; notes dated 9 July 2025. https://arxiv.org/pdf/2408.07086v5.

Motivation

In the AdS/CFT correspondence a quantum theory of gravity in an asymptotically anti-de Sitter spacetime is equivalent to a conformal field theory on its boundary. A central question is how local bulk physics is encoded in the boundary theory, and in particular which bulk region is described by a given boundary subregion $R$. Harlow's TASI 2017 lectures (arXiv:1802.01040) review the answer that emerged from quantum error correction: the boundary Hilbert space is a code, bulk effective field theory lives in a code subspace, and the boundary subregion $R$ can reconstruct every bulk operator in its entanglement wedge. The lectures state as their main technical target the theorem that this entanglement wedge reconstruction, the quantum Ryu–Takayanagi (RT) formula with a central area operator, and the JLMS formula (equality of boundary and bulk relative entropies) are mathematically equivalent. All of these statements are finite-dimensional linear algebra, which makes them formalizable now.

Timeline. Almheiri, Dong and Harlow proposed the quantum-error-correction interpretation of AdS/CFT in 2014 (arXiv:1411.7041). Jafferis, Lewkowycz, Maldacena and Suh derived the JLMS relation in 2015 (arXiv:1512.06431), and Dong, Harlow and Wall established the implications between JLMS and reconstruction for factors in 2016 (arXiv:1601.05416). Harlow proved the general three-way equivalence for arbitrary finite-dimensional von Neumann algebras in 2016 (arXiv:1607.03901, Comm. Math. Phys. 2017). The TASI lectures (2017, published 2018) present this theorem as Theorem 5.2.

Setting

All Hilbert spaces are finite-dimensional. The boundary space factorizes as $\mathcal H=\mathcal H_R\otimes\mathcal H_{\overline R}$. A code subspace $\mathcal H_{code}\subseteq\mathcal H$ is described by an isometry $V$ whose columns $|\tilde i\rangle$ are an orthonormal basis of $\mathcal H_{code}$. An operator $O_R$ on $\mathcal H_R$ represents a logical operator $\tilde O$ if $O_R|\tilde\psi\rangle=\tilde O|\tilde\psi\rangle$ and $O_R^\dagger|\tilde\psi\rangle=\tilde O^\dagger|\tilde\psi\rangle$ for every code state.

A von Neumann algebra $M$ on $\mathcal H_{code}$ is a set of operators closed under sums, products and adjoints and containing all multiples of the identity; $M'$ is its commutant and $Z_M=M\cap M'$ its center. Every such $M$ is block diagonal, $\mathcal H_{code}=\bigoplus_\alpha\mathcal H_{r_\alpha}\otimes\mathcal H_{\overline r_\alpha}$ with $M=\bigoplus_\alpha\mathcal L(\mathcal H_{r_\alpha})\otimes I_{\overline r_\alpha}$. For a state $\tilde\rho$ with diagonal blocks $p_\alpha\tilde\rho_{r_\alpha\overline r_\alpha}$, the algebraic entropy is $S(\tilde\rho,M)=-\sum_\alpha p_\alpha\log p_\alpha+\sum_\alpha p_\alpha S(\tilde\rho_{r_\alpha})$, and the algebraic relative entropy $S(\tilde\rho|\tilde\sigma,M)$ is defined analogously (eqs. (5.16), (5.18)).

Formalization targets

Goal: Theorem 5.2 (entanglement wedge reconstruction theorem)

For $\mathcal H_{code}\subseteq\mathcal H_R\otimes\mathcal H_{\overline R}$ and a von Neumann algebra $M$ on $\mathcal H_{code}$, the following are equivalent:

$$\text{(1) every } \tilde O\in M \text{ is represented on } R \text{ and every } \tilde O'\in M' \text{ on } \overline R;$$ $$\text{(2) } \exists\,\mathcal L_R\in Z_M:\ S(\tilde\rho_R)=\mathrm{Tr}(\tilde\rho\mathcal L_R)+S(\tilde\rho,M),\ \ S(\tilde\rho_{\overline R})=\mathrm{Tr}(\tilde\rho\mathcal L_R)+S(\tilde\rho,M')\ \ \forall\tilde\rho;$$ $$\text{(3) } S(\tilde\rho_R|\tilde\sigma_R)=S(\tilde\rho|\tilde\sigma,M),\ \ S(\tilde\rho_{\overline R}|\tilde\sigma_{\overline R})=S(\tilde\rho|\tilde\sigma,M')\ \ \forall\tilde\rho,\tilde\sigma.$$

Milestones

• Theorem 4.1: four equivalent characterizations of a correctable erasure of $\overline R$ (operator reconstruction on $R$; $PX_{\overline R}P=\lambda P$; decoupling of a reference system from $\overline R$; the explicit encoding $|\tilde i\rangle=U_R(|i\rangle_{R_1}|\chi\rangle_{R_2\overline R})$).
• Eq. (4.25): the quantum Singleton bound $m\ge\frac{n+k}{2}$ for codes whose accessibility depends only on the number of qudits.
• Theorem 5.1: every von Neumann algebra on a finite-dimensional Hilbert space is a block-diagonal direct sum of factors, with the matching descriptions of $M'$ and $Z_M$.

Significance

Theorem 5.2 turns three separately motivated features of holography into a single mathematical statement. Since the RT formula is independently derived from the gravitational path integral, the theorem implies subregion duality in the entanglement wedge; it also shows that a non-trivial area operator requires an algebra with non-trivial center. Theorem 4.1 is the subsystem-code special case, and Theorem 5.1 is the structure result that gives the algebraic entropies their meaning.

The results are proved in the literature (Harlow 2017 for Theorem 5.2; Theorems 4.1 and 5.1 are standard), but the lectures state Theorem 5.2 without proof, and none of these statements has a machine-checked proof that this mission is aware of. The mission produces formal statements and, eventually, formal proofs of the finite-dimensional structure theory of operator-algebra quantum error correction.

Difficulty

The three conditions live at different levels: (1) is a statement about operators, (2) about von Neumann entropies of single states, and (3) about relative entropies of pairs of states. Passing between them requires control of the full block structure of $M$ relative to the bipartition $R\overline R$, not only of a single factor, and the classical term $\sum_\alpha p_\alpha\log(p_\alpha/q_\alpha)$ of (5.18) couples different blocks, so the general case does not reduce to the factor case treated earlier in the literature. Relative entropies can be infinite (when supports are not nested), so the equalities in (3) are equalities of extended reals and every argument must remain valid at $+\infty$.

Formalization scope

Hilbert spaces are coordinate spaces $\mathbb C^{\iota}$ for finite index types, operators are complex matrices, tensor products are Kronecker products, and $\mathcal H_{code}$ is the image of an isometry $V$ (an operator $O_R$ acts on code states as $O_R\otimes I_{\overline R}$ applied to $V$). States are density matrices (positive semidefinite, trace one). Von Neumann entropy and relative entropy are defined from eigen-decompositions; relative entropy takes values in the extended reals. A von Neumann algebra is a $*$-subalgebra of matrices; the algebraic entropies are computed in a block decomposition $U$ of $M$, which every statement takes as an arbitrary decomposition realizing $M$ (the value does not depend on the choice). The RT identity is stated as an equality of complex numbers. Theorem 4.1 assumes a nonzero code subspace; the Singleton bound assumes $d\ge2$ and $k\ge1$; both conditions are implicit in the lectures and are needed for the statements to be true.

A trivializing reading is excluded: the hypotheses of every statement are satisfiable, and the goal is a full equivalence of three non-trivial conditions rather than any single implication.

Useful reusable infrastructure: partial traces and their interaction with Kronecker products, entropies of block-diagonal states, relative entropy (Klein's inequality and its equality case), and the structure theory of finite-dimensional $*$-algebras of matrices. Contributions of proofs of the individual implications (1)⇒(2), (2)⇒(3), (3)⇒(1) as sketches are welcome.

Selected references

• D. Harlow, TASI Lectures on the Emergence of Bulk Physics in AdS/CFT, PoS(TASI2017)002, 2018. https://arxiv.org/abs/1802.01040
• D. Harlow, The Ryu–Takayanagi Formula from Quantum Error Correction, Comm. Math. Phys. 354 (2017) 865–912. https://arxiv.org/abs/1607.03901
• A. Almheiri, X. Dong, D. Harlow, Bulk Locality and Quantum Error Correction in AdS/CFT, JHEP 04 (2015) 163. https://arxiv.org/abs/1411.7041
• D. Jafferis, A. Lewkowycz, J. Maldacena, S. J. Suh, Relative entropy equals bulk relative entropy, JHEP 06 (2016) 004. https://arxiv.org/abs/1512.06431
• X. Dong, D. Harlow, A. C. Wall, Reconstruction of Bulk Operators within the Entanglement Wedge in Gauge-Gravity Duality, Phys. Rev. Lett. 117 (2016) 021601. https://arxiv.org/abs/1601.05416

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.

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

1. 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$.
2. 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}$.
3. Existence of state two-designs in every dimension (p. 29).
4. $f(B|\cdot)\le d_B^2(d_B+1)$ (p. 6).
5. 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}$.
6. 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}$.
7. Eq. (3) (p. 2): $Q$ equals the maximum over mixtures of feasible product states.
8. Hölder step (p. 11): $\mathrm{Tr}[GW]\le\mathrm{Tr}[GV]+\|G\|_\infty\|W-V\|_1$.
9. $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