Quantum Error Correction

Motivation

A quantum LDPC code is a CSS code whose two check matrices $H_X$ and $H_Z$ have rows and columns of bounded weight, so that every check measures only a few qubits. Such codes are the main candidates for fault-tolerant quantum memories, because their checks are local, but a code is only useful together with a decoder: an efficient procedure that recovers the error, up to stabilizers, from its syndrome. For classical LDPC codes built from expander graphs, Sipser and Spielman showed in 1996 that a simple bit-flipping algorithm corrects a constant fraction of the minimum distance in linear time (Sipser–Spielman 1996). In the quantum setting the obvious analogue fails, and before this work no family of quantum LDPC codes was known to admit an efficient decoder correcting a number of adversarial errors proportional to its minimum distance.

Timeline.

• 1996: Sipser and Spielman, expander codes and their linear-time bit-flipping decoder.
• 2009: Tillich and Zémor introduce the hypergraph product, giving quantum LDPC codes of positive rate and minimum distance of order $\sqrt n$ (arXiv:0903.0566).
• 2015: Leverrier, Tillich and Zémor take the hypergraph product of an expanding biregular graph with itself and prove that a greedy generator-flipping decoder corrects every error of weight up to a constant fraction of the minimum distance (arXiv:1504.00822, FOCS 2015). This mission formalizes that result.

Setting

Let $G = (A \cup B, \mathcal E)$ be a finite bipartite graph, $n_A = |A|$, $n_B = |B|$, with $n_B \le n_A$, and write $a \sim b$ for adjacency. $G$ is $(\Delta_A, \Delta_B)$-biregular if every vertex of $A$ has $\Delta_A$ neighbours and every vertex of $B$ has $\Delta_B$. For $S \subseteq A$ let $\Gamma(S)$ be its neighbourhood. $G$ is $(\gamma_A, \delta_A)$-left-expanding if $|\Gamma(S)| \ge (1 - \delta_A)\Delta_A |S|$ for every $S \subseteq A$ with $|S| \le \gamma_A n_A$; right expansion is the same on the $B$ side, and left-right expanding means both. $\Gamma_u(S)$ denotes the unique neighbours of $S$, adjacent to exactly one vertex of $S$.

Let $H$ be the $n_B \times n_A$ binary biadjacency matrix of $G$. The quantum code $\mathcal Q_G$ has $n = n_A^2 + n_B^2$ qubits, indexed by $A^2 \cup B^2$ (written $\alpha a$ and $b\beta$), and check matrices

$$H_X = (\mathbb 1_{n_A} \otimes H,\ H^T \otimes \mathbb 1_{n_B}), \qquad H_Z = (H \otimes \mathbb 1_{n_A},\ \mathbb 1_{n_B} \otimes H^T),$$

with rows indexed by $A \times B$ and $B \times A$. The row $ba$ of $H_Z$ has support the Z-generator $g_{ba} = \{\alpha a : \alpha \sim b\} \cup \{b\beta : \beta \sim a\}$. An $X$ error is $e \in \mathbb F_2^{A^2 \cup B^2}$, its syndrome is $\sigma_X(e) = H_X e^T$, and $\mathcal C_Z^\perp$ is the space of sums of Z-generators. The weight $w(e_X, e_Z)$ of a quantum error counts the qubits where $e_X$ or $e_Z$ is nonzero.

The decoder. On a syndrome $s$, one iteration picks a vector $e_1$ whose support lies in some generator $g_{ba}$, such that $s_1 = s + \sigma_X(e_1)$ has $|s_1| < |s|$ and the ratio $(|s| - |s_1|)/|e_1|$ is maximal among all such vectors. It iterates on the current syndrome, fails if it gets stuck at a nonzero syndrome, and otherwise outputs the sum $e_O$ of the flipped vectors. The $Z$ decoder is the same with $H_X$ and $H_Z$ exchanged.

Formalization targets

Goal: Theorem 2

Assume $G$ is $(\Delta_A, \Delta_B)$-biregular and $(\gamma_A, \delta_A, \gamma_B, \delta_B)$-left-right expanding with

$$\delta_A < \tfrac16, \qquad \delta_B < \tfrac16,$$

and let $(e_X, e_Z)$ be a quantum error with

$$w(e_X, e_Z) < w_0 = \frac{1}{3(1 + \Delta_B)} \min(\gamma_A n_A, \gamma_B n_B).$$

Then on every run, the $X$ decoder on input $\sigma_X(e_X)$ never outputs a failure and its output satisfies $e_O + e_X \in \mathcal C_Z^\perp$. The $Z$ decoder on $\sigma_Z(e_Z)$ behaves symmetrically, with $e_O + e_Z \in \mathcal C_X^\perp$.

Milestones

In the paper's order of proof:

• Lemma 3, $|\Gamma_u(S_A)| \ge (1 - 2\delta_A)\Delta_A |S_A|$;
• Proposition 4, distance at least $\gamma_A n_A$ for the classical code;
• the distance half of eq. (3), $d_Q \ge \min(d, d^T)$, already posed on the platform;
• Corollary 5, $d_Q \ge \min(\gamma_A n_A, \gamma_B n_B)$;
• the column-weight bound $|\sigma_X(e)| \le \Delta_B |e|$;
• Lemma 7, existence of a critical generator;
• the displays (19), (22), (23), (24) of Appendix B;
• Lemma 8, a step of ratio at least $1/3$ inside a critical generator;
• Lemma 10, the $X$ half of the goal.

Significance

The result. Theorem 2 gives the first family of quantum LDPC codes with an efficient decoder that corrects a number of adversarial errors proportional to the minimum distance. Here that number is of order $\sqrt n$. The same analysis yields a robustness property: low-weight errors have syndromes of proportional weight (Corollary 9 of the paper). Later work on quantum expander codes builds on this analysis, for example on their decoding under random noise (arXiv:1711.08351) and on fault tolerance with constant overhead (arXiv:1808.03821).

Formalizing it. The result is proved on paper. As far as is known, it has no machine-checked proof. The mission produces a formal statement of the decoder and its correctness, and it also produces reusable pieces:

• unique-neighbour expansion;
• the distance of expander codes;
• the distance of hypergraph product codes, tied to an open item of the Tillich–Zémor mission;
• a generic formalization of greedy syndrome-weight decoding.

Difficulty

