Quantum Information

Motivation

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

Let $k \ge 0$ be the number of gates of a quantum circuit and let $s \in [0,1]$. In the adiabatic simulation of the circuit, the interpolated Hamiltonian $H(s) = (1-s)H_B + sH_C$ leaves invariant the $(k+1)$-dimensional computational subspace spanned by the history states $|\psi_0\rangle, \dots, |\psi_k\rangle$, and on it acts, by $\langle\psi_j|H_B|\psi_{j'}\rangle = -\delta_{j,j'}\delta_{j,0}$ and $\langle\psi_j|H_C|\psi_{j'}\rangle = -(\delta_{j,j'+1}+\delta_{j,j'-1})$, as the real symmetric $(k+1)\times(k+1)$ matrix

$$A_k(s) = \begin{pmatrix} s-1 & -s & 0 & \cdots & 0 \\ -s & 0 & -s & \ddots & \vdots \\ 0 & -s & 0 & \ddots & 0 \\ \vdots & \ddots & \ddots & \ddots & -s \\ 0 & \cdots & 0 & -s & 0 \end{pmatrix},$$

whose $(0,0)$ entry is $s-1$, whose first off-diagonal entries are $-s$, and whose other entries vanish. Let $\lambda_0(s) \le \lambda_1(s) \le \cdots \le \lambda_k(s)$ be its eigenvalues, counted with multiplicity, and $\Delta_k(s) = \lambda_1(s) - \lambda_0(s)$ the gap between the smallest and the second smallest.

Lemma. The gap is $\Omega(1/k^2)$ uniformly in $s \in [0,1]$: there are a constant $c > 0$ and a threshold $k_0$ such that

$$\Delta_k(s) \ge \frac{c}{k^2} \qquad \text{for all } k \ge k_0 \text{ and all } s \in [0,1].$$

This bound on the minimum gap along the whole interpolation path is what makes an adiabatic evolution time $T = \mathrm{poly}(k)$ sufficient, and hence shows that adiabatic quantum computation can efficiently simulate the circuit model.

Formalization Note The matrix is the shared definition clockPathMatrix k s on $\mathrm{Fin}(k+1)$; the gap is spectralGap, the second smallest minus the smallest eigenvalue of the Hermitian matrix with multiplicity (so a degenerate ground level would give gap $0$). The constants $c$ and $k_0$ are quantified before $k$ and $s$.

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

• Lemma 33.1: Ω(1/k²) spectral gap of the adiabatic clock Hamiltonian on the computational subspace.

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 29 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

For $x\in[-1,1]$ let

$$W(x)=\begin{pmatrix} x & i\sqrt{1-x^2}\\ i\sqrt{1-x^2} & x\end{pmatrix}=e^{i\arccos(x)\sigma_x},$$

and for $\phi\in\mathbb R$ let $e^{i\phi\sigma_z}=\mathrm{diag}(e^{i\phi},e^{-i\phi})$. For $k\ge 0$ and a phase vector $\Phi=(\phi_0,\dots,\phi_k)\in\mathbb R^{k+1}$, the quantum signal processing sequence is

$$W_\Phi(x)=e^{i\phi_0\sigma_z}\,W(x)\,e^{i\phi_1\sigma_z}\,W(x)\cdots W(x)\,e^{i\phi_k\sigma_z},$$

with $k$ factors $W(x)$. For a polynomial $P\in\mathbb C[x]$ write $P^*$ for the polynomial with complex-conjugated coefficients (so $P^*(x)=\overline{P(x)}$ for real $x$).

Lemma. Let $k\ge0$ and $P,Q\in\mathbb C[x]$. There exists $\Phi\in\mathbb R^{k+1}$ such that for every $x\in[-1,1]$

$$W_\Phi(x)=\begin{pmatrix} P(x) & iQ(x)\sqrt{1-x^2}\\ iQ^*(x)\sqrt{1-x^2} & P^*(x)\end{pmatrix}$$

if and only if

1. $\deg P\le k$ and $\deg Q\le k-1$ (with $\deg 0=-\infty$; in particular $Q=0$ when $k=0$);
2. $P$ has parity $k \bmod 2$ and $Q$ has parity $k-1 \bmod 2$, where an even polynomial has parity $0$ and an odd one parity $1$, i.e. $P(-x)=(-1)^kP(x)$ and $Q(-x)=(-1)^{k-1}Q(x)$;
3. $|P(x)|^2+(1-x^2)|Q(x)|^2=1$ for all $x\in[-1,1]$.

This characterization is the core of quantum signal processing: it says exactly which polynomial transformations of a signal $x$ can be implemented by interleaving the signal rotation $W(x)$ with $z$-rotations, and it is later lifted, via qubitization, to polynomial transformations of block-encoded operators.

Formalization Note The matrix identity is required for all $x\in[-1,1]$, the domain on which $W(x)$ is defined in (29.6). The degree condition uses Mathlib's degree with values in $\mathbb N\cup\{-\infty\}$, so $\deg Q\le k-1$ is written $\deg Q<k$; the parity $k-1 \bmod 2$ of $Q$ is written as parity $k+1$, which is the same residue and avoids natural-number subtraction. Parity is the polynomial identity $P(-x)=(-1)^kP(x)$.

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

• Lemma 29.1: Quantum signal processing: which polynomial pairs a QSP sequence realizes.

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 3 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 analysis of Simon's algorithm.

Let $N=2^n$ and identify $\{0,\dots,N-1\}$ with $\{0,1\}^n$; write $i\oplus s$ for bitwise addition modulo $2$ and $s\cdot j=\sum_k s_kj_k \bmod 2$. An input is $x=(x_i)_{i\in\{0,1\}^n}$ with $x_i\in\{0,1\}^n$, and Simon's promise says there is a nonzero $s\in\{0,1\}^n$ with $x_i=x_j \iff (i=j \text{ or } i=j\oplus s)$. A query is the unitary $O_x:|i,y\rangle\mapsto|i,y\oplus x_i\rangle$. One run of the subroutine prepares

$$|\Psi_x\rangle=(H^{\otimes n}\otimes I)\,O_x\,(H^{\otimes n}\otimes I)\,|0^n\rangle|0^n\rangle$$

(one query, $2n$ Hadamard gates) and measures the first register. Then:

1. For every $n$, every $x$ and nonzero $s$ satisfying the promise, and every $j$, the outcome $j$ has probability $2^{-(n-1)}$ if $s\cdot j=0$ and $0$ otherwise; i.e. it is uniform on $\{j: s\cdot j=0\}$.
2. There are constants $C>0$ and $N_0$ (independent of $n$, $x$, $s$) such that for all $n\ge N_0$: if the subroutine is repeated independently until the outcomes obtained so far span a subspace of $\mathbb F_2^n$ of dimension $n-1$, the expected number of runs, which equals the expected number of $x_i$-queries, is at most $C\,n$.
3. If outcomes $j_1,\dots,j_m$ are all orthogonal to $s$ and span a subspace of dimension at least $n-1$, then the only nonzero solution $y$ of the system $j_k\cdot y=0$ $(k=1,\dots,m)$ is $y=s$.
4. There are constants $C>0$ and $N_0$ such that for every $n\ge N_0$ there is a classical Boolean circuit (AND, OR, NOT gates of fan-in at most $2$) of size at most $C n^3$ which, given any $n-1$ linearly independent strings $j_1,\dots,j_{n-1}$ orthogonal to a nonzero $s$, outputs $s$.

Together these say that Simon's algorithm finds $s$ with an expected $O(n)$ queries and polynomially many other operations, an exponential speed-up over classical randomized algorithms.

Formalization Note Item 2 uses the expected stopping time of an i.i.d. sequence drawn from the PMF whose masses are the first-register marginals of $|\Psi_x\rangle$; its existence is part of the conclusion. The intermediate measurement of the second register is omitted, as the source allows. The constant $N_0$ in item 4 also absorbs $n=1$, where a circuit with no input wires cannot output the constant $1$. The $n-1$ input strings are fed to the circuit row-major through $\mathrm{finProdFinEquiv}$.

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

• §3.2: Simon's algorithm: uniform orthogonal samples, expected O(n) queries, O(n^3) classical post-processing.
• §3.3.2: Classical randomized lower bound Ω(√(2^n)) for decision Simon.

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 22 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 Kutin's symmetrization lemma for the collision problem.

Fix $n \ge 0$ and consider strings $x \in [n]^n$, $[n] = \{1,\dots,n\}$, encoded by the indicator variables $\delta_{ij} = 1$ if $x_i = j$ and $0$ otherwise ($i, j \in [n]$). A triple $(m,a,b)$ of natural numbers is valid if $m \in \{0,\dots,n\}$, $a, b \ge 1$, $a \mid m$ and $b \mid n-m$. For a valid triple define the string

$$x^{m,a,b}_i = \begin{cases} \lceil i/a \rceil & 1 \le i \le m,\\ n - \lfloor (n-i)/b \rfloor & m < i \le n, \end{cases}$$

which is $a$-to-one on its first $m$ positions and $b$-to-one on the rest. For permutations $\sigma, \tau$ of $[n]$ let $x^{\sigma\tau}_i = \tau(x^{m,a,b}_{\sigma(i)})$ and let $\delta^{\sigma\tau}_{ij}$ be its indicator variables.

Let $p$ be any real polynomial in the $n^2$ variables $\delta_{ij}$, and for a valid triple set

$$P(m,a,b) = \mathbb{E}_{\sigma,\tau}\bigl[p(\{\delta^{\sigma\tau}_{ij}\})\bigr] = \frac{1}{(n!)^2} \sum_{\sigma,\tau \in S_n} p(\{\delta^{\sigma\tau}_{ij}\}).$$

Then there is a real polynomial $Q(m,a,b)$ in three variables with $\deg Q \le \deg p$ (total degrees) such that

$$Q(m,a,b) = P(m,a,b) \quad \text{for every valid triple } (m,a,b).$$

Applied to the acceptance probability of a $t$-query algorithm (a polynomial of degree at most $2t$ in the $\delta_{ij}$), this reduces the collision lower bound to degree bounds for a polynomial in three integer variables, to which Paturi's lemma is applied.

Formalization Note Indices and values are 0-based in Lean (Fin n); the defining formulas of $x^{m,a,b}$ are kept in 1-based form and the value is shifted by one. The polynomial $p$ is an arbitrary MvPolynomial (Fin n × Fin n) ℝ, not necessarily multilinear, and degrees are total degrees.

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

• Lemma 22.1: Kutin's lemma: the permutation-averaged polynomial is a polynomial in (m, a, b).

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

The AdS/CFT correspondence relates a theory of quantum gravity in anti-de Sitter space (the bulk) to a quantum field theory without gravity on its boundary (the CFT). A central question is how a local field operator $\phi(x)$ deep in the bulk is represented by boundary operators. Almheiri, Dong and Harlow (JHEP 04 (2015) 163) pointed out a puzzle.

• The bulk operator can be reconstructed on several different boundary regions. For example, it can be reconstructed on $A\cup B$, on $B\cup C$ or on $A\cup C$, but not on any single one of them.
• These reconstructions cannot all be the same CFT operator: an operator commuting with all local operators on a time slice must be trivial.

Their resolution is that the bulk effective theory is a quantum error-correcting code. Bulk operators are logical operators acting on a code subspace of the CFT Hilbert space. Different boundary representations agree only on that subspace, as one logical operator of an erasure-correcting code can be implemented on different subsets of qubits.

The mathematical backbone of that resolution is a finite-dimensional criterion for when a logical operator can be implemented on a given subsystem. This mission formalizes it (Appendix B of the paper), with the examples and corollaries of Section 3.

Timeline.

• 1996–1997: Schumacher and Nielsen characterize correctability by vanishing correlations with a reference system, condition (3.14) (arXiv:quant-ph/9604022). Grassl, Beth and Pellizzari give the matrix-element form (3.19) (arXiv:quant-ph/9610042).
• 1999: Cleve, Gottesman and Lo introduce the three-qutrit code as a quantum secret-sharing scheme (arXiv:quant-ph/9901025).
• 2006: Ryu and Takayanagi propose the holographic entanglement-entropy formula (arXiv:hep-th/0603001).
• 2007: Bény, Kempf and Kribs develop operator-algebra quantum error correction (arXiv:quant-ph/0608071, arXiv:0705.1574), of which the theorem here is a special case.
• 2014–2015: Almheiri, Dong and Harlow recast bulk reconstruction as quantum error correction; Pastawski, Yoshida, Harlow and Preskill build holographic tensor-network codes (arXiv:1503.06237).
• 2016: Dong, Harlow and Wall establish reconstruction in the entanglement wedge (arXiv:1601.05416). Harlow derives the Ryu–Takayanagi formula from operator-algebra error correction (arXiv:1607.03901).

Setting

The physical Hilbert space is a tensor product $\mathcal H = \mathcal H_E\otimes\mathcal H_{\bar E}$ of finite-dimensional spaces. $E$ is the part that may be erased (lost), and $\bar E$ is the part that remains. A code subspace is a subspace $\mathcal H_{\mathcal C}\subseteq\mathcal H$.

An operator $O$ acts within the code subspace if both $O$ and $O^\dagger$ map $\mathcal H_{\mathcal C}$ into itself. Such an operator has a representation on $\bar E$ if there is an operator $O_{\bar E}$ acting only on $\bar E$, that is of the form $\mathbb 1_E\otimes Y$, with

$$O_{\bar E}|\tilde\psi\rangle = O|\tilde\psi\rangle,\qquad O_{\bar E}^\dagger|\tilde\psi\rangle = O^\dagger|\tilde\psi\rangle\qquad\text{for all }|\tilde\psi\rangle\in\mathcal H_{\mathcal C}.$$

Representations on $E$ are defined in the same way, with operators $X\otimes\mathbb 1_{\bar E}$.

The three-qutrit code (Section 3.1) encodes one qutrit into three via

$$|\tilde\imath\rangle = \tfrac{1}{\sqrt3}\textstyle\sum_{a\in\mathbb Z_3}|a,\ a+i,\ a+2i\rangle,$$

that is, $|\tilde 0\rangle = (|000\rangle+|111\rangle+|222\rangle)/\sqrt3$ and so on (Eq. (3.3)).

Formalization targets

Goal: the basic theorem of operator-algebra quantum error correction (Section 3.5, proof in Appendix B)

For an operator $O$ acting within $\mathcal H_{\mathcal C}$,

$$O\ \text{has a representation on }\bar E\iff \langle\tilde\psi'|\,[O,\,X_E\otimes\mathbb 1_{\bar E}]\,|\tilde\psi\rangle = 0\ \ \text{for all } X_E \text{ on } E \text{ and all } |\tilde\psi\rangle,|\tilde\psi'\rangle\in\mathcal H_{\mathcal C}.$$

Milestones (in source order)

1. Section 3.1 (after Eq. (3.3)): for every encoded three-qutrit state, the reduced density matrix of each single qutrit is $\tfrac13\mathbb 1$.
2. Eqs. (3.4)–(3.6): the permutation $U_{12}$ of Eq. (3.6) is unitary, and $(U_{12}\otimes I_3)|\tilde\imath\rangle = |i\rangle\otimes\tfrac1{\sqrt3}(|00\rangle+|11\rangle+|22\rangle)$.
3. Eqs. (3.9)–(3.10): for every single-qutrit operator $O$, the operator $O_{12} = U_{12}^\dagger (O\otimes\mathbb 1) U_{12}$, with $O$ acting on the first qutrit, satisfies $O_{12}|\tilde\imath\rangle = \sum_j O_{ji}|\tilde\jmath\rangle$.
4. Section 3.2, Eqs. (3.19) ⟺ (3.21): the projection of every $X_E$ onto the code subspace is proportional to the identity iff every operator acting within the code subspace has a representation on $\bar E$. The source states, citing the literature, that (3.19) is equivalent to correctability of the erasure of $E$; that equivalence is not formalized.
5. Section 3.5, two-qubit example: on the code spanned by $(|00\rangle+|11\rangle)/\sqrt2$ and $(|01\rangle+|10\rangle)/\sqrt2$, the logical $X$ is realized by the bit flip of either qubit. No operator on the first qubit alone reproduces the logical $Z$ on the code, and every logical operator realizable on the first qubit acts on the code as $a\mathbb 1 + b\bar X$: the code corrects only the subalgebra generated by $\mathbb 1$ and $\bar X$.
6. Section 3.5, algebraic no-cloning: if $O_1$ has a representation on $\bar E$ and $O_2$ has a representation on $E$, then $O_1$ and $O_2$ commute on the code subspace. Consequently, the elements of any family of logical operators that is represented both on $E$ and on $\bar E$ commute pairwise on the code subspace, so a non-abelian algebra cannot be represented on both.

Significance

The result. The goal theorem characterizes, by a checkable commutation condition, which logical operators survive the loss of $E$; milestone 4 is its specialization to full erasure correction. Milestone 6 explains why a non-commuting algebra of bulk operators cannot be represented on two complementary boundary regions at once, so reconstructions of $\phi(x)$ on different regions are distinct operators that agree only on the code subspace. The three-qutrit code models this: every logical operator is realized on any two qutrits, and no single qutrit carries information.

Formalizing it. All statements are proved in the source, or cited there from standard references, and are finite-dimensional. This mission produces machine-checked versions and a reusable vocabulary of code subspaces, logical operators and subsystem representations. That vocabulary is the starting point for formalizing the later results it underlies, in particular the subsystem and operator-algebra theorems of Harlow's derivation of the Ryu–Takayanagi formula (arXiv:1607.03901).

Status honesty. The mathematics is unconditional finite-dimensional linear algebra. The application to AdS/CFT rests on the conjectured duality and on bulk effective field theory, and is context only; none of it enters the hypotheses. The appendix proof is the authors' own, and the theorem is a special case of the results of Bény, Kempf and Kribs. The equivalence of (3.19) with correctability of the erasure (the existence of a recovery unitary, Eqs. (3.14)–(3.18)) is cited in the source from Schumacher–Nielsen and Grassl–Beth–Pellizzari, and is not part of this mission. No machine-checked proof of any of these statements is known. Neither Mathlib nor Physlib (including its quantum-information library) formalizes code subspaces, erasure correction or operator-algebra quantum error correction.

Difficulty

The forward direction of the goal is a direct computation. The converse is an existence statement: an operator $O_{\bar E}=\mathbb 1_E\otimes Y$ has to be produced from a hypothesis that constrains only the matrix elements of $O$ between code states. That hypothesis says nothing about how $O$ acts off the code subspace, and $O$ generally acts nontrivially on $E$. So no candidate for $Y$ can be read off from $O$ itself.

Milestone 4 has the same character in both directions. One direction must produce a representation on $\bar E$ for every operator acting within the code subspace, starting from the scalar condition (3.19), which concerns operators on $E$ alone. The other direction is a non-existence claim about operators on $E$, to be derived from a property quantified over all logical operators.

The explicit-code milestones are finite but involve the irrational normalization $1/\sqrt3$ and a $27$-dimensional space.

Formalization scope

• Representation. Vectors on $\mathcal H_E\otimes\mathcal H_{\bar E}$ are functions on $e\times\bar e$ for finite types $e,\bar e$, with $E$ first. Operators are complex matrices, tensor products are Mathlib's Kronecker product ⊗ₖ, $O^\dagger$ is the conjugate transpose, and $\langle w|u\rangle$ is star w ⬝ᵥ u.
• Code subspace. The code subspace is an arbitrary complex subspace (Submodule ℂ). It is described without a basis: "$\langle\tilde\imath|\cdots|\tilde\jmath\rangle = 0$ for all $i,j$" is stated for all pairs of code vectors, which is equivalent by sesquilinearity.
• Proportionality. Eq. (3.19), $\langle\tilde\imath|X_E|\tilde\jmath\rangle = \delta_{ij}C(X)$, is stated basis-free as $\langle w|X_E v\rangle = c\,\langle w|v\rangle$ for one constant $c$ and all code vectors $v,w$.
• Three-qutrit vectors. These are indexed by $((q_1,q_2),q_3)$. $U_{12}$ is the permutation matrix of the table in Eq. (3.6), and the single-qutrit reduced states are partial traces over the other two qutrits.
• Not trivial. The goal quantifies over every code subspace and every operator acting within it. The zero subspace makes both sides true and is harmless. The examples are fixed concrete codes.
• Not formalized. Cited but not proved in the source: (3.14) with the recovery unitary (3.16)–(3.18), and the bound (3.25). Heuristic: the count (3.22) and the Page-theorem argument after it. Definitions only: quantum secret sharing (Section 3.3), (3.23) and (3.24). Immediate or by symmetry: (3.20), recovery from qutrits 2,3 or 1,3, and the $*$-subalgebra remark after the theorem. Out of scope: Sections 4–5 (the AdS/CFT model, backreaction).
• Infrastructure. A complete development needs lemmas on Kronecker products acting on vectors ((A ⊗ₖ B) *ᵥ v), conjugate transposes of Kronecker products, orthogonal projection onto a Submodule, and partial traces. These are reusable; stand-alone contributions are welcome.

Selected references

• A. Almheiri, X. Dong, D. Harlow, Bulk locality and quantum error correction in AdS/CFT, JHEP 04 (2015) 163. arXiv:1411.7041
• C. Bény, A. Kempf, D. W. Kribs, Generalization of quantum error correction via the Heisenberg picture, Phys. Rev. Lett. 98, 100502 (2007). arXiv:quant-ph/0608071
• C. Bény, A. Kempf, D. W. Kribs, Quantum error correction of observables, Phys. Rev. A 76, 042303 (2007). arXiv:0705.1574
• B. Schumacher, M. A. Nielsen, Quantum data processing and error correction, Phys. Rev. A 54, 2629 (1996). arXiv:quant-ph/9604022
• M. Grassl, T. Beth, T. Pellizzari, Codes for the quantum erasure channel, Phys. Rev. A 56, 33 (1997). arXiv:quant-ph/9610042
• R. Cleve, D. Gottesman, H.-K. Lo, How to share a quantum secret, Phys. Rev. Lett. 83, 648 (1999). arXiv:quant-ph/9901025
• S. Ryu, T. Takayanagi, Holographic derivation of entanglement entropy from AdS/CFT, Phys. Rev. Lett. 96, 181602 (2006). arXiv:hep-th/0603001
• F. Pastawski, B. Yoshida, D. Harlow, J. Preskill, Holographic quantum error-correcting codes: toy models for the bulk/boundary correspondence, JHEP 06 (2015) 149. arXiv:1503.06237
• X. Dong, D. Harlow, A. C. Wall, Reconstruction of bulk operators within the entanglement wedge in gauge-gravity duality, Phys. Rev. Lett. 117, 021601 (2016). arXiv:1601.05416
• D. Harlow, The Ryu–Takayanagi formula from quantum error correction, Commun. Math. Phys. 354, 865 (2017). arXiv:1607.03901

Why single-use information can underestimate communication

A sender can encode a classical message in a quantum state, transmit that state through a noisy quantum channel, and let a receiver measure the output. For researchers studying classical communication over quantum systems, the question is whether evaluating one channel use captures the benefit of encoding across several uses. Hastings established that the relevant information quantity can violate additivity when joint inputs are allowed. Hastings, 2009.

The result contributed here concerns the size of that discrepancy in finite dimensions. It gives channels for which positive single-use information is arbitrarily small while both the absolute two-use additivity gap and the relative benefit of two uses are arbitrarily large. The paper's introduction states the gap, capacity, and separation consequences; the released Lean theorem packages the small-information, gap, and ratio conclusions into one common-witness statement. Revised manuscript, Section 1, headline Lean theorem.

Channels, states, and information in bits

A finite-dimensional quantum channel $T:M_a(\mathbb C)\to M_b(\mathbb C)$ is a completely positive, trace-preserving linear map on complex matrices, where the positive integers $a,b$ are its input and output dimensions. A density matrix $\rho$ is a positive semidefinite matrix with trace one. Such matrices represent the possible input states. The released development represents a channel by finitely many rectangular Kraus matrices $A_k$, satisfying $\sum_k A_k^*A_k=I_a$, with action $T(X)=\sum_k A_kXA_k^*$. Concrete channel definitions.

The von Neumann entropy in bits is $S(\rho)=-\sum_j\lambda_j\log_2\lambda_j$, where $\lambda_j$ are the eigenvalues of $\rho$, using $0\log 0=0$. A finite ensemble consists of density matrices $\rho_x$ and real probabilities $p_x\ge0$ with $\sum_xp_x=1$. The Holevo quantity is

$$\chi(T)=\sup_{\{p_x,\rho_x\}} \left[S\!\left(\sum_xp_xT(\rho_x)\right) -\sum_xp_xS(T(\rho_x))\right].$$

The supremum includes all normalized finite ensembles. For two uses, $T^{\otimes2}$ acts on joint inputs, including states entangled between the uses. Write $\chi_2(T)=\chi(T^{\otimes2})$, $\Delta_\chi(T)=\chi_2(T)-2\chi(T)$, and, when $\chi(T)>0$, $r_2(T)=\chi_2(T)/(2\chi(T))$. These are the released definitions chi, chiTwo, gap, and twoUseRatio. Definitions.

The broader release also studies operational classical capacity $C(T)$: the supremum of achievable classical message rates in bits per use. Its independent definition uses actual density-matrix codewords, a normalized positive-operator-valued measurement decoder, and average Born decoding error tending to zero over all positive block lengths. Arbitrary block inputs and joint decoding are allowed. That coding development provides context for the result; it is a separate released branch outside this contribution's initial import. Released operational definition.

Formalization targets

Simultaneous small information, large absolute gap, and large ratio

The headline statement is

$$\forall\varepsilon>0\;\forall A,R\in\mathbb R\;\exists T: \quad 0<\chi(T)\le\varepsilon,\qquad \Delta_\chi(T)\ge A,\qquad r_2(T)\ge R.$$

One channel witnesses every inequality. The lower-bound thresholds $A,R$ are arbitrary real numbers; they are not restricted to positive values in the Lean statement. Input and output dimensions may depend on the thresholds. The goal imposes no hard-coded dimension bound or numerical constant. It is the exact statement of Nonadditivity.DeterministicConsequences.exists_small_chi_large_gap_and_ratio. Source.

The supporting separation statement uses a sequence of genuine finite channels $T^{(K)}$ with

$$\chi(T^{(K)})\longrightarrow0,\qquad \frac{\chi_2(T^{(K)})}{2}\longrightarrow+\infty.$$

The separation statement is already proved for the selected deterministic family. It gives the two information limits asserted in the manuscript's Corollary 1.3, with no analytic channel-existence assumption. The formal family is totalized at its first two indices by the one-dimensional identity channel; this finite prefix does not affect either limit. Its members have positive single-use Holevo information for every $K\ge2$. Released family, positivity, and limits.

What the result and its formal proofs provide

The theorem gives unbounded absolute Holevo additivity gaps and unbounded two-use ratios for the same witnesses, even while their single-use information is arbitrarily small. This supplies an existence result rather than an efficient method for finding small channels with practical parameters. The manuscript separately proves explicit sufficient input dimensions; those bounds are not conclusions of the headline theorem. Manuscript, Corollaries 1.2–1.3.

The mathematical result is proved, and its principal endpoints already have machine-checked Lean proofs in release v1.0.0. This contribution imports the existing deterministic separation theorem and its dependency library, preserving their source provenance and proofs. The reusable material includes density matrices, concrete channels, entropy, finite ensembles, tensor products, and the finite-channel construction. Independent review of the correspondence between the formal statements and the manuscript remains useful. Release and verification scope.

The broader release additionally proves $C(T)=\sup_{m\ge1}\chi(T^{\otimes m})/m$ from independently defined physical codes, implying $C(T)-\chi(T)\ge\Delta_\chi(T)/2$. It also proves a common-witness theorem combining small positive information with arbitrary capacity gain and two-use ratio. Those operational results are separate released context, rather than targets or imported milestones of this contribution. They concern unassisted memoryless communication and do not assert distinct-channel capacity nonadditivity or a strong converse. Released coding identity, released operational consequence.

Why the uniform bounds matter

A separate information estimate for each channel factor does not control inputs entangled across an entire block. The construction needs bounds valid for every such joint input, while retaining the favorable two-use behavior. Likewise, convergence of averaged matrix moments alone need not control exceptional eigenvalues and therefore cannot replace the needed norm control. These are substantive uniformity requirements in the paper's construction. Manuscript, Section 1.

Regrouping tensor powers of one fixed channel is insufficient for a gap linear in the regrouping length: the manuscript shows $\Delta_\chi(T^{\otimes m})/m\to0$ for a fixed $T$. The existential goal instead allows channel dimensions and the channel itself to vary. Fixed-channel limitation.

Formalization scope and conventions

The imported representation is ActualConsequences.FiniteQuantumChannel: finite, nonempty input and output index types, a finite environment index type, and a concrete Kraus channel. Entropy is computed spectrally with natural logarithms internally; holevoBits divides by $\ln2$. Supremum and infimum uses are accompanied by the developed nonemptiness and boundedness results. Positive tensor powers are indexed by a natural number $n$ meaning $n+1$ uses. Strict positivity of the goal's $\chi(T)$ prevents division-by-zero interpretations of its ratio. The channel and information quantities must retain these physical definitions; numerical records assigned the desired values would not formalize the result. Formal representation, bit conversion.

The headline proof uses the alternate deterministic finite-channel construction. It does not assert the prescribed-dimension result. The imported library provides complex matrix analysis, positivity and trace normalization, tensor products, entropy inequalities, finite ensembles, and the construction's finite group and moment infrastructure. The full manuscript remains outside the completed formalization: general Haar convergence interfaces and the broader finite-dimensional realization statement retain their documented limitations. The release's correspondence findings remain qualified; no complete semantic audit or independent human certification is claimed. Formalization status, statement review.

Selected references

• Jinzhao Wang, Unbounded Holevo additivity gaps in finite dimensions, arXiv preprint, 2026. arXiv:2609.18222v2; revised manuscript retained in the formalization release.
• M. B. Hastings, Superadditivity of communication capacity using entangled inputs, Nature Physics 5, 255–257, 2009. arXiv:0809.3972.
• A. S. Holevo, The capacity of the quantum channel with general signal states, IEEE Transactions on Information Theory 44, 269–273, 1998. DOI:10.1109/18.651037.
• B. Schumacher and M. D. Westmoreland, Sending classical information via noisy quantum channels, Physical Review A 56, 131–138, 1997. DOI:10.1103/PhysRevA.56.131.
• P. W. Shor, Equivalence of additivity questions in quantum information theory, Communications in Mathematical Physics 246, 453–472, 2004. arXiv:quant-ph/0305035.
• Nonadditivity project contributors, Holevo Additivity Gap: Lean certificates, software release v1.0.0, 2026. Release, source commit 635aa93eb3a2310b79fd5371e2ce311914ec5887.

Motivation: comparing quantum processes

A quantum channel describes a physical process that transforms a quantum state into another state. Comparing two channels means comparing their possible outputs, including outputs obtained when the input is entangled with a reference system. This distinction matters in quantum information: an experiment can retain a reference while sending the other part of an entangled state through an unknown process. The resulting measure of distinguishability should account for that experiment.

For states, several divergence measures approach relative entropy when their order parameter approaches one. For channels, optimization over inputs and arbitrarily many channel uses introduces an additional question: does this continuity survive those optimizations? Jinzhao Wang and Yuxiang Yang answer that question for the regularized, stabilized sandwiched Rényi divergence in Continuity of Regularized Channel Rényi Divergences, arXiv:2609.28635v1, Theorem 1. This mission contributes the completed result and its supporting formal infrastructure.

Setting: states, references, and repeated uses

Let $H$ and $K$ be nonzero finite-dimensional complex Hilbert spaces. A density operator is a positive operator with trace one. Two channels $N,M:\mathcal L(H)\to\mathcal L(K)$ are completely positive, trace-preserving linear maps with the same input and output spaces.

The relative entropy $D(\rho\Vert\sigma)$ compares density operators $\rho$ and $\sigma$. The sandwiched Rényi divergence $\widetilde D_\alpha(\rho\Vert\sigma)$ is an order-dependent comparison, defined for $\alpha\ge\tfrac12$, $\alpha\ne1$. The state, channel, and regularized divergences are measured in bits. Operator-level analytic lemmas may use natural logarithms; the state wrappers divide by $\log 2$. Singular states are allowed; the support conventions retain infinite values rather than assigning a finite substitute. These are the state quantities in the paper's equations (1.2)–(1.3).

The stabilized channel divergence optimizes the state divergence over normalized pure inputs on $H\otimes R$, where $R$ is a copy of $H$. The channel acts on $H$ and the identity acts on $R$. Writing $\psi=|\psi\rangle\langle\psi|$, the convention is

$$\mathbb D(N\Vert M)=\sup_{\|\psi\|=1} \mathbb D\bigl((N\otimes\operatorname{id}_R)(\psi) \Vert(M\otimes\operatorname{id}_R)(\psi)\bigr),$$

where $\mathbb D$ denotes either state divergence. The paper places the reference first; the formalization places it second and proves the tensor-factor convention agrees. A block of $n$ uses employs $N^{\otimes n},M^{\otimes n}$ and a reference copy of $H^{\otimes n}$. Its pure input may be entangled across every use. Equation (1.4) specifies this stabilization.

Formalization targets

The regularized divergences are defined independently as positive-block suprema:

$$\widetilde D_\alpha^{\mathrm{reg}}(N\Vert M) =\sup_{n\ge1}\frac{\widetilde D_\alpha(N^{\otimes n}\Vert M^{\otimes n})}{n}, \qquad D^{\mathrm{reg}}(N\Vert M) =\sup_{n\ge1}\frac{D(N^{\otimes n}\Vert M^{\otimes n})}{n}.$$

Two supporting targets establish that these definitions are the actual asymptotic limits in equation (1.5). For every fixed $\alpha\ge\tfrac12$, $\alpha\ne1$,

$$\lim_{n\to\infty}\frac{\widetilde D_\alpha(N^{\otimes n}\Vert M^{\otimes n})}{n} =\widetilde D_\alpha^{\mathrm{reg}}(N\Vert M),$$

and

$$\lim_{n\to\infty}\frac{D(N^{\otimes n}\Vert M^{\otimes n})}{n} =D^{\mathrm{reg}}(N\Vert M).$$

The main goal is Theorem 1:

$$\lim_{\alpha\to1,\,\alpha\ne1} \widetilde D_\alpha^{\mathrm{reg}}(N\Vert M) =D^{\mathrm{reg}}(N\Vert M).$$

This is convergence from both sides. Each target includes infinite divergence. The block identities are supporting identifications, rather than extra premises of the main theorem.

Significance: continuity after optimization

The main result identifies a single limit after optimization over entangled inputs and unbounded block lengths. It permits near-one regularized Rényi quantities to approach regularized relative entropy for arbitrary channel pairs in the stated finite-dimensional setting. When the latter is infinite, the conclusion is convergence to positive infinity. The paper discusses applications to discrimination and asymptotic approximation; those operational conclusions are beyond this mission's targets. Wang–Yang, arXiv:2609.28635v1.

This is a contribution of a known, formally proved result, rather than an unsolved conjecture. The original public Lean development includes proofs of the definitions' supporting properties and both block identities. Its recorded verification reports Lean checking with a transitive axiom audit, Comparator statement comparison and Lean kernel replay, and independent Nanoda kernel checking. These records concern the original pinned development. They are unsigned and do not establish independent human review of correspondence to the paper. The converted contribution uses Lean 4.30.0 and Mathlib c5ea003. Its 95 Definition bundles and 27 theorem nodes have been published; every theorem has an ACCEPTED proof and public Proved status. Before upload, the exact statement and solution files compiled locally, their types and transparent definition values were compared with the frozen compatibility port, and a transitive axiom audit of every generated declaration found only propext, Classical.choice, and Quot.sound. These new checks are separate from the original Comparator and Nanoda records. Human review of correspondence to the paper is still required.

Difficulty: optimization and singular inputs

Pointwise continuity for a fixed pair of output states does not justify interchanging a limit with the supremum over all block inputs. That domain includes every positive block length, so finite-dimensionality of each block does not itself supply a uniform conclusion. The right-hand limit is particularly sensitive to the order of these operations. Singular inputs introduce a separate issue: support mismatch can force genuine infinity, and converting all expressions to ordinary real numbers would discard that case. The formalization must preserve these domains and conventions throughout, as documented in the paper-to-Lean mapping.

Formalization scope

The Lean representation uses actual positive density operators, CPTP maps, reference systems, and tensor powers. State divergences have extended-real values; channel and regularized divergences take values in $[0,+\infty]$. Nonnegativity is proved for the admissible orders, so conversion to nonnegative extended reals preserves those values. Supremum definitions quantify over positive block lengths. The normalized block sequences are total at $n=0$, which is irrelevant to convergence as $n\to\infty$.

The main formal statement uses a punctured neighborhood of one. A sufficiently small such neighborhood lies within $\alpha>\tfrac12$, so totalized definitions at other real orders impose no assertion about their divergence interpretation outside the admissible range. No support inclusion, finite max-relative entropy, filter estimate, or Schatten estimate is assumed by the main theorem. Defining the limiting value to equal the desired conclusion, or replacing arbitrary channels by an easy special family, would not meet these targets.

The development builds on Mathlib and Lean-Quantum. Reusable components include extended-valued Fekete convergence, channel tensor identities, quantum testing quantities, prescribed-dilation approximation, and finite-dimensional Schatten bounds. The scope mapping records that the supporting decomposition estimate is formalized for $1<\alpha\le2$, sufficient near one; it does not claim the paper's entire all-orders version. Contributions that improve reuse, verify the converted dependency graph, or extend separately stated results are welcome. The paper's later operational corollaries are excluded.

Selected references

• Jinzhao Wang and Yuxiang Yang, Continuity of Regularized Channel Rényi Divergences, arXiv preprint, 2026, version 1. Paper and versioned source.
• Jinzhao Wang, Continuity of regularized channel Rényi divergence: Lean formalization, public software repository, 2026; development assisted by Codex. Source commit e29274a, v1.1.0 verification release.
• Hayata–Yamasaki Group, Lean-Quantum, formalization library, pinned revision bf1c4f6, 2026. Dependency source.
• Lean community, Mathlib4, mathematical library for Lean 4, 2026. Converted contribution's selected revision c5ea003.

Status: complete. This mission records a finished formalization rather than an open call for work. Every statement below, including the goal, was uploaded together with a proof that the platform has verified, so there is nothing left to prove.

Motivation

The Lovász Local Lemma (LLL) is a basic tool of the probabilistic method. It shows that a collection of rare "bad" events can all be avoided simultaneously, even when the events are not independent, provided each event depends on only a few others. Its best-known application is to satisfiability: a $k$-CNF formula in which every variable appears in few clauses has a satisfying assignment.

Quantum satisfiability ($k$-QSAT) is the quantum analogue of $k$-SAT. Clauses are replaced by projectors acting on $k$ qubits, and the question is whether some nonzero state is annihilated by all of them, equivalently whether the corresponding local Hamiltonian is frustration-free. Bravyi showed that $k$-QSAT is $\mathsf{QMA}_1$-complete for $k \ge 4$, so sufficient conditions for satisfiability are of interest in quantum complexity theory and in many-body physics. Ambainis, Kempe and Sattath (arXiv:0911.1696, J. ACM 2012) proved a quantum version of the LLL in which probability is replaced by relative dimension, and derived a sufficient condition for $k$-QSAT instances to be satisfiable.

Timeline

• 1975. Erdős and Lovász introduce the local lemma, in the symmetric form, to colour hypergraphs (Infinite and Finite Sets, 1975).
• 1977. Spencer publishes the general (asymmetric) form, credited to Lovász, and applies it to Ramsey numbers (Discrete Math. 20, 1977).
• 1985. Shearer determines the optimal dependency condition, in terms of the independence polynomial of the dependency graph (Combinatorica 5, 1985).
• 2009 to 2010. Moser gives a constructive proof for $k$-SAT (arXiv:0810.4812, STOC 2009); Moser and Tardos make the general lemma constructive (arXiv:0903.0544, J. ACM 2010).
• 2011. Kolipaka and Szegedy show that the Moser and Tardos algorithm works throughout Shearer's region, giving an algorithmic proof of Shearer's bound (Moser and Tardos meet Lovász, STOC 2011, 235 to 244).
• 2009 to 2012. Ambainis, Kempe and Sattath prove the quantum local lemma and its $k$-QSAT corollaries (arXiv:0911.1696, J. ACM 59(5):24, 2012).
• 2013. Arad and Sattath (arXiv:1310.7766) and, independently, Schwarz, Cubitt and Verstraete (arXiv:1311.6474) give constructive versions for commuting projectors.
• 2016. Sattath, Morampudi, Laumann and Moessner extend Shearer's criterion to the quantum setting and conjecture that it is tight (arXiv:1509.07766, PNAS 2016).
• 2017. He, Li, Liu, Wang and Xia show that the abstract and variable versions of the local lemma differ: Shearer's bound, tight for the abstract version, is not tight for the variable version (the setting of $k$-SAT, where events are determined by independent variables) for instance when the base graph of the event-variable graph has an induced cycle of length at least 4, while there is no gap when it is a tree (arXiv:1709.05143, FOCS 2017).
• 2017. Gilyén and Sattath give an efficient quantum algorithm for the non-commuting case under a spectral gap condition (arXiv:1611.08571, FOCS 2017).
• 2018 to 2019. He, Li, Sun and Zhang prove this conjecture: Shearer's bound is tight for the quantum local lemma, so in this respect the quantum lemma behaves like the abstract version rather than the variable one; they also show that the tight regions of the quantum lemma and of its commuting variant differ in general (arXiv:1804.07055, STOC 2019).

Setting

Let $V$ be a nonzero finite-dimensional vector space. For a subspace $X \subseteq V$, the relative dimension is

$$R(X) = \frac{\dim X}{\dim V}.$$

It plays the role of probability: subspaces replace events, intersection replaces conjunction, and $R(X \mid Y) = \dim(X \cap Y)/\dim Y$ replaces conditional probability.

Subspaces $X_1, \dots, X_n$ have dependency sets $\Gamma(1), \dots, \Gamma(n) \subseteq \{1, \dots, n\}$ when, for every $i$ and every set $S$ of indices with $i \notin S$ and $S \cap \Gamma(i) = \emptyset$,

$$R\Big(X_i \cap \bigcap_{j \in S} X_j\Big) = R(X_i)\, R\Big(\bigcap_{j \in S} X_j\Big).$$

In words, $X_i$ is independent, for relative dimension, of every intersection of subspaces outside its dependency set.

A $k$-QSAT instance on $n$ qubits is a family of projectors $\Pi_1, \dots, \Pi_m$, each acting on a set of $k$ qubits and extended by the identity on the others. It is satisfiable if a nonzero state lies in the kernel of every $\Pi_i$.

The formalization proves the local lemma once, for an abstract valuation: a real function $R$ on a bounded lattice that is nonnegative, monotone and modular, $R(x) + R(y) = R(x \vee y) + R(x \wedge y)$, with $R(\top) = 1$ and $R(\bot) = 0$. Relative dimension on subspaces and the uniform probability on subsets of a finite set are the two instances used.

Formalization targets

Goal: the quantum local lemma (Theorem 14)

Let $X_1, \dots, X_n$ be subspaces with dependency sets $\Gamma(i)$, and let $0 \le y_i < 1$ satisfy $R(X_i) \ge 1 - y_i \prod_{j \in \Gamma(i)} (1 - y_j)$ for every $i$. Then

$$R\Big(\bigcap_{i=1}^{n} X_i\Big) \ \ge\ \prod_{i=1}^{n} (1 - y_i).$$

Other formalized results

All of these are proved on Prove2Me and can be found by name (tag quantum-lll):

1. The same statement for any valuation on a bounded lattice (Theorem 14, abstract form): QLLL.Valuation.lll.
2. The symmetric quantum local lemma: if $R(X_i) \ge 1 - p$, each $X_i$ has at most $d$ dependencies and $p \cdot e \cdot (d + 1) \le 1$, then $R(\bigcap_i X_i) > 0$ (Theorem 4): QLLL.quantum_lll_symmetric.
3. The classical Erdős and Lovász local lemma, asymmetric and symmetric (Theorems 13 and 1), for the uniform probability on a finite set: QLLL.SAT.classical_lll, QLLL.SAT.classical_lll_symmetric.
4. $k$-SAT: a $k$-CNF formula in which every variable appears in at most $2^k/(e k)$ clauses is satisfiable (Corollary 2): QLLL.SAT.sat_of_degree_le.
5. $k$-QSAT: an instance of rank-$\le r$ constraints in which every qubit appears in at most $2^k/(e r k)$ constraints is satisfiable (Corollary 16): QLLL.PiQSAT.inf_ker_extendOp_ne_bot on Mathlib's tensor product, and QLLL.QSAT.satisfiable_of_degree_le for orthogonal projectors.
6. Two results beyond the paper: infinite $k$-SAT (QLLL.SAT.exists_assignment_forall), and the local lemma for infinite index sets under a continuity hypothesis (QLLL.lll_iInf).

Significance

The quantum local lemma gives a sufficient condition for $k$-QSAT satisfiability that depends only on the local structure of the instance: the rank of the projectors and the number of projectors per qubit. It shows that the classical criterion survives the passage from events to subspaces, even though subspaces do not form a distributive lattice. Later work on constructive and tight versions, listed in the timeline, builds on this statement.

All results of this mission are proved and machine-checked. The Lean development was written as a complete formalization of the paper, and every statement here was uploaded together with a proof verified by the platform. What the mission adds is a reusable, Mathlib-based library: the local lemma for abstract valuations, its classical and quantum instances, $k$-QSAT stated on Mathlib's tensor product of qubits, and linear algebra on intersections of tensor products of subspaces that Mathlib does not yet contain. Mathlib currently has no form of the Lovász Local Lemma.

Difficulty

The classical proof uses complements of events and the identity $\Pr(A) + \Pr(A^c) = 1$, together with the distributive law for events. Subspaces satisfy neither in general: the lattice of subspaces is modular but not distributive, and the orthogonal complement does not distribute over intersections. The argument has to be rebuilt from the properties of relative dimension that do hold. For $k$-QSAT, the further difficulty is to show that constraints acting on disjoint sets of qubits are independent for relative dimension, which requires computing intersections and dimensions of tensor products of subspaces.

Formalization scope

Conventions committed to in the Lean statements:

1. The local lemma is stated for $n$ indexed subspaces (or lattice elements) and real weights $0 \le y_i < 1$. An index is never in its own dependency set's complement: independence is required from intersections over sets $S$ that avoid both $\Gamma(i)$ and $i$ itself.
2. Independence is stated in product form, $R(X \cap Y) = R(X) R(Y)$, which agrees with the conditional form of the paper whenever the conditional relative dimension is defined.
3. The quantum lemma holds over any field and requires $V$ to be nonzero and finite-dimensional.
4. The classical lemmas are stated for good events (complements of bad events) under the uniform probability on a finite nonempty set.
5. Qubits: the main $k$-QSAT statement uses Mathlib's tensor product $\bigotimes_{j} \mathbb{C}^2$ and allows arbitrary local operators of rank at most $r$, since only the dimension of their kernels enters. A second form, on functions from bit strings to $\mathbb{C}$, requires the constraints to be orthogonal projectors (idempotent and self-adjoint). Self-adjointness cannot yet be stated on Mathlib's $n$-fold tensor product, which has no inner product in the pinned Mathlib version.
6. Degree conditions are integers: "at most $2^k/(e r k)$ projectors per qubit" is written as at most $D' + 1$ with $\frac{r}{2^k} \cdot e \cdot (k D' + 1) \le 1$, which the paper's hypothesis implies.

