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.