The obvious quantum analogue of Sipser–Spielman flips single qubits that lower the syndrome weight. It fails because of degeneracy: an error and its sum with a generator have the same syndrome. A small error can therefore look locally like a large one, and no single qubit need be worth flipping. The paper's decoder instead flips arbitrary patterns inside one generator. The difficulty is to show that some pattern always lowers the syndrome weight by a constant fraction of its size. The proof needs a combinatorial structure, the critical generator, whose existence uses unique-neighbour expansion on both sides of the graph, and a case analysis on its six parts. A second difficulty is that the decoder minimizes the syndrome weight, not the error weight, so the intermediate error can grow. Bounding that growth is what limits the guarantee to $w_0$ rather than the distance.

Formalization scope

• The graph is a relation adj : A → B → Prop on finite types, and $H$ = bipMatrix adj : Matrix B A (ZMod 2).
• The published TillichZemor.HGP.Setting is reused. The paper's $H_X$ is TillichZemor.HGP.hz H H and its $H_Z$ is hx H H; the X/Z names are swapped relative to the 2009 paper, and this is checked against eq. (5) in a sanity file.
• Qubits are (A × A) ⊕ (B × B), weights are hammingNorm, and $\mathcal C_Z^\perp$ is CodingTheory.dualCode of ker H_Z.
• Expansion constants are real and cardinalities are compared in $\mathbb R$. Distance statements are per-vector, so no $\infty$-valued minimum distance is cast to a real number.
• The decoder is defined once (Candidate, Step, Reach, DecodesCorrectly), generic in the syndrome and generator matrices. Its ratio is computed in $\mathbb Q$.
• Reach contains every state reachable under any tie-breaking. Correctness requires, at every reachable state, a further step while the syndrome is nonzero, and $e_O + e$ in the row space of the generator matrix once it is zero. Termination is automatic, because each step lowers a natural number.

Additions and omissions.

• The hypothesis $\Delta_A \ge 1$ is added throughout. With $\Delta_A = 0$ the expansion conditions are vacuous, $H = 0$, and every error is invisible.
• In Lemma 8 the vector $e_1$ is required to be nonzero. With $e_1 = 0$ the printed inequality reads $0 \ge 0$.
• Lemma 8 is posed in its first assertion only. The critical generator is taken with respect to a minimum-weight representative of the coset, as in Appendix B.
• The clauses "runs in time linear in the code length" and "letting $\Delta_A$, $\Delta_B$ be fixed and allowing $n_A, n_B$ to grow" are not formalized. The goal holds for every finite graph meeting the hypotheses.

Trivializing formalizations ruled out. The goal names the paper's own decoder, not "there exists a decoder", which a brute-force coset decoder would satisfy. It quantifies over every run, not a single favourable one. It asserts both never-failing and correctness, not partial correctness alone. It uses $H_X$ = hz H H, not the swapped matrix.

Welcome contributions. Proofs of the counting milestones (Lemma 3, Proposition 4, the column-weight bound, (19), (22)–(24)) are independent of one another. The distance bound of Tillich–Zémor, open on the platform, is the deepest dependency. Unique-neighbour expansion and the hypergraph-product distance bound are useful beyond this mission.

Selected references

• A. Leverrier, J.-P. Tillich, G. Zémor, Quantum expander codes, FOCS 2015; arXiv:1504.00822v1 (2015). https://arxiv.org/abs/1504.00822
• J.-P. Tillich, G. Zémor, Quantum LDPC codes with positive rate and minimum distance proportional to the square root of the blocklength, IEEE Trans. Inf. Theory 60(2), 2014; arXiv:0903.0566. https://arxiv.org/abs/0903.0566
• M. Sipser, D. A. Spielman, Expander codes, IEEE Trans. Inf. Theory 42(6), 1996. https://doi.org/10.1109/18.556667
• O. Fawzi, A. Grospellier, A. Leverrier, Efficient decoding of random errors for quantum expander codes, STOC 2018; arXiv:1711.08351. https://arxiv.org/abs/1711.08351
• O. Fawzi, A. Grospellier, A. Leverrier, Constant overhead quantum fault-tolerance with quantum expander codes, FOCS 2018; arXiv:1808.03821. https://arxiv.org/abs/1808.03821

Motivation

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

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

Setting

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

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

Formalization targets

Goal: Theorem 5.2 (entanglement wedge reconstruction theorem)

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

A quantum computer that runs long computations must protect its data with a quantum error-correcting code and must compute on the encoded data without letting errors spread. The simplest gates with that property are transversal gates: a code is laid out in several code blocks, and a transversal gate couples each physical subsystem of one block only to the corresponding subsystem of the other blocks, so a single fault never becomes several faults inside one block (Gottesman 1997; Aliferis, Gottesman, Preskill 2006). Every known code has some encoded gate that is not transversal, and fault-tolerant schemes pay for the missing gates with expensive constructions such as magic-state distillation. Whether some code has a universal transversal gate set was a long-standing question.

Timeline.

• 2007: Zeng, Cross and Chuang show that transversal gates are not universal for stabilizer codes on qubits (arXiv:0706.1382).
• 2008: Chen, Chung, Cross, Zeng and Chuang extend this to stabilizer codes on qudits (arXiv:0801.2360).
• 2008–2009: Eastin and Knill prove the statement for every code that detects an arbitrary error on any single subsystem, stabilizer or not (arXiv:0811.4262; Phys. Rev. Lett. 102, 110502, 2009). This is the result of the present mission, now called the Eastin–Knill theorem.

Setting

A composite quantum system $\mathcal Q$ consists of finitely many physical subsystems $j$, subsystem $j$ having dimension $d_j$. Operators on $\mathcal Q$ are complex matrices on $\mathbb C^{d_1}\otimes\cdots\otimes\mathbb C^{d_n}$. A product operator is $\bigotimes_j U_j$ with $U_j$ acting on subsystem $j$, and $\mathcal T$ is the group of unitary product operators ($U_j \in \mathcal U(d_j)$).

A quantum code is a subspace of the state space, represented by the orthogonal projector $P$ onto it; its dimension $\operatorname{rank} P$ is the dimension of the encoded system, and the code is nontrivial when this dimension is at least $2$. An error $E$ is detectable when $PEP \propto P$. The code is local-error-detecting when every error on any single subsystem is detectable: $P\,(I\otimes E\otimes I)\,P \propto P$ for every operator $E$ acting on one subsystem.

A unitary $U$ is logical when it preserves the code space,

$$(I-P)\,U\,P = 0 \qquad \text{(Eq. (1))},$$