An infinite version of $k$-QSAT is deliberately not included. Nonzero subspaces can have all finite intersections nonzero and zero total intersection, so the infinite statement has to be phrased with compatible families of density matrices, and the current Lean formulation does not yet restrict the constraints to positive operators.

The blueprint of the formalization, linking every paper statement to its Lean declaration, is at sattath.github.io/Quantum-Lovasz-Local-Lemma/blueprint. Natural extensions, outside the scope of this mission: the orthogonal-projector form of Corollary 16 on Mathlib's tensor product once inner products on $n$-fold tensor products are available, Shearer-type conditions, and a measure-theoretic classical local lemma on general probability spaces.

A note from the contributor

This is my first contribution to Prove2Me, so the definitions, statements, proofs and descriptions may fall short of what an experienced contributor would produce. Some choices may be unidiomatic, some lemmas may duplicate Mathlib, and the split into entries could be better. Every proof is checked by Lean, so the theorems are correct as stated; the question is whether they are stated in the most useful way.

Selected references

• P. Erdős and L. Lovász, Problems and results on 3-chromatic hypergraphs and some related questions, Infinite and Finite Sets, Colloq. Math. Soc. János Bolyai 10, 1975, 609 to 627.
• J. Spencer, Asymptotic lower bounds for Ramsey functions, Discrete Math. 20, 1977, 69 to 76.
• J. B. Shearer, On a problem of Spencer, Combinatorica 5, 1985, 241 to 245.
• R. A. Moser, A constructive proof of the Lovász local lemma, STOC 2009. arXiv:0810.4812
• R. A. Moser and G. Tardos, A constructive proof of the general Lovász local lemma, J. ACM 57(2), 2010. arXiv:0903.0544
• A. Ambainis, J. Kempe and O. Sattath, A quantum Lovász local lemma, J. ACM 59(5):24, 2012. arXiv:0911.1696
• I. Arad and O. Sattath, A constructive quantum Lovász local lemma for commuting projectors, 2013. arXiv:1310.7766
• M. Schwarz, T. S. Cubitt and F. Verstraete, An information-theoretic proof of the constructive commutative quantum Lovász local lemma, 2013. arXiv:1311.6474
• O. Sattath, S. C. Morampudi, C. R. Laumann and R. Moessner, When a local Hamiltonian must be frustration-free, PNAS 113(23), 2016. arXiv:1509.07766
• A. Gilyén and O. Sattath, On preparing ground states of gapped Hamiltonians: an efficient quantum Lovász local lemma, FOCS 2017. arXiv:1611.08571
• K. He, Q. Li, X. Sun and J. Zhang, Quantum Lovász local lemma: Shearer's bound is tight, STOC 2019. arXiv:1804.07055

