Linear algebra

Motivation

Many quantum algorithms act on a matrix $A$ that is not itself unitary: a Hamiltonian to be simulated, a linear system to be inverted, a projector to be amplified. The standard way to hand such a matrix to a quantum computer is to embed it as a block of a unitary $U$, so that $A=\widetilde\Pi U\Pi$ for two orthogonal projectors $\Pi,\widetilde\Pi$. The question is then which functions $f(A)$ can be produced from a few uses of $U$ and $U^\dagger$.

Gilyén, Su, Low and Wiebe (arXiv:1806.01838, STOC 2019) answered it for polynomials: interleaving $U$ and $U^\dagger$ with phase rotations about $\Pi$ and $\widetilde\Pi$ applies a polynomial to every singular value of $A$. This quantum singular value transformation (QSVT) recovers Hamiltonian simulation, amplitude amplification, fixed-point search, quantum walks and matrix inversion as instances of one identity, and is now the common language of these algorithms (see the survey of Martyn, Rossi, Tan and Chuang, PRX Quantum 2021).

Timeline.

• 2016: Low, Yoder and Chuang characterize the single-qubit sequences $e^{i\varphi_0\sigma_z}\prod_j W(x)e^{i\varphi_j\sigma_z}$, which they call quantum signal processing (QSP) (PRX 2016).
• 2016–2017: Low and Chuang lift QSP to Hermitian blocks by qubitization (Quantum 2019; PRL 2017).
• 2018: this paper replaces eigenvalues by singular values, so that arbitrary (even rectangular) blocks are allowed, and removes the earlier constraint $P_\Re(0)=0$ for even degree.

Setting

Let $\mathcal H_U$ be a finite-dimensional complex Hilbert space, $U$ a unitary on it, and $\Pi,\widetilde\Pi$ orthogonal projectors. The projected unitary is $A=\widetilde\Pi U\Pi$. Put $d=\operatorname{rank}\Pi$, $\tilde d=\operatorname{rank}\widetilde\Pi$, $d_{\min}=\min(d,\tilde d)$. A singular value decomposition of $A$ consists of orthonormal bases $(\psi_i)_{i\le d}$ of $\mathrm{img}\,\Pi$ and $(\tilde\psi_i)_{i\le\tilde d}$ of $\mathrm{img}\,\widetilde\Pi$ and numbers $\varsigma_1\ge\dots\ge\varsigma_{d_{\min}}\ge0$ with

$$A=\sum_{i=1}^{d_{\min}}\varsigma_i\,|\tilde\psi_i\rangle\langle\psi_i| .$$

For $f:\mathbb R\to\mathbb C$, the singular value transformation is $f^{(SV)}(A)=\sum_{i\le d_{\min}}f(\varsigma_i)|\tilde\psi_i\rangle\langle\psi_i|$ when $f$ is odd and $f^{(SV)}(A)=\sum_{i\le d}f(\varsigma_i)|\psi_i\rangle\langle\psi_i|$ when $f$ is even, with $\varsigma_i:=0$ for $i>d_{\min}$.

The phase operator of a projector is $e^{i\varphi(2\Pi-I)}=e^{i\varphi}\Pi+e^{-i\varphi}(I-\Pi)$. For $\Phi=(\varphi_1,\dots,\varphi_n)\in\mathbb R^n$, the alternating phase modulation sequence $U_\Phi$ is the product, from $j=1$ on the left to $j=n$ on the right, of $e^{i\varphi_j(2\widetilde\Pi-I)}U$ when $n-j$ is even and of $e^{i\varphi_j(2\Pi-I)}U^\dagger$ when $n-j$ is odd. On the single-qubit side, $R(x)=\begin{pmatrix}x&\sqrt{1-x^2}\\ \sqrt{1-x^2}&-x\end{pmatrix}$ for $x\in[-1,1]$, and $\Phi$ is said to realize $P\in\mathbb C[x]$ if $P(x)$ is the top-left entry of $\prod_{j=1}^n e^{i\varphi_j\sigma_z}R(x)$ for every $x\in[-1,1]$.

In Lean these are ProjUnitarySVD U Proj Projt (the decomposition data), svtOdd/svtEven, phaseRefl, altPhaseSeq, reflR and qspRefl, in the namespace QSVT19.Main.

Formalization targets

Goal: Corollary 18 (singular value transformation by real polynomials)

Let $n\ge1$ and let $P_\Re\in\mathbb R[x]$ have degree $n$, parity $n \bmod 2$, and $|P_\Re(x)|\le1$ on $[-1,1]$. Then there is $\Phi\in\mathbb R^n$ such that for every singular value decomposition of $\widetilde\Pi U\Pi$