and $\mathcal G$ denotes the logical unitary product operators. An encoded unitary is a unitary operator $W$ of the code space ($PWP = W$, $W^\dagger W = WW^\dagger = P$). A set $S$ of unitaries is universal when every encoded unitary is approximated to arbitrary accuracy by the actions $PUP$, $U \in S$, on the code space.

For a code made of blocks $b$, each with subsystems at the same positions $j$ and a block code $P_b$, the joint code is $P = \bigotimes_b P_b$. The transversal part $j$ collects subsystem $j$ of every block, and a transversal unitary is a product of unitaries, one on each transversal part.

Formalization targets

Goal: Corollary 1

For block codes $P_b$, each local-error-detecting, with $\operatorname{rank}\bigotimes_b P_b \ge 2$, the set $\mathcal G$ of transversal logical unitaries is not universal:

$$\{\,W : PWP = W,\ W^\dagger W = WW^\dagger = P\,\}\ \not\subseteq\ \overline{\{\,PUP : U \in \mathcal G\,\}}.$$

Theorem 1 (milestone)

The same conclusion for product operators on the physical subsystems of a single local-error-detecting code with $\operatorname{rank} P \ge 2$.

Milestones on the way

In attack order: Lemma 1 (logical unitaries form a group); Lemma 2 (logical unitaries in a closed group of unitaries form a closed subgroup); $\mathcal T$ is a compact group; the derivative step $(I-P)DP = 0$; elements of the Lie algebra of $\mathcal T$ are sums of local Hermitian operators; $DP \propto P$ for a logical sum of local Hermitians; the identity component $\mathcal C$ of $\mathcal G$ acts on the code space as a scalar; $\mathcal G$ has finitely many actions on the code space up to phase; Theorem 1; and the detectability of an error on a single transversal part.

Significance

The result. The theorem rules out the simplest route to fault tolerance for every code that detects single-subsystem errors, which includes every code of distance at least $2$. It explains why every fault-tolerant architecture needs a non-transversal ingredient (state injection and distillation, code switching, gauge fixing, measurements with feed-forward), and it is the starting point for later refinements: approximate and covariant versions for continuous symmetries (Faist et al. 2020), and restrictions on the level of the Clifford hierarchy reachable transversally (Bravyi–König 2013).

Formalizing it. The result is proved; no machine-checked proof of it is known to exist. The mission produces a checked statement of the theorem for arbitrary finite-dimensional subsystems and arbitrary (non-stabilizer) codes, together with a reusable layer: tensor-product operators on index-typed subsystems, codes as projectors, logical operators, local error detection, encoded universality and block codes. Related platform items are QAlgorithms_Defs_QECC (qubit stabilizer codes, detectability for submodule codes) and QAlgorithms.GottesmanIntro.knillLaflamme (the error-correction criterion), which use a different model of codes and are not imported here.

Difficulty

The paper's argument runs through Lie theory: $\mathcal G$ is a closed subgroup of the compact group $\mathcal T$, so it is a compact Lie group with finitely many connected components; its identity component is generated by exponentials of its Lie algebra, and local error detection forces that Lie algebra to act on the code space by scalars. None of this is about the code alone; the difficulty is the passage from a closed matrix group to its Lie algebra and back (exponential coordinates, connectedness of the identity component, finiteness of the component group of a compact Lie group). Mathlib has the matrix exponential and compactness of the unitary group but not Cartan's closed-subgroup theorem or the Lie algebra of a closed matrix group.

A frequent first idea, that $\mathcal G$ itself is a finite group, is false: every global phase $e^{i\theta}I$ is a logical product unitary, so $\mathcal G$ always contains a circle. Only the action of $\mathcal G$ on the code space is finite, and only up to phase; a statement that ignores the phase is false.

Formalization scope

Subsystem $j$ is a finite index type $\alpha_j$ (so $d_j = |\alpha_j|$), and the system has basis $\prod_j \alpha_j$; operators are Matrix over ℂ, unitaries are Matrix.unitaryGroup. A code is its projector (Hermitian, idempotent) and its dimension is Matrix.rank; "nontrivial" is $2 \le \operatorname{rank} P$. Closure is in the standard topology on complex matrices, which is the topology of any norm. Exponentials are NormedSpace.exp with the factor $i$ of the physics convention (footnote 1).

Disclosed restatements:

1. "Lie group/Lie subgroup" (Lemma 2, $\mathcal T$) is stated as closed or compact subgroup; Cartan's theorem is not in Mathlib.
2. "$D$ in the Lie algebra" is stated through the one-parameter group $t\mapsto e^{itD}$.
3. The real coefficients $\alpha_j$ in $D = \sum_j \alpha_j H_j$ are absorbed into the Hermitian $H_j$.
4. The page's "the constant of proportionality must be one" is a slip (global phases lie in $\mathcal C$); the identity-component and finite-actions milestones state $CP \propto P$ and $GP = c\,FP$.
5. Corollary 1's code blocks are a tensor product of block codes $P_b$ with common positions $j$ and possibly different codes and dimensions; a single block is Theorem 1.

Universality is defined only through approximation of encoded unitaries, local error detection quantifies over every matrix on one subsystem, and $\mathcal G$ is the full intersection of $\mathcal T$ with the logical unitaries, so no hypothesis trivializes the conclusion; at rank $1$ the conclusion is false, which is why the rank hypothesis is $\ge 2$ and not $P \ne 0$.

A complete development needs the Lie algebra of a closed subgroup of Matrix.unitaryGroup, connectedness of the identity component via exponentials, and finiteness of the component group of a compact matrix group. These parts are reusable far beyond this mission, and contributions of them, as well as alternative proofs of Theorem 1 that avoid Lie theory, are welcome.

Selected references

• B. Eastin, E. Knill, Restrictions on Transversal Encoded Quantum Gate Sets, Phys. Rev. Lett. 102, 110502 (2009). https://arxiv.org/abs/0811.4262
• B. Zeng, A. Cross, I. L. Chuang, Transversality versus Universality for Additive Quantum Codes, IEEE Trans. Inf. Theory 57 (2011). https://arxiv.org/abs/0706.1382
• X. Chen, H. Chung, A. W. Cross, B. Zeng, I. L. Chuang, Subsystem stabilizer codes cannot have a universal set of transversal gates for even one encoded qudit, Phys. Rev. A 78, 012353 (2008). https://arxiv.org/abs/0801.2360
• D. Gottesman, Stabilizer Codes and Quantum Error Correction, PhD thesis, Caltech (1997). https://arxiv.org/abs/quant-ph/9705052
• S. Bravyi, R. König, Classification of topologically protected gates for local stabilizer codes, Phys. Rev. Lett. 110, 170503 (2013). https://arxiv.org/abs/1206.1609
• P. Faist et al., Continuous symmetries and approximate quantum error correction, Phys. Rev. X 10, 041018 (2020). https://arxiv.org/abs/1902.07714