Motivation

Quantum mechanics predicts probabilities, but it is notoriously quiet about what a probability is. Categorical quantum mechanics answers that by rewriting the finite-dimensional formalism in the language of dagger categories: a state is a morphism $I \to A$, an effect is a morphism $A \to I$, and the probability of an outcome is a scalar — an endomorphism of the tensor unit. On that translation the Born rule stops being an axiom and becomes a theorem about a complete, disjoint family of effects.

This mission formalizes that theorem, together with the two lemmas it rests on, in Lean 4 over Mathlib. It covers the dagger and measurement material of Chapter 2 of Reutter and Vicary's Categorical Quantum Mechanics.

Setting

Fix a monoidal dagger category $\mathcal{C}$ with zero morphisms. The unit object $I$ carries a commutative monoid structure $\mathrm{End}(I)$ — the scalars. For a state $a : I \to c$ and an effect $x : c \to I$, the probability that $x$ occurs on $a$ is the scalar

$$\mathrm{Prob}(a,x) \;=\; a^\dagger \circ x^\dagger \circ x \circ a .$$

A family of effects $x : I \to \mathrm{Eff}(c)$ is complete when the induced map $\langle x \rangle : \bigoplus_i I \to c$ satisfies $\bigvee_i x_i = \mathrm{id}_c$, and disjoint when $x_i^\dagger \circ x_j = 0$ for $i \neq j$. Both conditions are stated for a dagger biproduct of the unit objects.

