Quantum Information

Motivation

This mission develops Chapter 15 of Quantum Computing: Lecture Notes by Ronald de Wolf. 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

This is the exponential lower bound on the length of 2-query locally decodable codes.

A map $C : \{0,1\}^n \to \{0,1\}^N$ is a $(2,\delta,\varepsilon)$-locally decodable code if for every $i \in [n]$ a classical randomized algorithm making at most $2$ queries to an $N$-bit string $y$ outputs $x_i$ with probability at least $\frac12 + \varepsilon$, for every $x \in \{0,1\}^n$ and every $y$ within Hamming distance $\delta N$ of $C(x)$.

There are constants $c > 0$ and $n_0 \in \mathbb N$ such that for all $n \ge n_0$, all $N$, all $\delta > 0$, $\varepsilon > 0$, and every $(2,\delta,\varepsilon)$-locally decodable code $C : \{0,1\}^n \to \{0,1\}^N$,

$$N \ge 2^{c\,\delta^2 \varepsilon^4 n}.$$

Hence the Hadamard code, of length $2^n$, is essentially optimal among 2-query LDCs.

Formalization Note The asymptotic $2^{\Omega(\delta^2\varepsilon^4 n)}$ is read with absolute constants $c$ and $n_0$, quantified before $N, \delta, \varepsilon$ and $C$. The threshold $n_0$ is needed: the identity code with $n = N = 1$ is a $(2, \delta, 1/2)$-LDC for every $\delta < 1$, while $1 \ge 2^{c\delta^2\varepsilon^4}$ fails for every $c > 0$.

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

• §15.2, Theorem 4: Nayak: quantum random access codes need (1 - H(p))n qubits.
• §15.3, Fact 1: Katz–Trevisan normal form for decoders of locally decodable codes.
• §15.3, Theorem 5: 2-query locally decodable codes have exponential length.

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

• Ronald de Wolf, Quantum Computing: Lecture Notes, 27 August 2026. https://homepages.cwi.nl/~rdewolf/qcnotes.pdf.

Motivation

This mission develops Chapter 20 of Quantum Computing: Lecture Notes by Ronald de Wolf. 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

This is the Gottesman–Knill theorem.

Let $\mathcal P_n=\{\pm1,\pm i\}\cdot\{I,X,Y,Z\}^{\otimes n}$ be the $n$-qubit Pauli group. A measurement-controlled Clifford circuit family $F=\{C_n\}$ consists, for each number of qubits $n$, of a sequence of at most $s(n)$ operations, $s$ a polynomial, each of which is a Pauli gate, a Hadamard gate $H$, the phase gate $S=\mathrm{diag}(1,i)$, a CNOT gate, or the projective measurement of a Pauli $M\in\{I,X,Y,Z\}^{\otimes n}$ with projectors $M_\pm=(I\pm M)/2$. The next operation is computed from $n$, a string $r$ of $q(n)$ uniformly random bits ($q$ a polynomial) and the outcomes of the earlier measurements by a classical polynomial-time algorithm. Running $C_n$ on the computational basis state $|x\rangle$, $x\in\{0,1\}^n$, produces a random final pure state $|\psi\rangle$; write $\mathcal D_F(n,x)$ for the distribution of its density matrix $|\psi\rangle\langle\psi|$.

A stabilizer description (tableau) is a list $P^{(1)},\dots,P^{(n)}\in\mathcal P_n$ with phases $\pm1$ that pairwise commute, are independent (none is a phase times a product of the others) and do not generate $-I$; it describes the state with density matrix $\prod_{j=1}^n \tfrac12(I+P^{(j)})$.

Theorem. For every measurement-controlled Clifford circuit family $F$ there is a randomized classical polynomial-time algorithm $A$ such that for every $n$ and every $x\in\{0,1\}^n$:

1. every possible output of $A$ on input $(n,x)$ is the encoding of a stabilizer description $T=(P^{(1)},\dots,P^{(n)})$;
2. the distribution of the described state satisfies

$$\Pr_{A}\Big[\textstyle\prod_{j=1}^n \tfrac12\big(I+P^{(j)}\big)=\rho\Big]=\Pr_{\mathcal D_F(n,x)}\big[|\psi\rangle\langle\psi|=\rho\big]\quad\text{for every matrix }\rho .$$

Thus Clifford circuits with intermediate Pauli measurements and classical (randomized) control, started on a basis state, can be sampled exactly by a classical computer; the quantum advantage requires non-Clifford resources such as the $T$ gate.

Formalization Note The source says the simulator is "given C"; following its own remark on p.187 that one strictly has to speak of families $\{C_n\}$, the simulator is fixed for the family (chosen before $n$ and $x$) and receives $(n,x)$ encoded as a bit string. Polynomial time is the Turing-machine notion PolyTimeComputable of this repository, applied to the input followed by a uniformly random string of polynomial length. Distributions over states are compared via density matrices, so the global phase is ignored, as in the source's footnote 3 on p.185.

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

• §20.3, Theorem 6: Gottesman–Knill: measurement-controlled Clifford circuits are efficiently classically simulable.
• §20.3, Theorem 6: Gottesman–Knill: measurement-controlled Clifford circuits are efficiently classically simulable.

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

• Ronald de Wolf, Quantum Computing: Lecture Notes, 27 August 2026. https://homepages.cwi.nl/~rdewolf/qcnotes.pdf.

Motivation

This mission develops Chapter 5 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

This is a corrected form of the quantum construction of a separation oracle from a membership oracle.