Why decoding good quantum LDPC codes matters

Quantum computers must correct errors faster than they accumulate, and quantum low-density parity-check (LDPC) codes are the leading candidates for doing so with little overhead: every check involves a bounded number of qubits, so syndromes can be measured by local circuits. In 2021–2022 the first asymptotically good quantum LDPC codes appeared, with dimension and minimum distance both linear in the code length $n$: the expander lifted product codes of Panteleev and Kalachev (arXiv:2111.03654) and the quantum Tanner codes of Leverrier and Zémor (arXiv:2202.13641). A code is only useful if errors can be corrected efficiently. Leverrier and Zémor (arXiv:2208.05537) give two decoders for quantum Tanner codes that correct every error of weight up to a constant fraction of $n$: a sequential one running in linear time, and a parallel decoder running in a logarithmic number of rounds of local updates. This mission is about the parallel decoder.

Timeline:

• 2021, Panteleev–Kalachev: asymptotically good quantum LDPC codes and locally testable classical codes (arXiv:2111.03654).
• 2022, Leverrier–Zémor: quantum Tanner codes, a simpler construction on left-right Cayley complexes (arXiv:2202.13641).
• 2022, Gu–Pattison–Tang, Leverrier–Zémor and Dinur–Hsieh–Lin–Vidick: efficient decoders for linear-distance quantum LDPC codes (arXiv:2206.06557, arXiv:2206.07571, arXiv:2206.07750).
• 2022, Leverrier–Zémor, Decoding quantum Tanner codes: sequential and parallel decoders up to a constant fraction of $n$, with a revised parallel analysis in v3 (arXiv:2208.05537v3).

The code and the decoder

Let $G$ be a finite group and $A=A^{-1}$, $B=B^{-1}\subseteq G$ with $|A|=|B|=\Delta$. The quadripartite left-right Cayley complex has four copies of $G$ as vertices, $V_{ij}=G\times\{ij\}$, and one square $\{(g,00),(ag,01),(gb,10),(agb,11)\}$ for every $(g,a,b)\in G\times A\times B$. The set of squares $Q$ has $n=|G|\Delta^2$ elements, and every vertex $v$ sees its $Q$-neighbourhood $Q(v)$ as an $A\times B$ array: columns are indexed by $b$, rows by $a$. The left Cayley graph $\mathrm{Cay}(G,A)$ and the right Cayley graph $\mathrm{Cay}(G,B)$ are assumed to be non-bipartite Ramanujan graphs: every adjacency eigenvalue other than $\pm\Delta$ has absolute value at most $2\sqrt{\Delta-1}$.

Two local codes $C_A\subseteq\mathbb F_2^A$, $C_B\subseteq\mathbb F_2^B$ with $\dim C_A+\dim C_B=\Delta$ are fixed. Write $V_0=V_{00}\cup V_{11}$ and $V_1=V_{01}\cup V_{10}$. The code $\mathcal C_1\subseteq\mathbb F_2^Q$ consists of the vectors whose view on every $Q(v)$, $v\in V_1$, lies in the dual tensor code $C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B$: every local view is a sum of a word whose columns are in $C_A$ and a word whose rows are in $C_B$. $\mathcal C_0$ is defined in the same way on $V_0$ with $C_A^\perp$, $C_B^\perp$. The local codes and their duals have distance at least $\delta\Delta$. Both dual tensor codes are $\kappa$-product-expanding: every codeword $x$ splits as $x=c+r$ with $|x|\ge\kappa\Delta(\|c\|+\|r\|)$, where $\|c\|$ counts non-zero columns and $\|r\|$ non-zero rows.

A $\sigma_x$-type error $e\in\mathbb F_2^Q$ is decoded in three phases. In the preprocessing phase every $v\in V_1$ chooses a minimum-weight local error $\varepsilon_v$ with the local syndrome of $e$; the mismatch is $Z=\sum_{v\in V_1}\varepsilon_v$. The mismatch decomposition writes $Z=\hat C_0+\hat R_0+\hat C_1+\hat R_1$, with $\hat C_j$ a sum of $C_A$-columns and $\hat R_i$ a sum of $C_B$-rows. Postprocessing outputs $\hat e=\sum_{v\in V_{10}}\varepsilon_v+\hat C_0+\hat R_1$. The parallel decoder (Algorithm 3) runs rounds of four substeps, one for each of $V_{00},V_{01},V_{10},V_{11}$. In a substep, every vertex $v$ of the current class simultaneously looks for a non-zero local dual tensor codeword $x_v$ on $Q(v)$ with $|\hat Z|-|\hat Z+x_v|\ge|x_v|/2$, picks one of maximum weight, splits it as $c_v+r_v$ with $\|c_v\|+\|r_v\|$ minimal, and updates $\hat C_j$, $\hat R_i$ and $\hat Z$.

Formalization targets

Goal: Theorem 20 (= Theorem 3)

Fix $\varepsilon\in(0,1/6)$ and $\delta,\kappa>0$. For all $\Delta$ large enough, every error with

$$|e|<\frac1{2^{12}}\min\Big(\frac{\varepsilon^3}{16},\frac\kappa4\Big)\delta^2\kappa^2\frac n\Delta$$

is corrected by every run of the parallel decoder. With $\theta=\frac14\big(\frac14-\frac32\varepsilon\big)$, each round satisfies $|\hat Z_{k+1}|\le(1-\theta)|\hat Z_k|$, so $\hat Z_k=0$ once $(1-\theta)^k\cdot4|e|<1$, and then $e+\hat e$ lies in the span $\mathcal C_0^\perp$ of the $\sigma_x$-generators.

Milestones