Formalization targets

Goal — the Born rule

$$\sum_{i} \mathrm{Prob}(a, x_i) \;=\; \mathrm{id}_I \qquad \text{for } x \text{ complete and disjoint}$$

This is the mission's goal. It fixes nothing beyond completeness and disjointness; the statement is exactly the categorical Born rule for a finite outcome set.

Supporting results

• Lemma 2.52. A family of effects is disjoint if and only if the dagger of its lift is an isometry; and complete if and only if the kernel of its lift is trivial.
• Lemma 2.53. A complete and disjoint family of effects lifts to a unitary $\langle x \rangle : \bigoplus_i I \to c$.
• Lemma 2.41, Corollary 2.42. Dagger biproducts: transposing a matrix of morphisms daggers every entry, and daggers distribute over addition.

Significance

The Born rule is the point where the categorical and the Hilbert-space pictures are reconciled: the abstract statement specialises, in $\mathbf{Hilb}$, to the usual $\sum_i |\langle x_i | a \rangle|^2 = 1$. Proving it categorically means the rule is a consequence of the dagger-biproduct structure rather than an extra assumption, which is what makes the framework usable for quantum protocols — measurement, teleportation and the like are all built on complete disjoint families.

The supporting lemmas are reusable well beyond this mission: dagger biproducts are the categorical home of matrix calculus, and the isometry/unitary characterisations of disjointness and completeness are the standard toolkit for any later argument about measurements.