Quantum membership oracle. Points of $\mathbb{R}^d$ are written in an $m$-qubit register through an encoding $p \mapsto \mathrm{enc}(p)$. A quantum oracle implementing $\mathrm{MEM}_{0,\epsilon'}(K)$ is a unitary $O$ acting on the point register, an answer qubit and $k$ workspace qubits. On every basis point it acts as

$$O\,|p\rangle|0\rangle|0^k\rangle = |p\rangle|\varphi_p\rangle ,$$

where measuring the answer qubit of $\varphi_p$ returns the correct membership bit $[\mathrm{enc}(p) \in K]$ with probability at least $1-\epsilon'$.

Separation oracle. $\mathrm{SEP}_{\epsilon,\delta}(x)$ (Definition 5.22) must, with probability at least $1-\delta$, either assert $x \in B_2(K,\epsilon)$ or return a unit vector $g$ with $\langle g, y\rangle \le \langle g, x\rangle + \epsilon$ for all $y \in B_2(K,-\epsilon) = \{y : B_2(y,\epsilon) \subseteq K\}$.

Theorem. There are absolute constants $C > 0$ and $c \in \mathbb{N}$ with the following property. Let $d \in \mathbb{N}$ and $r, R, \epsilon, \delta \in \mathbb{R}$ with $0 < r < R$, $0 < \epsilon < R$ and $0 < \delta < 1/3$. Then there is $\epsilon' > 0$ such that for every $x \in \mathbb{R}^d$ there exist an encoding $\mathrm{enc}$ and, for every workspace size $k$, a quantum circuit with measurement decoding. The circuit makes at most

$$C\,\bigl(\log(2+d) + \log(2+R) + \log(2+1/r) + \log(2+1/\epsilon) + \log(2+1/\delta)\bigr)^{c}$$

uncontrolled calls to the oracle or its inverse. It correctly implements $\mathrm{SEP}_{\epsilon,\delta}(x)$ for every convex $K$ with $B_2(0,r) \subseteq K \subseteq B_2(0,R)$ and $x \notin B_2(K,-\epsilon)$, and for every unitary implementing $\mathrm{MEM}_{0,\epsilon'}(K)$.

Classically, separation from membership needs $\tilde O(d)$ membership calls. This result gives an exponential improvement in the dimension for the query complexity of convex optimization with a membership oracle.

Formalization Note The source leaves several objects open: the unitary implementing $\mathrm{MEM}$, the value of $\epsilon'$, and the parameters hidden in $\tilde O(1)$. The statement makes each of them explicit. The unit-norm requirement on $g$ is added because Definition 5.22 as printed accepts $g = 0$, which would make the separation oracle trivial.

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 5.3: Jordan's gradient circuit recovers the gradient of an exactly representable linear function.
• Proposition 5.6: The gradient algorithm for approximately linear functions.
• Proposition 5.16: A Hadamard-test circuit is a probability oracle for (1 + Re⟨ψ|ϕ_x⟩)/2.
• Corollary 5.18: Pure-state tomography with Euclidean error using Õ(d/ϵ) uses of U.
• Proposition 5.25: Properties of the height function: convexity, Lipschitz continuity, and separation from an ϵ̄-subgradient (corrected).
• Lemma 5.28: The central-difference gradient is within (η/2)Δ^(η)f(x) of every subgradient.
• Lemma 5.30: The Laplace approximation is at most dL/r on average over a cube.
• Lemma 5.32: Deviation from the finite-difference linearization on the ℓ1 ball is at most (η²/2)Δ^(η)f(z).
• Proposition 5.31: Finite differences of an approximate function at a random point give an explicit ϵ′-subgradient at the origin (corrected).
• Proposition 5.36: Algorithm 4 (binary tree of controlled R_Y rotations) prepares the amplitude encoding of a real unit vector.
• Corollary 5.37: Amplitude encoding of a complex vector to error ϵ with Õ(d) gates from {H, T, CX}.
• Corollary 5.45: Amplitude encoding with O(log d) QRAM queries and O(log d (log d + log 1/ϵ)) two-qubit gates after Õ(d) classical preprocessing (corrected).
• Theorem 5.33: Separation oracle from polylogarithmically many calls to a quantum membership oracle (corrected).

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 7 of Stabilizer Codes and Quantum Error Correction 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

Fix an erasure probability $p \in [0,1]$. The qubit erasure channel $\mathcal N_p$ acts independently on each qubit sent: with probability $1-p$ the qubit passes unchanged together with a classical flag $0$, and with probability $p$ it is replaced by the maximally mixed state $I/2$ together with the flag $1$, so that the receiver knows which qubits were erased. On $n$ qubits the channel is $\mathcal N_p^{\otimes n}$.

A rate $R \in \mathbb R$ is achievable (for quantum codes, equivalently one-way entanglement purification) if for every $\varepsilon > 0$ and $\delta > 0$ there is $N_0$ such that for every $n \ge N_0$ there are a number $k \ge (R-\delta)n$ of logical qubits, an encoding quantum channel $\mathcal E$ from $k$ qubits to $n$ qubits and a decoding quantum channel $\mathcal D$ from the channel output (qubits and erasure flags) to $k$ qubits with

$$F_e\big(\mathcal D \circ \mathcal N_p^{\otimes n} \circ \mathcal E\big) \ge 1 - \varepsilon,$$

where $F_e(\Phi) = \langle \Phi_k | (\mathrm{id} \otimes \Phi)(|\Phi_k\rangle\langle \Phi_k|) | \Phi_k \rangle$ is the entanglement fidelity with respect to the maximally entangled state $|\Phi_k\rangle$ of two $k$-qubit registers. The theorem states that the quantum capacity of the erasure channel is $\max(0, 1-2p)$, in the strong form that the set of achievable rates is exactly

$$\{R : R \text{ achievable for } \mathcal N_p\} = \big(-\infty,\ \max(0, 1-2p)\big].$$

In particular every rate below $1-2p$ is achievable (random stabilizer codes), no rate above $1-2p$ is (a no-cloning argument), and for $p \ge 1/2$ the capacity is zero.

Formalization Note The supremum of achievable rates is not written as a real sSup (which would be junk on an empty or unbounded set); instead the achievable set itself is characterized. Because the definition of achievability already has the slack $\delta$, the achievable set is closed, so the capacity $\max(0,1-2p)$ is itself an achievable rate. The author's errata note that the thesis's proof of the upper bound assumes there is no superadditivity when a noiseless channel is added to a zero-rate channel; the theorem itself is the established value (Bennett–DiVincenzo–Smolin).

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

• §7.5: The quantum capacity of the erasure channel is max(0, 1 − 2p).

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, Stabilizer Codes and Quantum Error Correction, 1997 thesis, downloaded arXiv v1 PDF; PDF title page now prints 2024. https://arxiv.org/pdf/quant-ph/9705052v1.

Motivation

This mission develops Chapter 4 of A Survey of Quantum Learning Theory by Srinivasan Arunachalam and Ronald de Wolf. 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

This is Aaronson's theorem on "pretty good tomography": an $n$-qubit state can be PAC-learned from linearly many (in $n$) measurement results.

An $n$-qubit state is a density matrix $\rho\in\mathbb C^{2^n\times 2^n}$ (positive semidefinite, trace $1$). A two-outcome measurement is an effect $E$, i.e. $0\preceq E\preceq \mathrm{Id}$; its first outcome has probability $\mathrm{Tr}(E\rho)$. Let $D$ be a probability distribution (Borel) on the set of effects.

There is a polynomial $p$ in three variables with nonnegative coefficients such that for every $n$ and all $\varepsilon,\gamma>0$, $\delta\in(0,1)$ there are a number

$$T\ \le\ n\cdot p\big(1/\varepsilon,\ 1/\gamma,\ \log(1/\delta)\big)$$

and a (measurable) learner $L$, mapping $T$ measurement results to an $n$-qubit density matrix, with the following property: for every $n$-qubit state $\rho$ and every distribution $D$, if $E_1,\dots,E_T$ are drawn i.i.d. from $D$ and, independently given the $E_i$, each $b_i$ is a bit with $\Pr[b_i=1]=\mathrm{Tr}(E_i\rho)$, then with probability at least $1-\delta$ the output $\sigma=L((E_1,b_1),\dots,(E_T,b_T))$ satisfies

$$\Pr_{E\sim D}\big[\,|\mathrm{Tr}(E\sigma)-\mathrm{Tr}(E\rho)|>\gamma\,\big]\ \le\ \varepsilon .$$

The learner knows neither $\rho$ nor $D$. Only the number of measurement results is bounded, not the running time.

Formalization Note "$T=n\cdot\mathrm{poly}$" is read as an upper bound on $T$ (a learner may ignore extra results). The condition $\delta<1$ is added: for $\delta\ge 1$ the claim is empty and $\log(1/\delta)\le 0$. The learner is deterministic and measurable; the probability of success is written out as an integral over $D^{T}$ of the probabilities of the bit strings.

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

• §4.1.1, Theorem 4.3: Servedio–Gortler: quantum exact learning needs Ω(max{1/√γ(C), log|C|/n}) queries.
• §4.1.1, Corollary 4.4: Servedio–Gortler: D(C) = O(n·Q(C)^3).
• §4.1.2, Theorem 4.5: Classical (N,M)-query complexity of exact learning is Θ(min{M,N}).
• §4.1.2, Theorem 4.6: Kothari: optimal quantum (N,M)-query complexity of exact learning.
• §4.1.2, Theorem 4.8: Kothari: quantum exact learning with O(√((1/γ)/log(1/γ))·log|C|) queries.
• Theorem 4.12: Quantum PAC learning needs Ω(d/ε + log(1/δ)/ε) quantum examples.
• Theorem 4.13: Diagonal of the square root of an XOR-invariant Gram matrix (corrected: with the factor 2^{-k/2}).
• Theorem 4.15: Quantum agnostic learning needs Ω(d/ε² + log(1/δ)/ε²) quantum examples.
• Theorem 4.16: Quantum states are PAC-learnable from n·poly(1/ε, 1/γ, log(1/δ)) measurement results.

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

• Srinivasan Arunachalam and Ronald de Wolf, A Survey of Quantum Learning Theory, 2017, v3. https://arxiv.org/pdf/1701.06806v3.

Motivation

This mission develops Chapter 30 of Lecture Notes on Quantum Algorithms by Andrew Childs. 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

This is the quantitative quantum adiabatic theorem.

There are absolute constants $c_1, c_2, c_3 > 0$ (the constants of the first- and second-order perturbation bounds $\|\dot P\| \le c_1 \|\dot H\|/\Delta$ and $\|\ddot P\| \le c_2\|\ddot H\|/\Delta + c_3\|\dot H\|^2/\Delta^2$) with the following property. Let $\mathcal H = \mathbb C^{d}$ be a finite-dimensional Hilbert space with $d \ge 2$, and let $H(s)$, $s \in [0,1]$, be a twice continuously differentiable family of Hermitian operators on $\mathcal H$, with derivatives $\dot H(s)$ and $\ddot H(s)$ (one-sided at the endpoints). Suppose that for every $s \in [0,1]$ the ground state of $H(s)$ is nondegenerate, and let $\Delta(s) > 0$ be the gap between the smallest eigenvalue $E(s)$ of $H(s)$ and the nearest distinct eigenvalue. Norms of operators are spectral norms. Let $\epsilon > 0$ and let the total evolution time $T$ satisfy

$$T \ge \frac{2}{\epsilon}\left[c_1\frac{\|\dot H(0)\|}{\Delta(0)^2} + c_1\frac{\|\dot H(1)\|}{\Delta(1)^2} + \int_0^1 \left((3c_1^2 + c_1 + c_3)\frac{\|\dot H(s)\|^2}{\Delta(s)^3} + c_2\frac{\|\ddot H(s)\|}{\Delta(s)^2}\right) ds\right].$$

If $|\psi(s)\rangle$ solves the Schrödinger equation $i\,\frac{d}{ds}|\psi(s)\rangle = T\,H(s)|\psi(s)\rangle$ on $[0,1]$ and $|\psi(0)\rangle$ is a unit ground state of $H(0)$, then there is a unit ground state $|\phi(1)\rangle$ of $H(1)$ with

$$\big\|\,|\psi(1)\rangle - |\phi(1)\rangle\,\big\| \le \epsilon.$$

The theorem quantifies how slowly a Hamiltonian must be varied for a system started in its ground state to end close to the final ground state, with the required time governed by the spectral gap; it underlies adiabatic optimization and adiabatic quantum computation.

Formalization Note The instantaneous ground state $|\phi(1)\rangle$ is fixed only up to a global phase, so the conclusion asserts the existence of some unit ground state of $H(1)$ within $\epsilon$. The constants are quantified before the dimension and the Hamiltonian. The derivatives $\dot H, \ddot H$ are given as functions with derivative-within-$[0,1]$ hypotheses and $\ddot H$ continuous; the gap is the difference of the two smallest eigenvalues counted with multiplicity, which equals the source's $\Delta$ when the ground state is nondegenerate.

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 30.1: Quantitative adiabatic theorem.

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

• Andrew Childs, Lecture Notes on Quantum Algorithms, 17 April 2025. https://www.cs.umd.edu/~amchilds/qa/qa.pdf.

Motivation

This mission develops Chapter 5 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

There exist an $[[n,1,2t+1]]$ code with fault-tolerant gadgets of a common depth (Definitions 2–5) and a threshold $p_T>0$ with the following property. For every $p$ with $0\le p<p_T$ there are constants $K>0$ and $c\in\mathbb N$ such that for every ideal circuit $C$ (Definition 6: preparation, $H$, $R_{\pi/8}$, CNOT, wait and measurement locations, no input) and every $\varepsilon>0$ there is a level $L$ for which the $L$-fold concatenated fault-tolerant simulation $C'=C^{(L)}$ satisfies

1. $\#\mathrm{qubits}(C')\le K\,\big(\log_2(2+|C|/\varepsilon)\big)^{c}\,\#\mathrm{qubits}(C)$ and $\#\mathrm{steps}(C')\le K\,\big(\log_2(2+|C|/\varepsilon)\big)^{c}\,\#\mathrm{steps}(C)$, where $|C|$ is the number of locations of $C$;
2. for every local stochastic error model on $C'$ (Definition 12) with error bounds $p_i\le p$, $p_i<1$,

$$d_{\mathrm{TV}}\big(\text{decoded output of } C',\ \text{output of } C\big)\le\varepsilon.$$

The output of $C'$ is decoded classically level by level. The threshold theorem shows that arbitrarily long quantum computations can be performed reliably with polylogarithmic overhead once the physical error rate is below a constant.

Formalization Note The fault-tolerant circuit is pinned to the concatenated circuit of the proof (p.42); an unconstrained circuit with free classical computation could sample the output of $C$ classically. $\mathrm{polylog}(x)$ is encoded as $K(\log_2(2+x))^c$, which is positive also for $x\le 1$.

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

• §5.1, Theorem 6: Good implies correct: an extended rectangle with at most t faults is correct.
• §5.2, Theorem 7: A fault-tolerant circuit with only good ExRecs has the ideal output distribution.
• §5.2, Lemma 2: *Correctness for the ideal decoder implies correctness for a -decoder.
• §5.2, Lemma 3: *A good truncated ExRec is correct for ideal decoders and -decoders.
• Theorem 8: A fault-tolerant circuit simulates the ideal circuit with errors at the bad ExRecs.
• Theorem 9: Level reduction: a local stochastic model on C′ induces one on C with bounds Σ_{|R|=t+1} Π p_j.
• Theorem 10: Threshold theorem: below p_T, concatenated circuits simulate C to distance ε with polylog overhead.

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

Simulating the time evolution $e^{-iHt}$ of a many-body Hamiltonian is one of the main proposed uses of quantum computers. For a Hamiltonian $H = \sum_X h_X$ whose terms act on small, nearby groups of sites of a lattice, Haah, Hastings, Kothari and Low give a quantum algorithm whose gate count is nearly linear in the space-time volume $n t$, and show that this is optimal up to logarithmic factors. The algorithm decomposes $e^{-iHt}$ into evolutions of overlapping blocks, and the error of each step is controlled by a Lieb–Robinson bound: in a locally interacting system, an operator evolved for time $t$ stays, up to a superexponentially small error, inside a region whose size grows linearly with $t$.

Lieb–Robinson bounds go back to Lieb and Robinson (1972), who proved a finite propagation speed for quantum spin systems. Hastings (2004), Nachtergaele and Sims (2006) and Hastings and Koma (2006) gave the commutator form used today and applied it to the decay of correlations in gapped ground states. Appendix C of the paper re-derives the bound in a self-contained way. Section C.4 treats strictly local interactions, where every term is supported on a set of diameter at most $1$, and obtains a bound with an explicit factor $(2\zeta_0|t|)^\ell/\ell!$. This mission formalizes that bound.

Setting

Let $\Lambda$ be a finite set of sites with a metric $\mathrm{dist}$. Every site carries $\mathbb{C}^q$, and operators act on $\bigotimes_{x \in \Lambda} \mathbb{C}^q$; all norms $\|\cdot\|$ are operator norms. An operator is supported on $X \subseteq \Lambda$ if it has the form $m \otimes \mathbb{1}_{\Lambda \setminus X}$. For finite sets of sites, $\mathrm{dist}(X, Y) = \min_{x \in X, y \in Y} \mathrm{dist}(x, y)$, $\mathrm{diam}(X) = \max_{x, x' \in X} \mathrm{dist}(x, x')$, and $X \sim Y$ means $X \cap Y \ne \emptyset$.

A Hamiltonian is a family $(h_X)_{X \subseteq \Lambda}$ of Hermitian operators, $h_X$ supported on $X$, with $H = \sum_{X \subseteq \Lambda} h_X$; for a region $\Omega$, $H_\Omega = \sum_{Z \subseteq \Omega} h_Z$. The Heisenberg evolution of an operator $O$ is $O(t; J) = e^{iJt} O e^{-iJt}$, and $O(t) = O(t; H)$. The interaction is strictly local if $h_X = 0$ whenever $\mathrm{diam}(X) > 1$, and its strength is measured by

$$\zeta_0 = \max_{x \in \Lambda} \sum_{Q \ni x} |Q|\, \|h_Q\| .$$

The proof works with two auxiliary quantities attached to a fixed operator $B$ supported on $Y$:

$$C_B(X, t) = \sup_{A \in \mathcal{A}_X,\ \|A\| \le 1} \|[A(t), B]\|, \qquad D_B(X, t) = \|[h_X(t), B]\|,$$

where $\mathcal{A}_X$ is the algebra of operators supported on $X$. A tuple $(Z_1, \dots, Z_k)$ is linked from $X$ if $X \sim Z_1 \sim \cdots \sim Z_k$.

Formalization targets

Goal: display (48)

For $A$ supported on $X$, $B$ supported on $Y$, $\ell = \lfloor \mathrm{dist}(X, Y) \rfloor$ and every real $t$,

$$\|[A(t), B]\| \le 2\,\|A\|\,\|B\|\,|X|\,\frac{(2\zeta_0|t|)^{\ell}}{\ell!} .$$

Milestones

1. The elementary bounds (28): $C_B(Z, 0) \le 2\|B\|\delta_{Z \sim Y}$, $C_B(Z, t) \le 2\|B\|$, and the same for $D_B$ with an extra factor $\|h_Z\|$.
2. The integral inequality (24): $C_B(X, t) \le C_B(X, 0) + \sum_{Z \sim X} 2\int_0^{|t|} D_B(Z, s)\, ds$.
3. The closed recursion (42): $C_B(X, t) \le C_B(X, 0) + 2\sum_{Z : X \sim Z} \|h_Z\| \int_0^{|t|} C_B(Z, s)\, ds$.
4. The truncated iteration (44): $C_B(X, t) \le 2\|B\| \frac{(2|t|)^\ell}{\ell!} \sum_{Z_1, \dots, Z_\ell : \text{linked}} \prod_j \|h_{Z_j}\|$.
5. The counting bounds (45)–(46): $\sum_{Q : P \sim Q \sim S} \|h_Q\| \le \zeta_0 \sum_{p \in P} \delta_{\mathrm{dist}(p, S) \le 1}$ and its weighted, distance-tracking companion.
6. Lemma 5, eq. (4) = (49): $\|O_X(t; H) - O_X(t; H_\Omega)\| \le |X|\,\|O_X\|\,(2\zeta_0|t|)^\ell/\ell!$ with $\ell = \lfloor \mathrm{dist}(X, \Lambda \setminus \Omega) \rfloor$, under the added hypothesis $\mathrm{dist}(X, \Lambda \setminus \Omega) \ge 1$.

The goal is (48) rather than Lemma 5 because (48) is proved in full on pp. 26–27, while Lemma 5 is obtained "by manipulation analogous to Eq. (39)" and is false as printed when $\ell = 0$.

Significance

The bound (48) states that commutators with distant operators are suppressed by a factor that, at fixed $t$, decays faster than any exponential in the distance. The same factor controls Lemma 5, which is what the decomposition lemmas of the paper (Lemma 6 and its corollaries) use to bound the error of replacing a global evolution by evolutions of overlapping blocks; that in turn gives the paper's gate counts. Bounds of this type also underlie the exponential clustering of correlations in gapped ground states and the quasi-adiabatic continuation technique.

The results are proved in the literature and in this paper. A search of the local Prove2Me prior-art index found no matching formal statement for this finite spin-system bound. The mission seeks a machine-checked proof of the strictly local bound with its explicit constant, together with reusable infrastructure: operators supported on subsets of a tensor product of matrix algebras, their Heisenberg evolution, and an integral inequality for commutator growth.

Difficulty

The obvious argument expands $A(t) = \sum_k (it)^k \mathrm{ad}_H^k(A)/k!$ and notes that the first $\ell$ nested commutators with $B$ vanish. This does not give the stated bound: the norm of $\mathrm{ad}_H^k(A)$ grows like $k!$ times the number of growing clusters of terms, and the tail of the series is not controlled by its leading term. The explicit factor $(2\zeta_0|t|)^\ell/\ell!$, with no exponential prefactor, requires precise control of the time-dependent supremum $C_B(Z,s)$ and the combinatorics of linked chains. A second difficulty is Lemma 5, whose printed form is false at $\ell = 0$ and whose proof in the paper is a one-line reference to an analogous computation.

Formalization scope

Sites are an arbitrary finite metric space $\Lambda$ ([Fintype Λ] [MetricSpace Λ]); operators are matrices Matrix (Λ → Fin q) (Λ → Fin q) ℂ in the product basis, with the same local dimension $q$ at every site. This generalizes the paper's qubits on a lattice in $\mathbb{R}^D$. The norm is the $L^2$ operator norm (Matrix.Norms.L2Operator), never the entrywise or Frobenius norm. SupportedOn X M states $M = m \otimes \mathbb{1}$ entrywise, and is not vacuous: a nonzero operator on a single site satisfies it, and only scalars are supported on $\emptyset$. The Hamiltonian is time-independent and sums over every subset of $\Lambda$; strict locality is the hypothesis $1 < \mathrm{diam}(X) \Rightarrow h_X = 0$ on the terms. The constant $\zeta_0$ is carried as an upper bound of the site sums $\sum_{Q \ni x} |Q|\,\|h_Q\|$, which is equivalent to the paper's maximum for these monotone bounds; no bound $\|h_X\| \le 1$ is assumed. $\mathrm{dist}(X, Y)$ is a minimum over nonempty sets and $0$ if a set is empty, $\ell$ is its natural-number floor, and $C_B$ is a real supremum over a nonempty set bounded by $2\|B\|$. The integral milestones (24) and (42) are stated for $t \ge 0$; the goal, (44) and Lemma 5 hold for every real $t$. Lemma 5 carries one disclosed added hypothesis, $\mathrm{dist}(x, y) \ge 1$ for $x \in X$, $y \notin \Omega$, without which it is false.

None of the statements is trivialized: the goal mentions neither $C_B$ nor linked sums, its norm is the operator norm, the integrals are of continuous functions on compact intervals, the supremum is over a nonempty bounded set, and no disjointness of $X$ and $Y$ is assumed, so it covers $\ell = 0$ as well.

A complete development needs the derivative of $t \mapsto e^{iHt} A e^{-iHt}$, unitarity of $e^{iHt}$ for Hermitian $H$, commutation of operators with disjoint supports, Grönwall-type iteration of integral inequalities, and the simplex-volume identity $\int_{\Delta^k} dt = |t|^k/k!$. The support and evolution layer is reusable for any lattice-system result. Contributions that prove the milestones in order, or that develop the support calculus independently, are welcome.

Selected references

• J. Haah, M. B. Hastings, R. Kothari, G. H. Low, Quantum algorithm for simulating real time evolution of lattice Hamiltonians, SIAM J. Comput. (2021); arXiv:1801.03922v4 (2020). https://arxiv.org/abs/1801.03922
• E. H. Lieb, D. W. Robinson, The finite group velocity of quantum spin systems, Comm. Math. Phys. 28 (1972) 251–257. https://doi.org/10.1007/BF01645779
• M. B. Hastings, Lieb–Schultz–Mattis in higher dimensions, Phys. Rev. B 69 (2004) 104431. https://arxiv.org/abs/cond-mat/0305505
• B. Nachtergaele, R. Sims, Lieb–Robinson bounds and the exponential clustering theorem, Comm. Math. Phys. 265 (2006) 119–130. https://arxiv.org/abs/math-ph/0506030
• M. B. Hastings, T. Koma, Spectral gap and exponential decay of correlations, Comm. Math. Phys. 265 (2006) 781–804. https://arxiv.org/abs/math-ph/0507008

Motivation

A local quantum system is built from degrees of freedom placed at sites of a lattice. Its Hamiltonian may contain many terms, each acting on a small group of sites. Even though a term is local, time evolution can spread an observable beyond its original support. A Lieb–Robinson bound limits the size of a commutator between the evolved observable and one supported elsewhere. It gives a quantitative way to say that information propagates with an effective finite velocity. The Appendix C bound of Haah, Hastings, Kothari and Low treats interactions with exponential spatial decay and makes the effect of almost commuting Hamiltonian terms explicit.

The paper studies quantum simulation, where a system's real time evolution is approximated by a circuit. Lemma 12 is an analytic ingredient: it controls how far a local observable can spread during the simulated evolution. The mission targets that lemma and the displayed estimates in its proof, with the constants printed in the pinned arXiv version. The paper proves the results; the remaining task here is to give the stated finite system version machine checked proofs.

Setting

Let $\Lambda$ be a finite set of sites equipped with a metric $\operatorname{dist}(x,y)$. Each site has the same local Hilbert space $\mathbb C^q$, and the whole system has product basis indexed by configurations $\sigma:\Lambda\to\{0,\ldots,q-1\}$. An operator supported on $X\subseteq\Lambda$ is a matrix of the form $m_X\otimes I_{\Lambda\setminus X}$: it may change the configuration on $X$, but acts as the identity on every site outside $X$. The matrix norm throughout is the spectral operator norm.

For every $X\subseteq\Lambda$, let $h_X$ be a Hermitian operator supported on $X$, and define the time independent Hamiltonian $H=\sum_{X\subseteq\Lambda}h_X$. The sum includes all subsets, including the empty set. Let

$$O(t;J)=e^{iJt}Oe^{-iJt},\qquad O(t)=O(t;H).$$

For site sets, write $X\sim Y$ when $X\cap Y\ne\varnothing$, and $\operatorname{dist}(x,Y)=\min_{y\in Y}\operatorname{dist}(x,y)$ when $Y$ is nonempty. The diameter is $\operatorname{diam}(X)=\max_{x,y\in X}\operatorname{dist}(x,y)$ for nonempty $X$. The paper imposes two quantitative conditions. First, for some $0\le\eta\le1$, every pair of terms has a small commutator:

$$\|[h_X,h_Y]\|\le 2\eta\|h_X\|\|h_Y\|.\tag{14}$$

Second, for some $\zeta,\mu>0$, the interactions decay in the weighted sense

$$\sum_{X\ni x}\|h_X\|\,|X|^2e^{\mu\operatorname{diam}(X)}\le\zeta \qquad(x\in\Lambda).\tag{15}$$

Neither condition bounds each $\|h_X\|$ by one. This matters because the result is meant to include large but nearly commuting terms. These conventions are from Appendix C.1 of the source.

Formalization targets

The goal is Lemma 12. For an operator $A$ supported on $X$ and an operator $B$ supported on a disjoint set $Y$, and every real $t$, the proposed formal statement is

$$\|[A(t),B]\|\le \frac{2}{\sqrt\eta}\|A\|\|B\| \bigl(e^{\zeta|t|\sqrt{8\eta}}-1\bigr) \sum_{x\in X}e^{-\mu\operatorname{dist}(x,Y)}. \tag{16}$$

The coefficient of $|t|$ in the exponential is proportional to $\sqrt\eta$. The goal keeps the paper's explicit factor $2/\sqrt\eta$, its $\sqrt{8\eta}$ inside the exponential, and the full sum over sites in $X$. The statement is for $\eta>0$, as the displayed formula is undefined at $\eta=0$; a family satisfying (14) with $\eta=0$ also satisfies it for any positive $\eta\le1$.

The milestones follow the source's numbered displays: the initial estimates for $C_B$ and $D_B$ in (28), their integral inequalities (24) and (27), the linked set series (32), the four estimates of Proposition 13, and the bound on its $k$th line in (37). Here $C_B(X,t)$ takes a supremum over supported operators of norm at most one, and $D_B(X,t)=\|[h_X(t),B]\|$. The milestone list is a map of the quantities that the proof controls, while the goal itself mentions only the physical operators and the two hypotheses.

Significance

The bound shows that a commutator is small when the support of $B$ is far from $X$, with a rate determined by the decay parameter $\mu$ and the small commutator parameter $\eta$. It applies to finite systems of any size with the same constants in (14) and (15). This makes it useful for reasoning about local approximations of time evolution in the quantum simulation setting of the paper. The authors also explain why a velocity proportional to $\sqrt\eta$ can occur under their hypotheses, so a linear dependence on $\eta$ is not generally available. See the discussion immediately after Lemma 12 in Appendix C.1.

Formalizing the result would supply a reusable finite matrix model of local observables and a checked version of the analytic estimates for near commuting interactions. The source paper provides a proof, but this proposed statement and its milestones currently have no machine checked proof in the mission. The definitions of support, Heisenberg evolution and linked interactions may also be reused in later formalizations of quantum lattice dynamics.

Difficulty

The obvious global norm bound $\|[A(t),B]\|\le2\|A\|\|B\|$ ignores the distance between supports. Merely bounding $\|H\|$ also loses spatial information and can grow with the whole system. The sharper statement simultaneously tracks where an interaction overlaps the current support and how the small commutator factor enters repeated interactions. A rigorous treatment must control a supremum over local operators, time dependent matrix exponentials, and an infinite series of finite linked set sums without changing any of the paper's constants.

Formalization scope

Sites form an arbitrary finite metric space, a disclosed generalization of the lattice setting used for the main algorithm. A common local dimension $q$ is used at every site; qubits occur at $q=2$. Operators are complex matrices on the configuration space $\Lambda\to\operatorname{Fin}(q)$, with Mathlib's scoped L2 operator norm. Every term is Hermitian and explicitly supported on its stated set, and $H$ is the sum over all subsets. Time is real and $H$ is constant in time. The paper mentions a piecewise continuous time dependent extension, which this mission does not state.

The goal explicitly requires $X\cap Y=\varnothing$. The printed sentence of Lemma 12 omits this, but its derivation on page 24 assumes it; without disjointness the right side is zero at $t=0$ while the left side need not be. The positive $\eta$ condition is likewise explicit. These are the two repairs to the printed lemma, and they are recorded on each relevant item. The milestones (24) and (27) are restricted to $t\ge0$, the direction for which the displayed forward integral uses $D_B(Z,s)$ and $C_B(Z\cup X,s)$.

For an empty set, the Lean point to set distance and the local set distance are taken to be zero; a supported operator on the empty set is a scalar, so its commutators vanish. $C_B$ uses a real supremum of a nonempty, bounded set, and (32) states an actual sum with HasSum. The integral milestones involve continuous finite dimensional evolution. The support definition includes nonconstant single site operators, and the $q=2$ case is part of the goal. These choices prevent the result from being obtained through a vacuous support predicate, an entrywise norm, division by zero at $\eta=0$, a default value of an unbounded supremum or divergent sum, or omitted disjointness. Contributions that establish the support calculus, matrix evolution estimates, integral inequalities, or linked set bounds are all within scope.

Selected references

• Jeongwan Haah, Matthew B. Hastings, Robin Kothari and Guang Hao Low, Quantum algorithm for simulating real time evolution of lattice Hamiltonians, SIAM Journal on Computing, 2021. arXiv:1801.03922v4, Appendix C.1–C.3, pp. 21–25.

Motivation

Deciding whether a bipartite quantum state is entangled is a basic computational problem of quantum information theory, and it is NP-hard in general (Gurvits 2003). The most widely used family of tests is the DPS hierarchy of Doherty, Parrilo and Spedalieri (DPS 2002, DPS 2004): a sequence of semidefinite programs, indexed by an integer level $\ell\ge1$, whose feasible sets shrink to the set of separable states. On the dual side, a matrix $M$ that is nonnegative on separable states is an entanglement witness, and certifying such witnesses is the problem of certifying nonnegativity of a biquadratic Hermitian form, a classical question in real algebraic geometry.

That the DPS hierarchy is, dually, a sum-of-squares hierarchy for these forms has been used repeatedly in the literature, but, as Fang and Fawzi note (arXiv:1908.05155v1, p. 4), without a formal and complete proof. Their Theorem 12 gives one. They then combine it with their sum-of-squares convergence rate on the sphere (Theorem 2 of the same paper) to recover the $O(d_B^2/\ell^2)$ convergence rate of Navascués, Owari and Plenio 2009 for the DPS hierarchy.

Timeline:

• 2002–2004: Doherty, Parrilo, Spedalieri introduce the hierarchy and prove completeness.
• 2009: Navascués, Owari, Plenio prove $h_{\mathrm{DPS}_\ell}\le(1+O(d_B^2/\ell^2))h_{\mathrm{Sep}}$ by a quantum argument.
• 2019: Fang and Fawzi prove the duality (Theorem 12) and recover the 2009 rate from sums of squares (Theorem 15).

Setting

Let $\mathcal H_A=\mathbb C^{d_A}$ and $\mathcal H_B=\mathbb C^{d_B}$. A matrix $M$ on $\mathcal H_A\otimes\mathcal H_B$ has entries $M_{ij,kl}$ (row $(i,j)$, column $(k,l)$); $\mathrm{Herm}(d_Ad_B)$ is the space of Hermitian ones.

• The separable cone $\mathcal{SEP}$ is the set of finite conic combinations $\sum_ip_i(x_ix_i^\dagger)\otimes(y_iy_i^\dagger)$, $p_i\ge0$.
• Fix $\ell\ge1$ and $\ell$ copies $B_1,\dots,B_\ell$ of $\mathcal H_B$. The DPS cone $\mathcal{DPS}_\ell$ is the set of positive semidefinite $\rho$ on $\mathcal H_A\otimes\mathcal H_B$ that have a positive semidefinite extension $\rho_{AB[\ell]}$ on $\mathcal H_A\otimes\mathcal H_B^{\otimes\ell}$ with three properties: tracing out $B_2,\dots,B_\ell$ returns $\rho$; $(I\otimes\Pi_\ell)\rho_{AB[\ell]}(I\otimes\Pi_\ell)=\rho_{AB[\ell]}$, where $\Pi_\ell=\frac1{\ell!}\sum_{\sigma\in\mathfrak S_\ell}P_\sigma$ projects onto the symmetric subspace of $\mathcal H_B^{\otimes\ell}$; and every partial transpose $\rho_{AB[\ell]}^{\mathsf T_{B[s]}}$ on $B_1,\dots,B_s$, $s=1,\dots,\ell$, is positive semidefinite.
• The EXT cone $\mathcal{EXT}_\ell$ is the same without the partial-transpose conditions.
• For a set $K$, the dual cone is $K^*=\{M\in\mathrm{Herm}(d_Ad_B):\mathrm{Tr}[M\rho]\ge0\ \forall\rho\in K\}$.
• To $M$ is attached the Hermitian polynomial $p_M(x,\bar x,y,\bar y)=\sum_{ijkl}M_{ij,kl}x_i\bar x_ky_j\bar y_l$.
• A real-valued polynomial in $(x,\bar x,y,\bar y)$ is rsos if it is a finite sum of squares of Hermitian polynomials, equivalently of real polynomials in the real and imaginary parts of $x,y$; it is csos if it is a finite sum $\sum_i|q_i(x,y)|^2$ with $q_i$ holomorphic polynomials.

Formalization targets

Goal: Theorem 12

$$\mathcal{SEP}^*=\{M: p_M\ge0\},\qquad \mathcal{DPS}_\ell^*=\{M:\|y\|^{2(\ell-1)}p_M\ \text{is rsos}\},\qquad \mathcal{EXT}_\ell^*=\{M:\|y\|^{2(\ell-1)}p_M\ \text{is csos}\},$$

for all $d_A,d_B$ and all $\ell\ge1$, with $M$ ranging over $\mathrm{Herm}(d_Ad_B)$.

Milestones

1. Theorem 12 (i), the first equality.
2. The identity (37): $(x\otimes\bar y^{\otimes s}\otimes y^{\otimes\ell-s})^\dagger W(\cdot)=(x\otimes y^{\otimes\ell})^\dagger W^{\mathsf T_{B[s]}}(x\otimes y^{\otimes\ell})$.
3. Lemma 19: $\|y\|^{2(\ell-1)}p_M$ is rsos iff it is $\sum_{s=0}^\ell(x\otimes\bar y^{\otimes s}\otimes y^{\otimes\ell-s})^\dagger W_s(x\otimes\bar y^{\otimes s}\otimes y^{\otimes\ell-s})$ with $W_s\succeq0$.
4. (39): $(x\otimes y^{\otimes\ell})^\dagger(Y-\Pi_\ell Y\Pi_\ell)(x\otimes y^{\otimes\ell})=0$.
5. The dual SDP description: $\mathcal{DPS}_\ell^*=\{M: M\otimes I_{B[2:\ell]}=(Y-\Pi_\ell Y\Pi_\ell)+\sum_{s=0}^\ell W_s^{\mathsf T_{B[s]}},\ Y\in\mathrm{Herm},\ W_s\succeq0\}$.
6. Lemma 20: $\|y\|^{2(\ell-1)}p_M$ is csos iff it is $(x\otimes y^{\otimes\ell})^\dagger W(x\otimes y^{\otimes\ell})$ with $W\succeq0$.
7. Theorem 15: there are absolute $C,C'>0$ with $h_{\mathrm{Sep}}(M)\le h_{\mathrm{DPS}_\ell}(M)\le(1+Cd_B^2/\ell^2)h_{\mathrm{Sep}}(M)$ for $\ell\ge C'd_B$, whenever $(x\otimes y)^\dagger M(x\otimes y)\ge0$.

Significance

Theorem 12 makes the DPS hierarchy and the sum-of-squares hierarchy for biquadratic forms interchangeable. A convergence bound for one is a convergence bound for the other: the paper uses this to derive the DPS rate (Theorem 15) from a rate for sums of squares on the sphere, and conversely quantum de Finetti arguments give sum-of-squares bounds. Part (iii) separates the two notions of Hermitian sum of squares: dropping the partial transposes corresponds exactly to passing from real to complex sums of squares. This explains, for example, why $(z+\bar z)^2$ (rsos but not csos) behaves differently in the two hierarchies.

The results are proved on paper; none is formalized. The mission produces a machine-checked statement and proof of the duality, together with the matrix-analytic infrastructure behind it: partial traces and partial transposes on $\mathcal H_A\otimes\mathcal H_B^{\otimes\ell}$, the symmetric projector, conic duality for semidefinite cones, and the passage between Gram matrices and sums of squares. Theorem 15 additionally depends on the sphere rate of the companion mission (Theorem 6 there) and on the unproved Lemma 13 and display (26) of the paper.

Difficulty

The inclusion of each sum-of-squares cone in the corresponding dual cone is a direct computation. The reverse inclusions are harder: a certificate involving arbitrary Hermitian polynomials must yield positive semidefinite matrices indexed by the prescribed tensor products, even though its square terms can mix different patterns of complex conjugation. Likewise, weak semidefinite duality alone does not show that every element of $\mathcal{DPS}_\ell^*$ has the displayed finite certificate; limits of certificates may require a separate closedness argument. The symmetric-subspace condition adds another constraint because an extension must be supported on that subspace, not merely invariant under permutations.

Formalization scope

• Indices: $\mathcal H_A\otimes\mathcal H_B$ is Fin dA × Fin dB (Mathlib's Kronecker convention); $\mathcal H_A\otimes\mathcal H_B^{\otimes\ell}$ is Fin dA × (Fin ℓ → Fin dB).
• The level is written $\ell=m+1$ with $m\in\mathbb N$, so $\ell\ge1$ is built in and $\|y\|^{2(\ell-1)}=\|y\|^{2m}$; $B_1,\dots,B_\ell$ are coordinates $0,\dots,m$.
• Matrices are complex; positive semidefiniteness is Mathlib's Matrix.PosSemidef (which includes Hermitian). Dual cones are subsets of $\mathrm{Herm}(d_Ad_B)$ with the pairing $\operatorname{Re}\mathrm{Tr}[M\rho]$.
• $p_M$ is (25) literally; "$p_M\ge0$" is $\operatorname{Re}p_M\ge0$.
• rsos is a finite sum of squares of real polynomials (MvPolynomial over $\mathbb R$) in the real and imaginary parts of $(x,y)$; csos is a finite sum of $|q_i|^2$ with $q_i$ complex polynomials in $(x,y)$ only. Swapping the two, or allowing complex $g_i$ in rsos, would change parts (ii) and (iii).
• Condition (21) is stated literally with the explicit projector; "commutes with all permutations" would be weaker and is not used.
• In Theorem 15, $h_{\mathrm{Sep}}$ and $h_{\mathrm{DPS}_\ell}$ are real suprema over trace-one elements, $d_A,d_B\ge1$ is assumed so the sets are nonempty, and $C,C'$ are quantified before all dimensions.

No trivializing reading is available: the cones are defined by their page conditions, the dual cones keep the Hermitian constraint, and no degree bound or extra hypothesis is placed on the sums of squares. Welcome contributions include a general library for partial traces and transposes of multipartite matrices, the spanning property of $\{y^{\otimes\ell}\}$ in the symmetric subspace, and Gram-matrix characterizations of sums of squares of polynomials; all are reusable well beyond this mission.

Selected references

• K. Fang, H. Fawzi, The sum-of-squares hierarchy on the sphere, and applications in quantum information theory, arXiv preprint, 2019. https://arxiv.org/abs/1908.05155v1
• A. C. Doherty, P. A. Parrilo, F. M. Spedalieri, Distinguishing separable and entangled states, Physical Review Letters 88, 187904, 2002. https://arxiv.org/abs/quant-ph/0112007
• A. C. Doherty, P. A. Parrilo, F. M. Spedalieri, Complete family of separability criteria, Physical Review A 69, 022308, 2004. https://arxiv.org/abs/quant-ph/0308032
• M. Navascués, M. Owari, M. B. Plenio, Power of symmetric extensions for entanglement detection, Physical Review A 80, 052306, 2009. https://arxiv.org/abs/0906.2731
• L. Gurvits, Classical deterministic complexity of Edmonds' problem and quantum entanglement, STOC 2003. https://doi.org/10.1145/780542.780545

Motivation

Textbook quantum theory starts from postulates about Hilbert spaces, density matrices and completely positive maps, none of which has an evident operational meaning. A long line of work, from Birkhoff–von Neumann quantum logic through Ludwig, Hardy (quant-ph/0101012), Dakić–Brukner and Masanes–Müller (arXiv:1004.1483), asks whether the formalism can instead be derived from principles that speak only about preparations, measurements and their statistics.

Chiribella, D'Ariano and Perinotti (Phys. Rev. A 84, 012311 (2011), arXiv:1011.6451) give such a derivation for finite-dimensional quantum theory. Five axioms (causality, perfect distinguishability, ideal compression, local distinguishability, pure conditioning) describe a broad class of information-processing theories containing classical theory; one further postulate, purification, singles out quantum theory. The paper builds on the framework of operational-probabilistic theories of the same authors (Phys. Rev. A 81, 062348 (2010)).

Setting

An operational-probabilistic theory (OPT) has systems $A,B,\dots$, a composite system $AB$ for every pair, and, for each pair $(A,B)$, tests: finite families $\{\mathcal C_i\}_{i\in X}$ of transformations from $A$ to $B$. Tests with no input are preparation tests (families of states $\rho_i$), tests with no output are observation tests (families of effects $a_j$). Composing a preparation test with an observation test yields a joint probability distribution $p(i,j)=(a_j|\rho_i)$, and parallel composition multiplies probabilities. After identifying objects with the same statistics, the states of $A$ span a real vector space $\mathrm{St}_{\mathbb R}(A)$ of finite dimension $D_A$, effects are linear functionals on it, and transformations are linear maps. $\mathrm{St}_1(A)$ denotes the normalized (deterministic) states.

Standard notions are then defined operationally: refinement and coarse-graining, pure states and atomic effects/transformations (only trivial refinements), completely mixed states (refined by every state), reversible transformations, the face $F_\rho$ of a state, and perfectly distinguishable families $\{\rho_i\}_{i=1}^N$ (there is an observation test with $(a_j|\rho_i)=\delta_{ij}$). The informational dimension $d_A$ is the common size of all maximal perfectly distinguishable families of pure states.

Formalization targets

Goal (Theorem 20)

For every theory satisfying the six principles and every system $A$, there is a real-linear isomorphism $S:\mathrm{St}_{\mathbb R}(A)\to\mathrm{Herm}_n(\mathbb C)$ with

$$S\big(\mathrm{St}_1(A)\big)=\{M\in M_n(\mathbb C):\ M\succeq 0,\ \operatorname{tr}M=1\},$$

and $n=d_A$, the size of every maximal family of perfectly distinguishable pure states. In words: the normalized states of every system are exactly the density matrices on $\mathbb C^{d_A}$.

Milestones

In the order of the paper: Theorem 6 (maximal distinguishable sets and completely mixed states), Lemma 16 (atomicity of composition), Theorem 8 (pure state / atomic effect duality), Lemma 32 (the informational dimension is well defined), Corollary 15 ($d_{AB}=d_Ad_B$), Theorem 9 with Lemma 10 (the invariant state is the uniform mixture of any maximal set), Theorem 10 (spectral decomposition), Theorem 12 ($D_A=d_A^2$), Theorem 13 (the Bloch ball and $G_A\cong SO(3)$ for $d_A=2$), Theorem 16 (superposition principle).

Significance

The result shows that, inside a class of theories defined by operational requirements, the density-matrix formalism is forced by purification. The intermediate results are of independent interest: an operational spectral theorem (Theorem 10), the dimension formula $D_A=d_A^2$ (Theorem 12) that replaces Hardy's "simplicity" axiom, and the derivation of the qubit Bloch ball (Theorem 13). Corollary 52 of the paper upgrades the goal to transformations (all completely positive trace-non-increasing maps), using a cited result of the 2010 framework paper; it is not part of this mission's goal.

The paper is a physics article with diagrammatic proofs and several steps delegated to the earlier framework paper. A formalization makes every framework assumption explicit and checks the derivation end to end; no machine-checked development of operational-probabilistic theories is known to the proposer.

Difficulty

The derivation never assumes a Hilbert space, so the matrix representation must be built from the principles: first qubits (via the Bloch ball classification, which uses the classification of compact subgroups of $O(3)$), then projections on faces, the superposition principle and finally a coordinate system on $d$-level systems in which positivity of all states can be checked. Each step relies on many operational lemmas (Choi isomorphism, teleportation, uniqueness of purification up to channels) that in the paper are proved diagrammatically or cited.

Formalization scope

Lean namespace InfoDerivQT. A theory is a structure OPT already in quotiented, finite-dimensional form: $\mathrm{St}_{\mathbb R}(A)$ is modelled as $\mathbb R^{D_A}$, effects as linear functionals, transformations as linear maps, and tests as families indexed by finite types. The framework records the circuit rules used throughout the paper: the probability rule, product rule, coarse-graining, identity, sequential composition with classical control, classical randomization, rescaled preparations, parallel composition of all kinds of tests, conditioning on one side of a bipartite state, swap and associator, closedness of the state set, and spanning of states and effects. Because transformations are identified with their action on single-system states, this encoding is faithful in the presence of local distinguishability (Eq. (5) of the paper), which every target assumes. The trivial system is not modelled. The six principles are bundled in OPT.SatisfiesPrinciples; quantum theory is a model, so the hypothesis is satisfiable. The choice of framework axioms is the main point for audit: a missing circuit rule could make a target false, an extra one could exclude intended theories.

Contributions welcome: proofs of the milestones, a formal check that finite-dimensional quantum theory is a model of SatisfiesPrinciples, and the Choi isomorphism and teleportation lemmas of Secs. IV and IX as further milestones.

Selected references

• G. Chiribella, G. M. D'Ariano, P. Perinotti, Informational derivation of quantum theory, Phys. Rev. A 84, 012311 (2011). https://doi.org/10.1103/PhysRevA.84.012311
• G. Chiribella, G. M. D'Ariano, P. Perinotti, Probabilistic theories with purification, Phys. Rev. A 81, 062348 (2010). https://doi.org/10.1103/PhysRevA.81.062348
• L. Hardy, Quantum theory from five reasonable axioms (2001). https://arxiv.org/abs/quant-ph/0101012
• Ll. Masanes, M. P. Müller, A derivation of quantum theory from physical requirements, New J. Phys. 13, 063001 (2011). https://arxiv.org/abs/1004.1483