• Lemma 4 (expander mixing) and Lemma 5: $\lambda(\mathcal G^\square_0),\lambda(\mathcal G^\square_1)\le4\Delta$.
• Lemmas 7, 10, 11, 8 and Theorem 9: the minimum distance, $d_{\min}\ge\delta^2\kappa^2n/(1024\Delta)$.
• Lemmas 14, 15, 16 and Theorem 12: if a minimum decomposition of a non-zero mismatch has few active vertices, some local codeword lowers $|Z|$ by $(1-\varepsilon)|x_v|$.
• Lemma 17: $|Z|\le4|e|$ and $\|Z\|\le4|e|/(\kappa\Delta)$.
• Lemma 19: below $2^{-16}\varepsilon^3\kappa^2\delta^2n/\Delta$, sequential decoding with parameter $1/2$ never stalls, and switching to $\varepsilon$ still converges.
• Lemma 18: if the $\varepsilon$-sequential decoder converges, one parallel round removes at least $\theta|Z|$.

Significance

The theorem shows that asymptotically good quantum LDPC codes can be decoded against adversarial errors of linear weight by $O(\log n)$ rounds of local computation, each vertex acting only on its own $Q$-neighbourhood. This matters for fault tolerance, where decoding latency is a bottleneck. The milestones carry independent value. Theorem 9 is a linear minimum distance bound for quantum Tanner codes in the quadripartite setting. Theorem 12 is the local-to-global "weight reduction" principle on which both decoders rest. Lemmas 4–5 are spectral facts about Cayley graphs and square complexes that are reusable for any expander-based code.

The paper's results are proved, not open; none has been machine-checked. The sequential decoder's correctness (Theorem 13) is posed separately on the platform as an open goal in the mission Decoding quantum Tanner codes (Leverrier, Zemor), which shares this mission's published definitions; this mission does not restate it. Formalizing the present chain would give a complete, checked proof that a parallel decoder exists for good quantum LDPC codes, and would expose the constants. Two printed constants are corrected here (see the scope section), and sharper constants or simpler arguments are welcome.

Difficulty

The obvious argument is to bound the mismatch and its norm, apply Theorem 12 repeatedly, and let all vertices of a class flip at once. That argument fails because parallel flips are not sequential flips. A vertex's best local move against the mismatch at its turn need not be the move a converging sequential run would make, and a round could stall even though a sequential run never does. Lemma 18 resolves this with a virtual sequential run, a partition of its increments into "good" and "bad" ones (Claim 1), and the maximum-weight rule at every vertex. Without that rule the lemma is false. Theorem 12 itself is a counting contradiction. It uses robustness, the expander mixing lemma twice, and two notions of "exceptional" vertices, and it needs $\Delta$ large. Theorem 9 needs the coset-minimization of Lemma 7 before the same counting can start.

Formalization scope

The development builds on the published layers QAlgorithms_Defs_TensorCode and QAlgorithms_Defs_TannerDecoder. These define the complex, $\varphi_v$, $\mathcal C_0$, $\mathcal C_1$, the $\sigma_x$ span, minimum local corrections, the mismatch, Algorithm 2 and the output $\hat e$. The conventions are:

• A vertex $(g,ij)$ is (g, (i, j)) : G × (Bool × Bool), squares are G × A × B, and weights are hammingNorm cast to ℝ.
• One new definitions file holds Algorithm 3 (admissible move, parallel choice, substep, round, run), decompositions and their norm, active, exceptional and ordinary vertices, the clustering sets $T$, stalled and converging sequential decoders, $\mathcal C_1^\perp$, and the square graphs $\mathcal G^\square_k$.
• "$\Delta$ large enough" is $\exists\Delta_0\,\forall\Delta\ge\Delta_0$, with $\Delta_0$ depending only on the constants fixed before it.
• Only $\sigma_x$-type errors are treated; the $\sigma_z$ case is symmetric.
• Non-bipartiteness of the Cayley graphs (the standing choice of p. 10) is assumed wherever spectral bounds are used.
• Theorem 12 assumes $Z\ne0$ and asks for a non-zero $x_v$.

Corrected constants. Theorem 9 is stated with $1024$ instead of the printed $256$, because Lemma 8 and the proof's $|x|\ge\frac{\kappa\Delta}2\|x\|$ give $1024$. The goal's error bound uses $\min(\varepsilon^3/16,\kappa/4)$ instead of $\min(\varepsilon^3/16,\kappa)$, which is what the corrected distance supports. Both corrected statements are weaker than the printed ones.

No trivialization. Every vertex must flip a maximum-weight admissible move whenever one exists, and runs range over all such choices. "Logarithmic time" is the per-round contraction factor, not mere eventual termination. Validity is membership of $e+\hat e$ in the $\sigma_x$-generator span, with $\hat e$ the paper's postprocessing output. A formalization that lets vertices idle, drops the maximum-weight rule, or proves only eventual termination does not prove this theorem.

Needed and reusable infrastructure:

• spectral graph theory for regular multigraphs (expander mixing, eigenvalues of commuting Cayley adjacencies);
• product expansion and local minimality of decompositions;
• the combinatorics of the left-right complex (shared rows and columns).

Contributions proving the graph lemmas or Lemma 18, whose proof is pure counting, are especially welcome.

Selected references

• A. Leverrier, G. Zémor, Decoding quantum Tanner codes, IEEE Transactions on Information Theory; arXiv:2208.05537v3, 2022. https://arxiv.org/abs/2208.05537
• A. Leverrier, G. Zémor, Quantum Tanner codes, FOCS 2022; arXiv:2202.13641. https://arxiv.org/abs/2202.13641
• P. Panteleev, G. Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, STOC 2022; arXiv:2111.03654. https://arxiv.org/abs/2111.03654
• S. Gu, C. A. Pattison, E. Tang, An efficient decoder for a linear distance quantum LDPC code, STOC 2023; arXiv:2206.06557. https://arxiv.org/abs/2206.06557
• A. Leverrier, G. Zémor, Efficient decoding up to a constant fraction of the code length for asymptotically good quantum codes, SODA 2023; arXiv:2206.07571. https://arxiv.org/abs/2206.07571
• I. Dinur, M.-H. Hsieh, T.-C. Lin, T. Vidick, Good quantum LDPC codes with linear time decoders, arXiv:2206.07750, 2022. https://arxiv.org/abs/2206.07750
• G. Kalachev, P. Panteleev, Two-sided robustly testable codes, arXiv:2206.09973, 2022. https://arxiv.org/abs/2206.09973

Motivation

NLTS Hamiltonians from good quantum codes establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Fix positive clustering constants $c_1,c_2,\delta_0$, a bound $s$ on the number of nonzero entries in each row and column of the binary check matrices, and a positive constant $B$ bounding the total number of checks by $Bn$. There exist $a>0$ and an integer $n_0\ge2$, uniform over the code, state, energy density and preparing circuit, with the following property.