Difficulty

Moderate. The mathematics is elementary once the definitions are in place — the work is in bookkeeping: biproduct universal properties, the interaction of the dagger with the biproduct structure, and careful handling of the scalar monoid. The main intellectual step is realising that completeness alone, not equalizers, gives the second unitary identity.

Formalization scope

Formalized here: dagger categories and their morphism classes (§2.3), dagger biproducts (§2.3.3), and the scalar/state/effect vocabulary with the Born rule (§2.4.3). Mathlib has no dagger-category theory at all, so the definitions are supplied from scratch as Lean Definitions and are importable independently of this mission.

Not formalized: the Hilbert-space and relational models, the graphical calculus of §2.2, and the measurement/post-processing material after §2.4.3.

Two corrections to the source are made and documented in the formalization. The printed statement of Proposition 2.55 assumes completeness only, which is false; disjointness is required, as the book's own proof (which invokes Lemma 2.52) already assumes. And the book attributes the identity $x^\dagger \circ x = \mathrm{id}$ on $A$ to Lemma 2.52, whereas Lemma 2.52 only gives the identity on $\bigoplus_i I$; the identity on $A$ is Lemma 2.53. Lemma 2.53 is proved here without the book's equalizer hypothesis, so it is strictly stronger than the printed version.

Selected references