$$P_\Re^{(SV)}(\widetilde\Pi U\Pi)=\bigl(\langle+|\otimes\Pi'\bigr)\bigl(|0\rangle\langle0|\otimes U_\Phi+|1\rangle\langle1|\otimes U_{-\Phi}\bigr)\bigl(|+\rangle\otimes\Pi\bigr),$$

with $\Pi'=\widetilde\Pi$ for odd $n$ and $\Pi'=\Pi$ for even $n$. The only constraints on $P_\Re$ are those that are necessary; no degree-dependent constant appears.

Milestones

1. Lemma 6, Theorem 5, Theorem 4 (first claim): sum-of-squares factorization and the characterization of which polynomials, and which real parts, arise from QSP.
2. Corollary 8: every $P$ meeting four explicit conditions is realized by some $\Phi\in\mathbb R^d$ in the reflection form; Corollary 10: every $P_\Re$ as in the goal is $\Re[P]$ for such a $P$.
3. Definition 11 (existence of the decomposition), Table 2 (orthonormality of the spanning vectors of Definition 12), Lemma 14 (the block decomposition of $U$ into one- and two-dimensional pieces).
4. Theorem 17: if $\Phi$ realizes $P$, then $P^{(SV)}(\widetilde\Pi U\Pi)=\widetilde\Pi U_\Phi\Pi$ for odd $n$ and $\Pi U_\Phi\Pi$ for even $n$.
5. Lemma 9 (optional): explicit phases realizing the Chebyshev polynomial $T_d$.

Significance

The result. Corollary 18 says that every real polynomial of degree $n$, of definite parity and bounded by $1$ on $[-1,1]$, can be applied to the singular values of $\widetilde\Pi U\Pi$ with $n$ uses of $U$ and $U^\dagger$ and one ancilla qubit. Every application in §3.4–§5 of the paper (fixed-point amplitude amplification, singular vector transformation, the pseudoinverse, Hamiltonian simulation, Gibbs sampling) is this corollary applied to a suitable approximating polynomial, so a formal proof makes all of them conditional only on polynomial approximation bounds.

Formalizing it. The result is proved in the paper; none of the statements of this mission has a machine-checked proof on the platform. A formal development would provide reusable infrastructure absent from Mathlib: singular value decompositions over sub-spaces, the two-dimensional invariant-subspace decomposition of a projected unitary (a quantitative form of Jordan's lemma), and the polynomial characterization of single-qubit QSP. Theorem 3 of the paper, the $W(x)$ form of the QSP characterization, is already posed on the platform as QAlgorithms.Childs.qsp_characterization; Corollary 8 depends on it.

Difficulty

The obvious argument for Theorem 17 is "restrict $U_\Phi$ to each two-dimensional subspace and read off the QSP product". Making that rigorous means proving that the subspaces of Definition 12 are pairwise orthogonal, invariant under every factor of $U_\Phi$, and that $U$ acts on each pair of bases by exactly the reflection $R(\varsigma_i)$, including the degenerate blocks with $\varsigma_i\in\{0,1\}$, the one-dimensional blocks $\mathcal H_i^R,\mathcal H_i^L$ where $U_\Phi$ contributes a phase $e^{\pm i\varphi_0}$, and the complement $\mathcal H_\perp$. The polynomial side is harder still: Lemma 6 factors a nonnegative even polynomial through its multiset of complex roots, grouping roots in $(0,1)$, in $[1,\infty)$, on the imaginary axis and in the open quadrant, while tracking degree and parity. Neither step reduces to a library lemma, and an argument that works only for Hermitian $A$, or only when $\Pi=\widetilde\Pi$, proves a different theorem.

Formalization scope

• $\mathcal H_U$ is ι → ℂ for a Fintype ι with the inner product star v ⬝ᵥ w; operators are Matrix ι ι ℂ; "unitary" is U ∈ Matrix.unitaryGroup ι ℂ; "orthogonal projector" is IsStarProjection. The projectors are named Proj, Projt because Π is Lean notation. Indices are 0-based.
• A singular value decomposition is the structure ProjUnitarySVD U Proj Projt of data: orthonormal families with $\Pi=\sum_i|\psi_i\rangle\langle\psi_i|$, $\widetilde\Pi=\sum_i|\tilde\psi_i\rangle\langle\tilde\psi_i|$, nonnegative non-increasing $\varsigma$, and (17). The goal is posed for every such decomposition, with $\Phi$ chosen first; the Definition 11 milestone shows that one exists. $\varsigma_i\le1$ is a consequence and is not assumed.
• $f^{(SV)}$ is the sum over the decomposition (Definition 16), never the right-hand side of (32) or (33); a formalization that defines it by an operator expression trivializes the goal.
• $e^{i\varphi(2\Pi-I)}$ is written $e^{i\varphi}\Pi+e^{-i\varphi}(I-\Pi)$, equal to the matrix exponential for an idempotent $\Pi$. The ancilla of (33) is the first tensor factor.
• $e^{i\varphi\sigma_z}$ and the parity predicate are the published definitions of QAlgorithms_Defs_Hamiltonian. "deg ≤ k − 1" is degree < k and "parity $k-1$" is parity $k+1$, avoiding natural-number subtraction.
• Printed slips that affect statements:
  • Corollary 10 omits $\Re[P]=P_\Re$; it is restored, as used in the proof of Corollary 18.
  • Corollary 8 and Corollary 18 are false for degree $0$ (a constant $e^{i\alpha}$, respectively a constant $c\neq1$); both are posed with $d\ge1$, $n\ge1$.
  • Theorem 17's "$P$ and $\Phi$ as in Corollary 8" is read as (14), the only property its proof uses.
  • Lemma 14's (25)–(28) index the $\mathcal H^L$ blocks by $[d]\setminus[r]$; this is read as $[\tilde d]\setminus[r]$, as in (24).
• Contributions welcome: proofs of any milestone, general lemmas on SVDs of compressions $\widetilde\Pi U\Pi$, and a proof of the platform's open QSP characterization.

Selected references

• A. Gilyén, Y. Su, G. H. Low, N. Wiebe, Quantum singular value transformation and beyond: exponential improvements for quantum matrix arithmetics, arXiv:1806.01838v1, 2018; STOC 2019. https://arxiv.org/abs/1806.01838
• G. H. Low, T. J. Yoder, I. L. Chuang, Methodology of resonant equiangular composite quantum gates, Physical Review X 6, 041067, 2016. https://doi.org/10.1103/PhysRevX.6.041067
• G. H. Low, I. L. Chuang, Optimal Hamiltonian simulation by quantum signal processing, Physical Review Letters 118, 010501, 2017. https://doi.org/10.1103/PhysRevLett.118.010501
• G. H. Low, I. L. Chuang, Hamiltonian simulation by qubitization, Quantum 3, 163, 2019. https://doi.org/10.22331/q-2019-07-12-163
• J. M. Martyn, Z. M. Rossi, A. K. Tan, I. L. Chuang, Grand unification of quantum algorithms, PRX Quantum 2, 040203, 2021. https://doi.org/10.1103/PRXQuantum.2.040203

Motivation

Decoded quantum interferometry (DQI) is a quantum algorithm, introduced by Jordan, Shutty, Wootters, Zalcman, Schmidhuber, King, Isakov, Khattar and Babbush (arXiv:2408.08292), that turns an approximate optimization problem over a finite field into a decoding problem for a linear code. It applies to max-LINSAT: given linear constraints over $\mathbb F_p$, satisfy as many of them as possible. For structured instances such as optimal polynomial intersection the authors find DQI reaching approximation ratios that no known polynomial-time classical algorithm reaches, which makes it one of the few concrete candidates for a quantum advantage in optimization.

Whether DQI is useful on an instance depends on one number: the expected fraction of constraints satisfied by the string it outputs. Theorem 4.1 of the paper computes this number, in the limit of many constraints, for the best DQI state of a given degree. Every comparison of DQI with classical algorithms in the paper (simulated annealing, Prange's algorithm, the OPI and max-XORSAT benchmarks) is a comparison against this formula, and the follow-up analysis of imperfect decoders (Theorem 10.1) is a perturbation of it.

Setting

Fix a prime $p$. A max-LINSAT instance is a matrix $B\in\mathbb F_p^{m\times n}$ with rows $\mathbf b_1,\dots,\mathbf b_m$ and subsets $F_1,\dots,F_m\subseteq\mathbb F_p$; constraint $i$ asks that $\mathbf b_i\cdot\mathbf x\in F_i$ (Definition 2.1). Throughout, $m>n$ and every $F_i$ has the same size $r\in\{1,\dots,p-1\}$. Put $f_i(a)=+1$ if $a\in F_i$ and $-1$ otherwise, and

$$f(\mathbf x)=\sum_{i=1}^m f_i(\mathbf b_i\cdot\mathbf x),\qquad s(\mathbf x)=\#\{i:\mathbf b_i\cdot\mathbf x\in F_i\}.$$

For a real polynomial $P$ of degree at most $\ell$, the DQI state is $|P(f)\rangle=\sum_{\mathbf x\in\mathbb F_p^n}P(f(\mathbf x))|\mathbf x\rangle$, normalized so that $\sum_{\mathbf x}P(f(\mathbf x))^2=1$. Measuring it in the computational basis returns $\mathbf x$ with probability $P(f(\mathbf x))^2$, so the expected number of satisfied constraints is

$$\langle s\rangle=\sum_{\mathbf x}P(f(\mathbf x))^2\,s(\mathbf x),$$

and $\langle s^{(m,\ell)}\rangle_{\rm opt}$ is its supremum over all such $P$.

The dual code is $C^\perp=\{\mathbf d\in\mathbb F_p^m:B^T\mathbf d=0\}$ and $d^\perp$ is the least Hamming weight of a nonzero codeword. The condition $2\ell+1<d^\perp$ says that syndromes of errors of weight up to $\ell$ (and a little more) determine the error.

The analysis passes through rescaled constraint functions $g_i=(f_i-\bar f)/\varphi$ with Fourier transforms $\tilde g_i$, the elementary symmetric polynomials $P^{(k)}$ evaluated at the $g_i(\mathbf b_i\cdot\mathbf x)$, and the $(\ell+1)\times(\ell+1)$ symmetric tridiagonal matrix $A^{(m,\ell,d)}$ with diagonal $0,d,2d,\dots,\ell d$ and off-diagonal entries $a_k=\sqrt{k(m-k+1)}$, at $d=(p-2r)/\sqrt{r(p-r)}$.

Formalization targets

Goal: Theorem 4.1 (the semicircle law)

Fix $p$, $r$ and $\mu\ge0$. For any sequence of instances with $m\to\infty$, $\ell/m\to\mu$ and $2\ell+1<d^\perp$, writing $\rho=r/p$,

$$\lim\frac{\langle s^{(m,\ell)}\rangle_{\rm opt}}{m}=\begin{cases}\big(\sqrt{\mu(1-\rho)}+\sqrt{\rho(1-\mu)}\big)^2,&\rho\le1-\mu,\\ 1,&\text{otherwise.}\end{cases}$$

For $\rho=\tfrac12$ the curve is $\tfrac12+\sqrt{\mu(1-\mu)}$, a semicircle, which gives the theorem its name.

Milestones

1. The normalization of the rescaled $g_i$, (37)–(40).
2. Lemma A.1: under a common quadratic identity, $P(x_1+\dots+x_m)$ is a fixed linear combination of elementary symmetric polynomials.
3. The counting identity (68), $\sum_{|\mathbf y|=k}|\tilde g(\mathbf y)|^2=\binom mk$, and the Fourier picture (65) of the DQI state.
4. Lemma 9.1 (norm $=\|\mathbf w\|^2$ when $2\ell<d^\perp$) and Lemma 9.2 (the expected count is $\frac{mr}p+\frac{\sqrt{r(p-r)}}p\mathbf w^TA^{(m,\ell,d)}\mathbf w$ when $2\ell+1<d^\perp$).
5. The finite-size identity (131): $\langle s^{(m,\ell)}\rangle_{\rm opt}/m=\rho+\sqrt{\rho(1-\rho)}\,\lambda_{\max}^{(m,\ell,d)}/m$.
6. Lemma 9.3, $\lambda_{\max}^{(m,\ell,d)}/m\to\mu d+2\sqrt{\mu(1-\mu)}$, with its lower half (114) and the Gershgorin bound (129).
7. The algebra (132) and (136)–(137) that produce the closed form.

Significance

The result. Theorem 4.1 makes DQI's performance a closed-form function of two numbers, $r/p$ and $\ell/m$, and moves every question about an instance into coding theory: how large a $d^\perp$ the instance's dual code has, and whether it can be decoded efficiently up to $\ell$ errors. The OPI advantage claim of the paper, the comparison with Prange's algorithm on max-XORSAT, and the imperfect-decoding bound of Theorem 10.1 all start from this formula. The finite-size identity (131) is also useful on its own: it gives the exact optimum for any instance, not only in the limit.

Formalizing it. The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. A formalization would check the Fourier bookkeeping of §8.2.1 and §9 (normalizations $\sqrt{p^{n-k}\binom mk}$, character sums over $\mathbb F_p$), the claim that every degree-$\ell$ DQI state is a combination of the $|P^{(k)}\rangle$ and conversely, and the eigenvalue asymptotics of the tridiagonal matrix. Two points of the printed text need care and are stated correctly here: Lemma 9.2 writes its decomposition in the $f_i$ where the normalization requires the rescaled $g_i$, and the "otherwise $=1$" branch of Theorem 4.1 is argued only briefly on p. 34.

Difficulty

The algebraic steps are finite but long, and every one carries a normalization that a careless formalization gets wrong. The asymptotic step is the main obstacle. Lemma 9.3 needs a lower bound on $\lambda_{\max}$ from a test vector of growing width and a matching upper bound from Gershgorin's theorem, and the upper bound holds only under $d\ge-(m-2\ell)/\sqrt{\ell(m-\ell)}$, which is exactly the regime $\rho\le1-\mu$. In the other regime that hypothesis fails and the Gershgorin bound overshoots, so the limit $1$ needs a separate argument; the observation that $\langle s\rangle_{\rm opt}$ "increases in $r$", printed on p. 34, does not give it at fixed $p$ and $r$. A second difficulty is that $\langle s\rangle_{\rm opt}$ is a supremum over polynomials, while Lemma 9.2 is a statement about weight vectors $\mathbf w$; identifying the two needs both directions of Lemma A.1's correspondence and the normalization of Lemma 9.1.

Formalization scope

All objects live in the namespace DQI.Semicircle and one definitions file. $\mathbb F_p$ is ZMod p with [Fact p.Prime]; vectors are Fin n → ZMod p; constraints are indexed by Fin m from $0$. $\omega_p^a=\exp(2\pi i\,a/p)$ is computed from the representative of $a$ in $\{0,\dots,p-1\}$. Polynomials are real with natDegree ≤ ℓ; weight vectors are real. The optimum $\langle s\rangle_{\rm opt}$ is the real supremum over exactly the normalized polynomials of degree at most $\ell$ evaluated at $f(\mathbf x)$; its set is nonempty (constant polynomials) and bounded by $m$. The dual-distance condition is "every nonzero $\mathbf d$ with $B^T\mathbf d=0$ has weight $>t$"; $d^\perp$ is never an infimum, and $m>n$ (the paper's standing assumption) guarantees a nonzero codeword, so the condition forces $2\ell<m$. $\lambda_{\max}$ is the supremum of the real spectrum. The limit "$m\to\infty$ with $\ell/m$ fixed" is any sequence of instances with $m_j\to\infty$ and $\ell_j/m_j\to\mu$, with $p$ and $r$ fixed along it. Convergence of the ratio includes irrational $\mu$ with integer sizes.

Added hypotheses, all disclosed in the items: Lemma 9.2 decomposes in the $g_i$ rather than the printed $f_i$; (129) assumes $\ell\ge1$ to avoid dividing by $\sqrt0$; Lemma 9.3 imposes its hypothesis on $d$ only when $\ell_j\ge1$; (114) is stated as a $\liminf$ with an explicit $\varepsilon$.

A formalization that replaces $\langle s\rangle_{\rm opt}$ by a supremum over all states (which gives $1$), drops "nonzero" from the distance condition (which makes it unsatisfiable), or states the goal at a single $m$ is not this theorem and is ruled out by the definitions above.

Needed infrastructure: Fourier analysis on $\mathbb F_p^n$ (character orthogonality, Parseval), elementary symmetric polynomials and their reduction modulo a quadratic, Rayleigh quotients and Gershgorin discs for real symmetric matrices, and elementary limits. The tridiagonal-matrix bounds and the quadratic-reduction lemma are reusable beyond DQI. Proofs of any milestone, alternative arguments for the "otherwise" branch, and sharper finite-$m$ bounds on $\lambda_{\max}$ are welcome.

Selected references

• S. P. Jordan, N. Shutty, M. Wootters, A. Zalcman, A. Schmidhuber, R. King, S. V. Isakov, T. Khattar, R. Babbush, Optimization by Decoded Quantum Interferometry, arXiv:2408.08292v5, 2025. https://arxiv.org/abs/2408.08292
• S. Gershgorin, Über die Abgrenzung der Eigenwerte einer Matrix, Izv. Akad. Nauk SSSR, Ser. Fiz.-Mat. 6, 749–754, 1931.
• R. G. Gallager, Low-Density Parity-Check Codes, IRE Trans. Inform. Theory 8(1), 21–28, 1962. https://doi.org/10.1109/TIT.1962.1057683

Motivation

In a linear exchange market every agent owns one divisible good and has linear utilities over all goods; an equilibrium is a price vector at which every agent can spend its budget on goods that maximize utility per unit of money, and all goods are sold. Computing such an equilibrium in strongly polynomial time, with a number of arithmetic operations bounded by a polynomial in the number of agents alone, was an open question until Garg and Végh (arXiv:1809.06266; Operations Research, 2023). Their algorithm alternates two kinds of phases. One identifies "revealed" edges that appear in every equilibrium (the subject of mission I of this series). The other computes good starting prices for the current set of revealed edges by solving a linear program whose constraint matrix has a special sign structure.

No strongly polynomial algorithm is known for that linear program. Systems in which every inequality has at most one positive and at most one negative coefficient, by contrast, are strongly polynomially solvable (Megiddo, 1983; Hochbaum and Naor, 1994). The paper bridges the gap with Theorem 6.4: a polyhedron given by a $Z_+$-matrix is sandwiched between a monotone two-variable-per-inequality polyhedron and its scaling by an explicit factor $B^2$. This mission formalizes that theorem and the lemmas of §7 that prove it. It is a statement about matrices and polyhedra only; no market notions enter.

Setting

Matrices are rational. For integers $k, t \ge 0$ a matrix $M \in \mathbb{Q}^{k\times t}$ is a $Z_+$-matrix, written $M \in \mathcal{Z}_+(k,t)$, if every off-diagonal entry is nonpositive and every column sum is nonnegative:

$$M_{ij} \le 0 \quad (i \ne j), \qquad \sum_{i=1}^k M_{ij} \ge 0 \quad (j \in [t]).$$

For a non-square matrix the diagonal entries are the $M_{ii}$ with $1 \le i \le \min\{k,t\}$. Square $Z_+$-matrices are exactly the transposes of weighted Laplacians of directed graphs, or such transposes with one row and column deleted.

$\mathcal{M}_2(m,t)$ is the set of $m\times t$ rational matrices with at most one positive and at most one negative entry in every row. A system $\bar M x \le \bar b$ with $\bar M \in \mathcal{M}_2(m,t)$ is a monotone two-variable-per-inequality system (M2VPI).

For $M \in \mathcal{Z}_+(k,t)$ and $b \in \mathbb{Q}^k$ with $b > 0$, the polyhedron of interest is

$$P_M = \{x \in \mathbb{R}^t : Mx \le b,\ x \ge 0\}.$$

Write $\ell$ for the number of nonzero entries of $M$, $\alpha P = \{\alpha x : x \in P\}$ for $\alpha > 0$, and

$$B = \frac{\sum_{j=1}^k b_j}{\min_{i\in[k]} b_i}.$$

In §7 the right-hand side is called $\gamma$ instead of $b$, and $\lambda_i = \sum_{j\ne i}\gamma_j$.

The proof works with a square $M \in \mathcal{Z}_+(t,t)$ with positive diagonal. Its digraph $([t],H)$ has an arc $ij$ whenever $M_{ij} < 0$. $D_i$ is the set of vertices reachable from $i$ (including $i$), and $M^{(i)}$ is the submatrix of the rows $M_j$, $j \in D_i$. The vertices split into $T_1$ (at most one outgoing arc), $T_2$ (at least two arcs and $\operatorname{rk} M^{(i)} = |D_i|$) and $T_3$ (at least two arcs and $\operatorname{rk} M^{(i)} < |D_i|$).

Formalization targets

Goal: Theorem 6.4 (p. 15)

For $M \in \mathcal{Z}_+(k,t)$ with $k \ge 1$ and $\ell$ nonzero entries, and $b \in \mathbb{Q}^k$ with $b > 0$, there are $\ell' \le \ell$, $\bar M \in \mathcal{M}_2(\ell',t)$ and $\bar b \in \mathbb{Q}^{\ell'}$ with

$$P_M \subseteq \{x \in \mathbb{R}^t : \bar Mx \le \bar b,\ x \ge 0\} \subseteq B^2 P_M.$$

Milestones (§7, pp. 16–23)

• Lemma 7.1: for $M \in \mathcal{Z}_+(t,t)$ and $\bar p \ge 0$ with $M\bar p \le \gamma$, $\ M\bar p \ge -\lambda \ge -(B-1)\gamma$.
• Lemma 7.2: the Gaussian elimination of the proof, run on $T \in \mathcal{Z}_+(\ell,t)$, returns $T' = YT$ with $Y \ge 0$, $T'$ upper triangular with diagonal entries in $\{0,1\}$ and nonpositive off-diagonal entries, and $T'_{kk} = 1$ whenever some $T_{ik} < 0$ with $i > k$.
• Claim 7.3(iii): for $i \in T_3$, $M_i$ is a linear combination of $\{M_h : h \in D_i \setminus\{i\}\}$.
• Lemma 7.4(i): for $i \in T_2\cup T_3$ there is a unique $q^{(i)} \in \mathbb{R}^t_+$ with $M_\ell q^{(i)} = 0$ ($\ell \in D_i\setminus\{i\}$), $q^{(i)}_i = 1$ and $q^{(i)}_\ell = 0$ off $D_i$.
• Lemma 7.4(iv) and (iii): points $r^{(i)} \in P_M$ tight on $D_i\setminus\{i\}$ (for $i \in T_3$) and on $D_i$ with $r^{(i)}_i = \kappa(i)$ (for $i \in T_2$).
• Claim 7.5: $\kappa(i)\,M_i q^{(i)} \le B\gamma_i$ for $i \in T_2$.
• The reduced case (§7, p. 16): Theorem 6.4 for square $M$ with positive diagonal.

Significance

Theorem 6.4 turns an LP over a $Z_+$ constraint matrix, for which no strongly polynomial algorithm is known, into an M2VPI system that is strongly polynomially solvable, at the price of a factor $B^2$. In the exchange-market algorithm $B \le n$, so the starting prices of each phase come within a factor $n^2$ of optimal (the proof of Theorem 3.7, p. 15). That bound is what lets the potential argument advance in a polynomial number of phases. The construction is not specific to markets: any LP of the form $\max \sum_i x_i$ over $P_M$ with $M$ a $Z_+$-matrix, which includes LPs over transposed weighted Laplacians of directed graphs, inherits the same approximation.

The result is proved in the paper; to our knowledge none of it has been machine-checked. A formalization produces a checked proof of the sandwich. It also produces reusable facts about Gaussian elimination on $Z_+$-matrices (Lemma 7.2), which hold for any matrix whose off-diagonal entries are nonpositive and whose column sums are nonnegative.

Difficulty

The obvious approach, deleting all but two variables from each inequality of $P_M$, fails: the dropped negative terms make the resulting system either too weak or invalid. The paper instead derives one new constraint per arc $ij$ of $H$, as a nonnegative combination of the inequalities $M\bar p \ge -\lambda$. Finding it requires an ordering of $D_i$ in which every vertex but $i$ has an in-neighbour placed after it, and an elimination on the permuted submatrix whose penultimate row has exactly two nonzero entries. The reverse containment $\{\bar M\bar p \le \bar b\} \subseteq B^2P_M$ is the hard direction. It splits by whether the rows on $D_i$ are linearly independent ($T_2$) or not ($T_3$), and the $T_2$ case needs the extra constraint $\bar p_i \le \kappa(i)$ and the comparison of entries of the elimination multipliers $Y^{(ij)}$ in Claim 7.5. Every step relies on a sign invariant of the elimination that Lemma 7.2 proves by induction.

Formalization scope

Indices are 0-based (Fin k, Fin t); the paper's $[n] = \{1,\dots,n\}$. Matrices $M$, $\bar M$ and right-hand sides $b$, $\bar b$, $\gamma$ are rational (ℚ), as on p. 15, and act on real vectors $x \in \mathbb{R}^t$ through the cast. A diagonal entry of a rectangular matrix is one whose two indices agree as natural numbers. $B^2P_M$ is the image $\{B^2x : x \in P_M\}$. $B$ is defined for $k \ge 1$ only, and every statement using it assumes $k \ge 1$ (resp. $t \ge 1$).

Not formalized: the running time $O(\ell(\min\{k,t\})^3)$ and the polynomial bound on the encoding size of $\bar M$, $\bar b$ in Theorem 6.4. The goal is the existence statement that the construction (13) witnesses. The standing assumptions of §7 ($\gamma > 0$; positive diagonal after the reduction) appear as hypotheses of the milestones that live in that setting.

Lemma 7.2 is stated about the specific elimination of the proof (p. 17), defined explicitly; an existential "there is $Y \ge 0$" form would be nearly trivial, since $Y = 0$ satisfies all but one clause. In the goal, $\bar M$ must have at most one positive and at most one negative entry per row, and $\ell' \le \ell$. Dropping either requirement makes the goal weaker than the paper's theorem.

$\kappa(i)$, defined in (12) through the elimination for an arbitrarily chosen arc, is restated intrinsically as the $i$-th entry of $(M_{D_i,D_i})^{-1}\gamma_{D_i}$, a number the paper shows equal (proof of Lemma 7.4(iii)). It is used only for $i \in T_2$, where that block is invertible. Claim 7.3(i)–(ii) and Lemma 7.4(ii), which concern the elimination output for a particular arc, are not milestones.

A complete development needs the elimination and its invariants, reachability in a finite digraph, ranks of row submatrices, and the construction (13). The elimination lemmas are reusable for any $Z_+$-matrix. Contributions are welcome on any milestone, on the reduction from rectangular $M$ to the square positive-diagonal case, and on the two containments of the reduced case.

Selected references

• J. Garg and L. A. Végh, A strongly polynomial algorithm for linear exchange markets, arXiv:1809.06266v3, 2022; Operations Research, 2023. https://arxiv.org/abs/1809.06266
• N. Megiddo, Towards a genuinely polynomial algorithm for linear programming, SIAM Journal on Computing 12(2), 1983. https://doi.org/10.1137/0212022
• D. S. Hochbaum and J. Naor, Simple and fast algorithms for linear and integer programs with two variables per inequality, SIAM Journal on Computing 23(6), 1994. https://doi.org/10.1137/S0097539793251876
• R. W. Cottle and A. F. Veinott, Jr., Polyhedral sets having a least element, Mathematical Programming 3, 1972. https://doi.org/10.1007/BF01584975

Motivation

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

Timeline.

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

Setting

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 3 (p. 7)

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

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

Milestones

The milestones follow the paper's proof:

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

Timeline.

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1 (p. 3)

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

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

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

General results

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Theorem 1 has two disclosed differences from the page:

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

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

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

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

Selected references

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

Motivation

Determining an unknown quantum state of $n$ qubits to good accuracy requires, in general, a number of copies of the state exponential in $n$; this follows from Holevo's theorem. One way around this barrier is to restrict the class of states. Stabilizer states are the natural candidate: they are the states produced from $|0^n\rangle$ by Clifford circuits, they underlie quantum error-correcting codes, measurement-based computation and randomized benchmarking, and there are $2^{\Theta(n^2)}$ of them, so $\Omega(n)$ copies are necessary to identify one.

Timeline.

• Aaronson and Gottesman (2008, Identifying stabilizer states, talk, http://pirsa.org/08080052/) described a procedure identifying an unknown stabilizer state from $O(n^2)$ copies with single-copy measurements, and a variant using $O(n)$ copies with measurements collective across all copies.
• Low (2009, arXiv:0907.2833) showed that a Clifford unitary can be identified from $O(n^2)$ uses, or $O(n)$ with access to its inverse.
• Rocchetto (2017, arXiv:1705.00345) showed that stabilizer states are PAC-learnable efficiently.
• Montanaro (2017, arXiv:1707.04012) gave the algorithm of this mission: $O(n)$ copies, collective measurements on at most two copies at a time, failure probability exponentially small in $n$. Zhao, Pérez-Delgado and Fitzsimons obtained a related $O(n)$-copy algorithm for graph states independently (arXiv:1510.03742).

Bell sampling became a standard tool after this paper, for instance in stabilizer testing (Gross, Nezami and Walter, arXiv:1712.08628), so a machine-checked version of its analysis is a reusable base.

Setting

A state of $n$ qubits is a vector $\psi:\{0,1\}^n\to\mathbb C$; its complex conjugate $\psi^*$ is taken entrywise in the computational basis. The paper uses the four $2\times2$ matrices

$$\sigma_{00}=\begin{pmatrix}1&0\\0&1\end{pmatrix},\ \sigma_{01}=\begin{pmatrix}0&1\\1&0\end{pmatrix},\ \sigma_{10}=\begin{pmatrix}1&0\\0&-1\end{pmatrix},\ \sigma_{11}=\sigma_{10}\sigma_{01}=\begin{pmatrix}0&1\\-1&0\end{pmatrix},$$

which are the Pauli matrices up to the factor $-i$ on $\sigma_{11}$. For a string $s\in\{0,1\}^{2n}$, $\sigma_s=\sigma_{s_1s_2}\otimes\cdots\otimes\sigma_{s_{2n-1}s_{2n}}$; strings are added bitwise, $s\oplus t$.

The Bell basis of $\mathbb C^4$ is $|\sigma_{00}\rangle=\frac1{\sqrt2}(|00\rangle+|11\rangle)$, $|\sigma_{01}\rangle=\frac1{\sqrt2}(|01\rangle+|10\rangle)$, $|\sigma_{10}\rangle=\frac1{\sqrt2}(|00\rangle-|11\rangle)$, $|\sigma_{11}\rangle=\frac1{\sqrt2}(|01\rangle-|10\rangle)$. Bell sampling on $2n$ qubits $A_1,\dots,A_n,B_1,\dots,B_n$ measures each pair $A_iB_i$ in the Bell basis and returns a string $r\in\{0,1\}^{2n}$. On two copies $|\psi\rangle|\psi\rangle$ (first copy on the $A$'s) the outcome $r$ has probability $p_\psi(r)=|\langle\sigma_r|\,\psi\otimes\psi\rangle|^2$.

A stabilizer state is $\psi=U|0^n\rangle$ for a Clifford unitary $U$ (a unitary normalising the Pauli group). Its stabilizer set $T(\psi)\subseteq\mathbb F_2^{2n}$ is the set of strings $t$ for which $\psi$ is an eigenvector of $\sigma_t$, i.e. those $\sigma_t$ that lie in the stabilizer group of $\psi$ up to a phase.

Algorithm 1. Bell-sample two fresh copies to get $r_0$; repeat $2n$ times to get $r_1,\dots,r_{2n}$; find a basis $B$ of $\operatorname{span}\{r_i\oplus r_0\}$; for each element of $B$ measure one copy of $\psi$ in the eigenbasis of the corresponding (Hermitian) Pauli matrix $M$ to learn whether $M|\psi\rangle=+|\psi\rangle$ or $-|\psi\rangle$. It uses $5n+2$ copies.

Formalization targets

Goal: Theorem 1, explicit form

For every $n$ and every $n$-qubit stabilizer state $\psi$, with the $2n+1$ Bell samples independent,

$$\Pr\bigl[\operatorname{span}\{r_i\oplus r_0:1\le i\le 2n\}=T(\psi)\bigr]\ \ge\ 1-2^{-n},$$

and for every basis $b_1,\dots,b_n$ of $T(\psi)$ with Hermitian Paulis $M_j$, each $M_j\psi=\pm\psi$ and every vector with the same eigenvalues under all $M_j$ is a scalar multiple of $\psi$. Together: Algorithm 1 identifies $\psi$ except with probability at most $2^{-n}$.

Milestones

1. $\sigma_s\sigma_t=\pm\sigma_{s\oplus t}$.
2. Lemma 2: $p_\psi(r)=|\langle\psi|\sigma_r|\psi^*\rangle|^2/2^n$.
3. The Bell-sampling probabilities of a unit vector sum to $1$.
4. For a stabilizer state, $|\psi^*\rangle=c\,\sigma_{10}^{\otimes S}|\psi\rangle$ with $|c|=1$.
5. Eqn (1): $p_\psi(r)=|\langle\psi|\sigma_r\sigma_{10}^{\otimes S}|\psi\rangle|^2/2^n$.
6. $T(\psi)$ is an $n$-dimensional subspace of $\mathbb F_2^{2n}$.
7. $\langle\psi|\sigma_t|\psi\rangle=0$ for $t\notin T(\psi)$.
8. $p_\psi$ is uniform on a coset $\{t\oplus s:t\in T\}$.
9. For two independent outcomes, $r_1\oplus r_2$ is uniform on $T$.
10. $T$ and the signs on a basis of $T$ determine $\psi$ up to a scalar.
11. $2n$ uniform samples of an $n$-dimensional $\mathbb F_2$-space fail to span it with probability at most $2^{-n}$.

Significance

The theorem gives a learning algorithm whose copy complexity $O(n)$ is optimal and whose measurements are simple: one Bell measurement on corresponding qubits of two copies. Its analysis isolates a structural fact about stabilizer states, that Bell sampling on two copies produces a uniformly random element of a coset of the stabilizer subspace, which is the engine of later work on stabilizer testing and on learning states with few non-Clifford gates.

The result is proved in the paper; no machine-checked proof of it is known. A complete formalization adds: the stabilizer formalism in a form usable from the definition "$U|0^n\rangle$ for a Clifford $U$" (the subspace $T$, its dimension, vanishing expectations off $T$, determination by signs); the conjugation identity, which the paper takes from a normal form cited from the literature; and the probabilistic bookkeeping of the algorithm with its exact constants.

Difficulty

The probability calculations (Lemma 2, eqn (1), the union bound) are finite sums. The difficulty lies in the stabilizer structure. The platform's definition of a stabilizer state is the image of $|0^n\rangle$ under a Clifford unitary; from it one must derive that the strings whose $\sigma_t$ fixes $\psi$ up to phase form an $n$-dimensional subspace, that all other Pauli expectations vanish, and that $\psi^*$ differs from $\psi$ by a diagonal Pauli. The paper obtains the last fact from the Dehaene–De Moor normal form $\psi\propto\sum_{x\in A}i^{\ell(x)}(-1)^{q(x)}|x\rangle$, a cited theorem whose proof is not on the page; formalizing either that normal form or a direct substitute is the central step. The natural shortcut, treating $T$ as given with "uniform outcomes on $T$" as a hypothesis, proves only the counting lemma and is ruled out below.

Formalization scope

• States are StabilizerRank.QState n = (Fin n → Bool) → ℂ and stabilizer states are StabilizerRank.IsStabilizerState (published platform definition, referenced). Qubit $i$ is coordinate $i$, false $=0$.
• Strings $\{0,1\}^{2n}$ are encoded as Fin n → ZMod 2 × ZMod 2, coordinate $i$ the pair $(s_{2i-1},s_{2i})$ of qubit $i$; $\oplus$ is +.
• $\sigma_{11}$ is the page's $\begin{pmatrix}0&1\\-1&0\end{pmatrix}$, not the Pauli $Y$. The "corresponding Pauli matrix" of step 5 is the Hermitian $(-i)^{\#\{i:t_i=11\}}\sigma_t$; the page does not fix this phase.
• The Bell outcome law is the Born rule with $\psi(x)\psi(y)$ the amplitude of $|\psi\rangle|\psi\rangle$ at $|x\rangle_A|y\rangle_B$.
• Algorithm 1 is modelled by its outcome law: the $2n+1$ samples are independent (fresh copies), and an event has probability $\sum \mathbf 1_E\,p_\psi(r_0)\prod_i p_\psi(r_i)$. Step 5 is deterministic once a basis of $T$ is known, and is stated as a property of every such basis.
• The explicit constants of p. 2 replace "$O(n)$" and "exponentially small": $2n+1$ Bell samples, success probability at least $1-2^{-n}$ (the page's "fails with probability at most $2^{-n}$", in a form that a mis-normalised outcome law cannot satisfy). The count $5n+2$ and "at most two copies at a time" are properties of the model, not separate clauses. The running time $O(n^3)$ is not formalized.
• Lemma 2 is stated for every vector, not only unit vectors (the identity is homogeneous). The conjugation identity carries a unit phase $c$, which the page omits. "$\langle\psi|M|\psi\rangle=0$ for $M\notin G$" is stated for strings outside $T$.
• Ruled out: $T$ as a hypothesis (it is always computed from $\psi$), dropping the reference sample $r_0$ or the independence of the samples, a degenerate outcome law, and reading "identifies" as "the samples span $T$" without the sign step.

Needed infrastructure: Kronecker-product manipulations of $\sigma_s$ indexed by bit strings, the Bell basis as an orthonormal basis of $(\mathbb C^2\otimes\mathbb C^2)^{\otimes n}$, the stabilizer formalism over $\mathbb F_2^{2n}$, and counting hyperplanes of finite $\mathbb F_2$-spaces. The stabilizer-formalism layer and the union bound are reusable beyond this mission. Contributions to any milestone are welcome, in particular direct proofs of milestones 4, 6 and 7 from the Clifford definition.

Selected references

• A. S. Holevo, Bounds for the quantity of information transmitted by a quantum communication channel, Problems of Information Transmission 9:177–183, 1973.
• D. Gross, S. Nezami and M. Walter, Schur–Weyl duality for the Clifford group with applications: property testing, a robust Hudson theorem, and de Finetti representations, Comm. Math. Phys. 385:1325–1393, 2021. https://arxiv.org/abs/1712.08628
• A. Montanaro, Learning stabilizer states by Bell sampling, arXiv preprint, 2017. https://arxiv.org/abs/1707.04012
• S. Aaronson and D. Gottesman, Identifying stabilizer states, PIRSA talk, 2008. http://pirsa.org/08080052/
• R. Low, Learning and testing algorithms for the Clifford group, Phys. Rev. A 80:052314, 2009. https://arxiv.org/abs/0907.2833
• A. Rocchetto, Stabiliser states are efficiently PAC-learnable, arXiv preprint, 2017. https://arxiv.org/abs/1705.00345
• L. Zhao, C. Pérez-Delgado and J. Fitzsimons, Fast graph operations in quantum computation, Phys. Rev. A 93:032314, 2016. https://arxiv.org/abs/1510.03742
• J. Dehaene and B. De Moor, Clifford group, stabilizer states, and linear and quadratic operations over GF(2), Phys. Rev. A 68:042318, 2003. https://arxiv.org/abs/quant-ph/0304125
• M. Van den Nest, Classical simulation of quantum computation, the Gottesman–Knill theorem, and slightly beyond, Quantum Inf. Comput. 10:258, 2010. https://arxiv.org/abs/0811.0898
• S. Aaronson, The learnability of quantum states, Proc. R. Soc. A 463:3089, 2007. https://arxiv.org/abs/quant-ph/0608142