For $n\ge n_0$, let $H_x\in\mathbb F_2^{m_x\times n}$ and $H_z\in\mathbb F_2^{m_z\times n}$ be check matrices with $m_x,m_z>0$, sparsity at most $s$, and $m_x+m_z\le Bn$. Put $C_x=\ker H_x$ and $C_z=\ker H_z$, and assume the CSS condition $C_x^\perp\subseteq C_z$. Write $k$ for the encoded dimension, and assume $k\ge2$. Assume Property 1: for every $0\le\delta<\delta_0$ and every $y\in\mathbb F_2^n$, $|H_z y|\le\delta m_z$ implies $|y|_{C_x^\perp}\le c_1\delta n$ or $|y|_{C_x^\perp}\ge c_2n$, and the same implication holds with $x,z$ interchanged. Here $|y|_S=\min_{v\in S}|y+v|$, and $|\cdot|$ is Hamming weight. Define the unnormalized check Hamiltonian $H=\sum_{w\text{ row of }H_x}(I-X^w)/2+\sum_{w\text{ row of }H_z}(I-Z^w)/2$, counting all supplied rows.

Define

$$E(C)=\frac{1}{400c_1}\frac{\min\{m_x,m_z\}}{n}\min\left\{\left(\frac{k-1}{4n}\right)^2,\delta_0,\frac{c_2}{2}\right\}.$$

The corrected permitted cutoff is

$$E_{\mathrm{eff}}(C)=\min\{E(C),\delta_0\min(m_x,m_z)/(400n)\}.$$

For every density matrix $\rho$ and every $0\le\epsilon<E_{\mathrm{eff}}(C)$,

$$\operatorname{tr}(H\rho)\le\epsilon n \quad\Longrightarrow\quad \operatorname{depth}(U)\ge a\log n$$

for every preparing circuit $U$. A preparing circuit consists of layers of disjoint arbitrary one- and two-qubit unitary gates on $n+w$ qubits, for any $w\ge0$, starts in $|0\rangle^{\otimes(n+w)}$, and has reduced output $\rho$ on the first $n$ qubits after discarding the other qubits. Depth is its number of layers; $\log$ is the natural logarithm.

Moreover, for every fixed $r,q>0$, there exist $e_*>0$ and $n_1\ge2$, uniform over all code instances, such that whenever $n\ge n_1$, $k\ge rn$ and $\min\{m_x,m_z\}\ge qn$, one has

$$k\ge2,\qquad E_{\mathrm{eff}}(C)\ge e_*.$$

Consequently the allowed energy density can be chosen as a positive constant for the constant-rate, linear-distance qLDPC families satisfying Property 1 considered in the paper. The distance parameter does not enter the displayed cutoff; the paper's footnote 3 notes that Property 1 at $\delta=0$ already implies linear distance.

This gives a depth obstruction for every low-energy density matrix, including mixed states, rather than only ground states.

Source correction. The paper prints only $\epsilon<E(C)$. Its proof uses Property 1 at $2\epsilon_1$ with $\epsilon_1=200n\epsilon/\min(m_x,m_z)$, so we also require $400n\epsilon<\delta_0\min(m_x,m_z)$. This is exactly the missing domain condition; it is automatic if $c_1\ge1$. No normalization $c_1\ge1$ is imposed, and the frozen printed cutoff is retained as the first entry of the minimum.

Correction to the printed source.

Printed: Theorem 5 permits eps < E(C), where E(C) is the printed energyCutoff, for arbitrary positive c1.

Corrected: Use eps < min(E(C), delta0min(mx,mz)/(400n)); give the eventual positive floor for this same minimum. No other hypothesis, constant, or conclusion is changed.

Reason: The source proof sets epsilon1=200neps/min(mx,mz) on p.3 and applies Property 1 at 2epsilon1 on p.4. Its domain is delta<delta0, but the printed cutoff only supplies 2c1epsilon1<delta0. The additional strict upper bound is exactly 2epsilon1<delta0. It is redundant for c1>=1 and retains every c1<1 instance satisfying the actual proof-domain condition.

Target

Theorem 5 (Formal statement of the NLTS theorem), §2

Fix positive clustering constants $c_1,c_2,\delta_0$, a bound $s$ on the number of nonzero entries in each row and column of the binary check matrices, and a positive constant $B$ bounding the total number of checks by $Bn$. There exist $a>0$ and an integer $n_0\ge2$, uniform over the code, state, energy density and preparing circuit, with the following property.

For $n\ge n_0$, let $H_x\in\mathbb F_2^{m_x\times n}$ and $H_z\in\mathbb F_2^{m_z\times n}$ be check matrices with $m_x,m_z>0$, sparsity at most $s$, and $m_x+m_z\le Bn$. Put $C_x=\ker H_x$ and $C_z=\ker H_z$, and assume the CSS condition $C_x^\perp\subseteq C_z$. Write $k$ for the encoded dimension, and assume $k\ge2$. Assume Property 1: for every $0\le\delta<\delta_0$ and every $y\in\mathbb F_2^n$, $|H_z y|\le\delta m_z$ implies $|y|_{C_x^\perp}\le c_1\delta n$ or $|y|_{C_x^\perp}\ge c_2n$, and the same implication holds with $x,z$ interchanged. Here $|y|_S=\min_{v\in S}|y+v|$, and $|\cdot|$ is Hamming weight. Define the unnormalized check Hamiltonian $H=\sum_{w\text{ row of }H_x}(I-X^w)/2+\sum_{w\text{ row of }H_z}(I-Z^w)/2$, counting all supplied rows.

Define

$$E(C)=\frac{1}{400c_1}\frac{\min\{m_x,m_z\}}{n}\min\left\{\left(\frac{k-1}{4n}\right)^2,\delta_0,\frac{c_2}{2}\right\}.$$

The corrected permitted cutoff is

$$E_{\mathrm{eff}}(C)=\min\{E(C),\delta_0\min(m_x,m_z)/(400n)\}.$$

For every density matrix $\rho$ and every $0\le\epsilon<E_{\mathrm{eff}}(C)$,

$$\operatorname{tr}(H\rho)\le\epsilon n \quad\Longrightarrow\quad \operatorname{depth}(U)\ge a\log n$$