• D. Reutter and J. Vicary, Categorical Quantum Mechanics, §2.3.3 and §2.4.3.
• S. Abramsky and B. Coecke, A categorical semantics of quantum protocols, LICS 2004.
• The Mathlib CategoryTheory.Limits.Biproducts and CategoryTheory.Monoidal.Category API, on which the definitions are built.

Motivation

Quantum algorithms for stochastic optimization are usually presented one paper at a time: a schedule is fixed, a quantum mean estimator is substituted for a classical minibatch, and a new rate is derived from scratch. The derivations are near-identical, and the step that actually differs — the price of one gradient query — is buried inside each proof rather than exposed as a parameter.

This mission publishes a Lean 4 development in which the oracle is a parameter, not an assumption. One rate theorem, instantiated at different oracle contracts and cost models, yields the classical rate, the inexact-gradient rate, and the quantum rate. All constants are explicit; nothing is asymptotic.

The published results it reproduces or corrects:

• Ghadimi--Lan (2013), the $\varepsilon^{-4}$ rate for smooth nonconvex SGD.
• Fang et al., the classical SPIDER variance-reduction schedule and its $\varepsilon^{-3}$ query complexity.
• Sidford--Zhang, Quantum speedups for stochastic optimization (arXiv:2308.01582) — Theorem 6's $\tilde O(\Delta\ell\sigma\sqrt{d}\,\varepsilon^{-3})$ and Theorem 8's $\tilde O(\ell\Delta\sqrt{d\sigma}\,\varepsilon^{-5/2})$, both obtained here from one schedule evaluated at two cost exponents.