for every preparing circuit $U$. A preparing circuit consists of layers of disjoint arbitrary one- and two-qubit unitary gates on $n+w$ qubits, for any $w\ge0$, starts in $|0\rangle^{\otimes(n+w)}$, and has reduced output $\rho$ on the first $n$ qubits after discarding the other qubits. Depth is its number of layers; $\log$ is the natural logarithm.

Moreover, for every fixed $r,q>0$, there exist $e_*>0$ and $n_1\ge2$, uniform over all code instances, such that whenever $n\ge n_1$, $k\ge rn$ and $\min\{m_x,m_z\}\ge qn$, one has

$$k\ge2,\qquad E_{\mathrm{eff}}(C)\ge e_*.$$

Consequently the allowed energy density can be chosen as a positive constant for the constant-rate, linear-distance qLDPC families satisfying Property 1 considered in the paper. The distance parameter does not enter the displayed cutoff; the paper's footnote 3 notes that Property 1 at $\delta=0$ already implies linear distance.

This gives a depth obstruction for every low-energy density matrix, including mixed states, rather than only ground states.

Source correction. The paper prints only $\epsilon<E(C)$. Its proof uses Property 1 at $2\epsilon_1$ with $\epsilon_1=200n\epsilon/\min(m_x,m_z)$, so we also require $400n\epsilon<\delta_0\min(m_x,m_z)$. This is exactly the missing domain condition; it is automatic if $c_1\ge1$. No normalization $c_1\ge1$ is imposed, and the frozen printed cutoff is retained as the first entry of the minimum.

Correction to the printed source.

Printed: Theorem 5 permits eps < E(C), where E(C) is the printed energyCutoff, for arbitrary positive c1.

Corrected: Use eps < min(E(C), delta0min(mx,mz)/(400n)); give the eventual positive floor for this same minimum. No other hypothesis, constant, or conclusion is changed.

Reason: The source proof sets epsilon1=200neps/min(mx,mz) on p.3 and applies Property 1 at 2epsilon1 on p.4. Its domain is delta<delta0, but the printed cutoff only supplies 2c1epsilon1<delta0. The additional strict upper bound is exactly 2epsilon1<delta0. It is redundant for c1>=1 and retains every c1<1 instance satisfying the actual proof-domain condition.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• NLTS Hamiltonians from good quantum codes, arXiv:2206.13228v4. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Additional independently reviewed proof targets

Theorem 1: No low-energy trivial states

There is a deterministically explicit family of binary CSS check descriptions on $n$ qubits, and constants $\epsilon,c,a,b>0$, a locality bound $s$, and a threshold $n_0\ge1$, all independent of $n$. Explicit means that a deterministic polynomial-time function on unary $n$ outputs the actual row counts and both binary check matrices. For every $n\ge1$, both check matrices have row and column weights at most $s$, their total row count $m_n$ satisfies $an\le m_n\le bn$, and their associated projector terms $h_i=(I-X^{w_i})/2$ or $(I-Z^{w_i})/2$ act on at most $s$ qubits, commute, and annihilate a common unit vector. Let $H_n=\sum_i h_i$ be this unnormalized Hamiltonian. Every circuit $P$ of parallel one- and two-qubit unitaries on disjoint wires, starting from zero qubits and allowing arbitrary clean ancillas and discarded qubits, has an output density operator $\rho_P$ satisfying, for $n\ge n_0$,

$$\operatorname{Tr}(H_n\rho_P)<\epsilon n \quad\Longrightarrow\quad \operatorname{depth}(P)\ge c\ln n.$$

This is the existence of an NLTS Hamiltonian family. Quantifying over every preparation circuit gives the lower bound for mixed as well as pure low-energy states.

Formalization Note The deterministic interpretation of explicit and the CSS witness implementation are recorded for independent moderation; the theorem does not assume an NLTS guarantee on its family.

Section 2: support of both measurement distributions

Let $H_X,H_Z$ be a binary CSS check presentation with $n,m_x,m_z>0$, and let $\rho$ be any density operator with $\operatorname{Tr}(H\rho)\le\epsilon n$, where $\epsilon\ge0$ and $H$ is the sum of the actual check projectors. Write $D_z,D_x$ for its standard- and product-Hadamard-basis distributions and $G_b^\delta$ for the words violating at most a $\delta$ fraction of the actual checks on side $b$. For every $\epsilon_1>0$,

$$D_z(G_z^{\epsilon_1})\ge1-\frac{\epsilon n}{\epsilon_1m_z}, \qquad D_x(G_x^{\epsilon_1})\ge1-\frac{\epsilon n}{\epsilon_1m_x}.$$

If $\epsilon=0$, both $G_z^0$ and $G_x^0$ have probability one. If $\epsilon>0$, choosing $\epsilon_1=200n\epsilon/\min(m_x,m_z)$ gives both masses at least $199/200$.

These bounds place low-energy measurement outcomes in the approximate classical codes. The energy identity and probability bounds are conclusions of the source argument, not hypotheses of the formal statement.

Section 2: equivalence classes and separated clusters

Let $C_X=\ker H_X$ and $C_Z=\ker H_Z$ be a binary CSS pair satisfying Property 1 with positive constants $c_1,c_2,\delta_0$. Assume $\epsilon_1\ge0$, $2\epsilon_1<\delta_0$, and $4c_1\epsilon_1<c_2$. On $G_z^{\epsilon_1}$ define $x\sim_z y$ when $|x+y|_{C_X^\perp}\le2c_1\epsilon_1n$, with the corresponding definition on $G_x^{\epsilon_1}$ modulo $C_Z^\perp$. Here $|v|_S=\min_{s\in S}|v+s|$. For either basis this is an equivalence relation. Its distinct computed classes are nonempty, pairwise disjoint, and cover the corresponding approximate code. Distinct classes satisfy

$$x\in B,\ y\in B',\ B\ne B'\quad\Longrightarrow\quad |x-y|\ge c_2n.$$

This constructs the separated clusters needed for the depth argument.

Formalization Note The strict domain follows Property 1 on page 2; the page-4 prose writes a non-strict endpoint. The classes are computed from the relation rather than supplied with a separation guarantee.

Correction to the printed source.

Printed: Page 4 says 'assuming 2 epsilon1 <= delta0', but Property 1 on page 2 is stated only for delta < delta0.

Corrected: Use 0 <= epsilon1 and the strict inequality 2 epsilon1 < delta0 in the clustering regime.

Reason: The proof invokes Property 1 at delta = 2 epsilon1; the strict domain is necessary. This is a standing-domain clarification pending independent moderation.

Lemma 2: one basis has no highly concentrated cluster

Consider a binary CSS presentation with $n,m_x,m_z>0$ and logical dimension $k\ge1$, satisfying Property 1 with $c_1,c_2,\delta_0>0$. Let $\rho$ be any density operator. Assume $\epsilon_1\ge0$, $2\epsilon_1<\delta_0$, $4c_1\epsilon_1<c_2$, and

$$2c_1\epsilon_1\le\left(\frac{k-1}{4n}\right)^2.$$

For the computed clusters in the preceding result, either every standard-basis cluster has $D_z$-mass strictly less than $99/100$, or every Hadamard-basis cluster has $D_x$-mass strictly less than $99/100$.

This uncertainty consequence selects a basis in which no single cluster captures almost all probability. It requires no low-energy hypothesis once the clusters are defined.

Formalization Note The subtraction $k-1$ takes place in the reals. The positive-$k$ reading comes from the section's positive-rate setting and is flagged for independent moderation.

Correction to the printed source.

Printed: The displayed finite lemma does not explicitly say k>=1, while Section 2 is introduced for constant-rate code families.

Corrected: State the finite lemma for k>=1 and n,mx,mz>0, keeping ((k-1)/(4n))^2 with real subtraction.

Reason: The proof uses a positive logical dimension; at k=0 the zero-radius clusters can concentrate in both bases. The finite positive-rate reading requires independent moderation.

Fact 3: uncertainty for subsets in conjugate bases

Let $\rho$ be any $n$-qubit density operator, and let $D_z,D_x$ be its standard- and product-Hadamard-basis measurement distributions. For all sets $S,T\subseteq\{0,1\}^n$,

$$D_x(T)\le2\sqrt{1-D_z(S)}+\frac{|S||T|}{2^n}.$$

This bounds concentration in conjugate bases and applies to mixed states. No positive-mass hypothesis on $S$ is required; empty sets and $n=0$ are allowed.

Section 2: positive-mass separated unions

Let a binary CSS presentation on $n>0$ qubits satisfy Property 1 with $c_1,c_2,\delta_0>0$, and assume $\epsilon_1\ge0$, $2\epsilon_1<\delta_0$, and $4c_1\epsilon_1<c_2$. Fix either basis and any density operator $\rho$. Suppose its measurement distribution $D$ gives the approximate-code set mass at least $199/200$, while each computed class has mass less than $99/100$. Then there are disjoint subcollections $M,M'$ of the computed classes whose unions $S,S'$ are disjoint and satisfy

$$D(S)\ge\frac1{400},\qquad D(S')\ge\frac1{400}, \qquad |x-y|\ge c_2n\quad(x\in S,\ y\in S').$$

This extracts two positive-mass separated sets in whichever basis Lemma 2 selects. Both probability constants and the cross-union separation are retained.

Fact 4: depth lower bound for well-spread distributions

Let $P$ be a circuit of depth $t$ consisting of layers of disjoint one- and two-qubit unitaries, starting in the all-zero product state. Allow any number of clean ancillas and measure only its $n>0$ output qubits in the standard basis, giving distribution $D$. Let $0<\mu<1$, and suppose $D(S),D(T)\ge\mu$. For any $u\ge0$ such that every $x\in S,y\in T$ has Hamming distance at least $u$,

$$u^2\le400n\ln(1/\mu)\,2^{3t}.$$

For positive set distance this is equivalently $t\ge\frac13\log_2(\operatorname{dist}(S,T)^2/(400n\ln(1/\mu)))$.

This is the quantitative circuit-depth obstruction for well-spread output distributions. The exponential formulation also covers overlapping sets without taking the logarithm of zero; the original circuit's workspace is unrestricted.

Lemma 8: expansion implies clustering

Let $A\in\mathbb F_2^{m\times n}$ and $V\subseteq\mathbb F_2^n$. Let $\delta>0$ and $0<\mu<\nu$. Suppose every $x\in V$ with $|x|\le\nu n$ satisfies $|Ax|\ge(\delta/\mu)|x|$. Then

$$x\in V,\quad |Ax|\le\delta n \quad\Longrightarrow\quad |x|\le\mu n\ \text{or}\ |x|\ge\nu n.$$

This transfers small-set expansion to the clustering dichotomy. Both the size cutoff and syndrome cutoff use the number of columns $n$, even for rectangular matrices.

Formalization Note Positivity is taken from the proof and the paragraph immediately following Lemma 8; the unsupported zero-$\delta$ extension is excluded.

Correction to the printed source.

Printed: The displayed Lemma 8 omits its parameter domain; its proof uses delta>0 and mu>0 and the following paragraph takes mu<nu.

Corrected: State Lemma 8 on the meaningful positive regime delta>0 and 0<mu<nu, as pinned by the plan and proof.

Reason: For delta=0, an expansion hypothesis with beta=0 supplies no information and the claimed nontrivial dichotomy can fail. Independent moderation must confirm the intended domain.

Section 3: minimal-representative expansion implies Property 1

Let $F$ be a family of binary CSS check presentations. Fix positive $\alpha_x,\beta_x,\alpha_z,\beta_z,\bar\delta,a,b$ and $n_0\ge1$. For all $n\ge n_0$, suppose $an\le m_x(n),m_z(n)\le bn$. For every $0\le\delta<\bar\delta$, define $V_z^\delta$ as the words in $G_z^\delta$ of minimum Hamming weight within their coset modulo $C_X^\perp$, and define $V_x^\delta$ analogously modulo $C_Z^\perp$. Assume $H_X$ is $(\alpha_x,\beta_x)$-expanding on $V_x^\delta$ and $H_Z$ is $(\alpha_z,\beta_z)$-expanding on $V_z^\delta$. Then there are constants $c_1,c_2,\delta_0>0$, independent of $n$, such that for all $n\ge n_0$ and $0\le\delta<\delta_0$,

$$y\in G_z^\delta\Longrightarrow |y|_{C_X^\perp}\le c_1\delta n\ \text{or}\ |y|_{C_X^\perp}\ge c_2n,$$

and the same dichotomy holds on the $X$ side modulo $C_Z^\perp$.

This derives Property 1 from uniform expansion of minimal representatives, without assuming the desired dichotomy. The check-density factors converting $\delta m_{\rm side}$ to a threshold relative to $n$ are retained.

These additional statements have current no-edit source review. Their formal proofs remain open; deferred results are excluded.