Setting

Let $E$ be a real inner-product space, $f:E\to\mathbb{R}$ an objective, and $g:E\to E$ a map supplied as a parameter in place of the gradient. The smoothness hypothesis is the descent-lemma inequality

$$f(y)\;\le\;f(x)+\langle g(x),y-x\rangle+\tfrac{L}{2}\|y-x\|^{2},$$

written $\mathrm{QuadUpper}\,f\,g\,L$; this is exactly what rate proofs consume, and it is implied by a Lipschitz gradient. Write $\Delta_0=f(x_0)-f^{\star}$ for the initial gap, $\varepsilon$ for the target accuracy, $\sigma$ for the gradient-noise scale, $\ell$ for the mean-squared smoothness constant, and $d$ for the ambient dimension.

A cost model converts a target accuracy into a query count as a power law with exponent $p$. Its $p=2$ member is the classical minibatch bill, scaling as $\sigma^{2}/\varepsilon^{2}$; its $p=1$ member is the quantum mean-estimation bill, scaling as $\sigma/\varepsilon$. That single exponent is where classical and quantum part company.

Target

The goal theorem is the exact crossover between the two SPIDER bills. Writing $Q$ and $C$ for the dominant terms of the quantum and classical query totals,

$$Q=\frac{64000\,\ell\Delta\sqrt{d}\sqrt{10\sigma}}{\varepsilon^{2}\sqrt{\varepsilon}},\qquad C=\frac{25\,728\,000\,\ell\Delta\sigma}{\varepsilon^{3}},$$

the target asserts, for $\ell,\Delta,\sigma,\varepsilon>0$ and $d\ge0$,

$$Q<C\quad\Longleftrightarrow\quad d\,\varepsilon<16000\,\sigma .$$

Every supporting rate is also published and proved: the two SPIDER query totals, SPIDER's correctness, the SGD and PL rates, the exact and inexact gradient-descent rates, the two variance-purchase bills, and the two query counts.

Significance

The results. The crossover makes the dimension-versus-accuracy trade-off of quantum stochastic optimization quantitative rather than folkloric. Two readings follow directly: at fixed $d$ the quantum advantage disappears as $\varepsilon\to0$, so the speedup lives at moderate accuracy, not asymptotically; and at fixed $\varepsilon$ the advantage requires $d<16000\sigma/\varepsilon$. Note what cancels — $\ell$, $\Delta$ and the $\varepsilon$-exponent all drop out, leaving only $d\varepsilon$ against $\sigma$.

The formalization. Because the oracle and the cost exponent are parameters, the classical and quantum rates are one theorem evaluated twice rather than two proofs. This mission is unusual in that its frontier is already closed: every node arrives with a machine-checked proof, transplanted from a green build. What it offers the platform is a reusable, fully-proved layer for first-order convergence analysis — function classes, cost models, a one-step descent recursion, accumulation laws including a stopped-time version, and the SPIDER schedule — on which further rates can be built by instantiation.

Difficulty

The apparent difficulty is not where a newcomer expects. Deriving a rate from the one-step recursion is routine telescoping. What is delicate is keeping the constants honest while the oracle varies: a rate proof that quietly assumes an exact gradient, or a global lower bound on $f$, will produce the right-looking exponent from the wrong hypotheses.

Two specific places carry real content. Evaluating an error recursion at a random return time breaks the unconditional variance bound, because conditioning on $\tau=k$ destroys independence; the stopped-time accumulation law is what repairs it. And reproducing a published constant exactly — rather than up to $\tilde O(\cdot)$ — is what certifies that the parametrized machinery has not silently degraded the bound it generalizes.

Formalization scope

Smoothness is QuadUpper on an explicitly supplied g; no differentiability or convexity is assumed anywhere, and the only lower-bound hypothesis is $f^{\star}\le f(x_K)$ at the terminal iterate rather than globally. Cost models are an inductive family with a power-law member, so the classical and quantum instances are $p=2$ and $p=1$ of one definition. Half-integer powers are written with Real.sqrt, so no real exponentiation appears in any statement. Stochastic results use a genuine Filtration and a conditional oracle contract; the tower property is derived, not assumed.

Two honesty notes. Several statements carry hypotheses that Lean marks unused; these are recorded as such in the individual nodes rather than presented as load-bearing. And the library records a discrepancy in Sidford--Zhang's Algorithm 7 parameter block, documented in its own STATUS notes; the formalization follows the corrected parameters.

Selected references

• S. Bubeck-style descent machinery aside, the rates reproduced here are: S. Ghadimi and G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23(4) (2013).
• C. Fang, C. J. Li, Z. Lin, T. Zhang, SPIDER: Near-optimal non-convex optimization via stochastic path-integrated differential estimator, NeurIPS 2018.
• A. Sidford and C. Zhang, Quantum speedups for stochastic optimization, arXiv:2308.01582.
• Source development: lean-optrates, github.com/shiy1022/lean-optrates at commit 4c0b8498, Apache-2.0, by Yueheng Shi. The platform copy renames the root namespace OptRates to ShiOptRates; no statement or proof is otherwise altered.

Motivation

Quantum low-density parity-check codes encode quantum information using sparse parity constraints. A standard way to construct them is to translate binary chain complexes into Calderbank--Shor--Steane codes and to combine complexes by tensor product. Homology identifies the logical operators of the resulting code, while the smallest Hamming weight of a nontrivial homology class controls one of its distances. Determining how this distance behaves under a tensor product is therefore a basic structural question, not merely a parameter calculation.

Weilei Zeng and Leonid P. Pryadko studied products in which one factor is an arbitrary finite binary chain complex and the other is the one-complex induced by a binary matrix. Their paper was published as “Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates,” Physical Review Letters 122, 230501 (2019). Its main distance result is Eq. (13) in the arXiv version: for this particular tensor factor, the usual product upper bound is always exact. The result extends the familiar two-complex setting of quantum hypergraph-product codes to the local structure occurring in complexes of any dimension.

Setting

A based binary chain complex consists of finite-dimensional vector spaces $A_i$ over $\mathbb F_2$, each equipped with a specified coordinate basis, and linear boundary maps

$$\cdots\longrightarrow A_{i+1}\xrightarrow{\partial_{i+1}}A_i \xrightarrow{\partial_i}A_{i-1}\longrightarrow\cdots$$

such that $\partial_i\partial_{i+1}=0$. Its degree-$i$ homology is $H_i(\mathcal A)=\ker\partial_i/\operatorname{im}\partial_{i+1}$. The homological distance is measured in the chosen basis:

$$d_i(\mathcal A)= \min\{\operatorname{wt}(x):x\in\ker\partial_i\setminus \operatorname{im}\partial_{i+1}\}.$$

Following the paper, the minimum of an empty set is $\infty$. Thus $d_i(\mathcal A)=\infty$ when $H_i(\mathcal A)$ is trivial.

The endpoint convention is also the one stated explicitly after Eq. (1). For an $m$-complex, $\partial_0:A_0\to\{0\}$ is the zero $0\times n_0$ matrix and $\partial_{m+1}:\{0\}\to A_m$ is the zero $n_m\times0$ matrix. Consequently

$$d_0(\mathcal A)=\min\{\operatorname{wt}(x): x\in A_0\setminus\operatorname{im}\partial_1\}$$

and

$$d_m(\mathcal A)=\min\{\operatorname{wt}(x): 0\ne x\in\ker\partial_m\}.$$

For an $r\times c$ binary matrix $P$, the one-complex $\mathcal K(P)$ has $\mathbb F_2^c$ in degree one, $\mathbb F_2^r$ in degree zero, and boundary $P$. Its two distances are

$$d_1(\mathcal K(P))= \min\{\operatorname{wt}(x):Px=0,\ x\ne0\}$$

and

$$d_0(\mathcal K(P))= \min\{\operatorname{wt}(y):y\notin\operatorname{im}P\}.$$

In particular, $d_0=1$ unless $P$ has full row rank, in which case $d_0=\infty$. The degree-$j$ chain group of $\mathcal A\times\mathcal K(P)$ is

$$(A_j\otimes\mathbb F_2^r)\oplus (A_{j-1}\otimes\mathbb F_2^c),$$

with the standard tensor-product boundary. Over $\mathbb F_2$ the usual sign in that boundary has no effect.

Formalization targets

Tensor-product upper bound for arbitrary complexes

The first milestone is Eq. (11) for two arbitrary finite-length based binary chain complexes:

$$d_j(\mathcal A\times\mathcal B)\le \min_i d_i(\mathcal A)d_{j-i}(\mathcal B).$$

Rank-sensitive lower bound

Let $u=\operatorname{rank}P$ and $\delta=d_1(\mathcal K(P))$. The second milestone is Theorem 1, including both of its cases:

$$u<r\Longrightarrow d_j(\mathcal A\times\mathcal K(P))\ge \min\!\left(d_j(\mathcal A),d_{j-1}(\mathcal A)\delta\right),$$

and

$$u=r\Longrightarrow d_j(\mathcal A\times\mathcal K(P))\ge d_{j-1}(\mathcal A)\delta.$$

Exact distance with a one-complex

The goal is Eq. (13):

$$d_j(\mathcal A\times\mathcal K(P))= \min\!\left( d_{j-1}(\mathcal A)d_1(\mathcal K(P)), d_j(\mathcal A)d_0(\mathcal K(P)) \right).$$

No full-rank hypothesis is imposed on $P$.

Significance

The equality determines the product distance exactly from four component distances. General tensor-product arguments immediately provide the upper bound, but an exact formula requires ruling out lower-weight homology classes that mix the two direct-sum blocks. Once established, the formula can be applied repeatedly to tensor products of one-complexes, which is the step used in the paper to obtain higher-dimensional quantum hypergraph-product code families and to compute their distances.

For formalization, the mission contributes reusable definitions of finite based binary chain data, homological distance valued in $\mathbb N\cup\{\infty\}$, the one-complex of a binary matrix, and the relevant tensor-product boundary maps. Mathlib contains Hamming weight and general homological-algebra infrastructure, while QECLean contains a closely related based length-three homological-code interface. Neither the selected Mathlib environment nor the inspected QECLean development currently supplies this rank-sensitive exact distance theorem.

Difficulty

The central issue is that Hamming weight depends on the chosen bases and is not preserved by arbitrary homological isomorphisms. A Künneth isomorphism describes the product homology and readily produces low-weight representatives, which is enough for the upper bound, but it does not by itself exclude a still lighter representative obtained by cancellation between the two tensor blocks. The lower bound must also remain valid at the endpoints of the complex and in singular cases where one or more homology groups vanish and the relevant distance is $\infty$.

The theorem cannot be reduced to a dimension calculation. It must reason about supports and Hamming weights of based representatives while respecting the quotient by boundaries, and it must cover both $\operatorname{rank}P<r$ and $\operatorname{rank}P=r$.

Formalization scope

The Lean development works over ZMod 2. A finite basis in degree $i$ is represented by Fin (dimension i), and a chain group is the function space from that coordinate type to ZMod 2. BasedBinaryChainComplex stores the dimension and boundary in every nonnegative degree, the chain condition, and a finite length above which all dimensions are zero. Thus the first milestone quantifies over genuinely arbitrary finite lengths for both $\mathcal A$ and $\mathcal B$, rather than over a local window or a one-complex specialization. If the stored length is $m$, the zero-dimensional source in degree $m+1$ makes $\partial_{m+1}:\{0\}\to A_m$ the unique zero map, just as the zero-dimensional target below degree zero makes $\partial_0:A_0\to\{0\}$ the unique zero map. Hence both singular endpoint cases in Eqs. (1) and (4) are represented directly.

Distances use WithTop ℕ. Their definitions are actual minima of Hamming weights of nontrivial representatives, with ⊤ produced by the empty-set case; infinite distance is not an extra hypothesis or a separately hard-coded branch. Coordinate types may be empty, which covers missing endpoint blocks. The binary matrix $P$ is represented as a linear map between two finite based function spaces. Its row and column coordinate types need not be nonempty, and no injectivity or surjectivity assumption is added.

The degree-$j$ product group is indexed by the disjoint union of all coordinate products $A_i\times B_{j-i}$ for $0\le i\le j$. Consequently its Hamming norm is the sum of the weights of all tensor-degree blocks. The product boundary is the standard signed tensor boundary; its sign disappears over $\mathbb F_2$. A formal proof verifies that every pair of consecutive product boundaries composes to zero; the cancellation of the two mixed terms uses characteristic two. Thus the product distance is taken from an actual chain complex, rather than from unrelated adjacent linear maps. A basis-free tensor product or an abstract homology group alone is insufficient for the target, because either would discard the weight data on which the statement depends. The mission does not formalize the asymptotic code-family construction later in the paper, the transposed cohomological distance, or the CSS-code parameter translation. Those are natural downstream missions; they should reuse rather than alter the present based-chain definitions.

Selected references

• Weilei Zeng and Leonid P. Pryadko, “Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates,” Physical Review Letters 122, 230501 (2019). arXiv:1810.01519.
• Benjamin Audoux and Alain Couvreur, “On Tensor Products of CSS Codes,” arXiv:1512.07081 (2015), especially Proposition 1.13 and Corollary 2.14 as cited by Zeng--Pryadko.
• Jean-Pierre Tillich and Gilles 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 (2014), 1193--1202.