All missions

Motivation

Amplitude Estimation from Quantum Signal Processing establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $a\in[0,1]$ be an unknown amplitude in the completed two-dimensional Grover space. Choose an orthonormal pair $|\Pi\rangle,|\Pi^\perp\rangle$, set $\bar a=\sqrt{1-a^2}$, and write $|\psi\rangle=a|\Pi\rangle+\bar a|\Pi^\perp\rangle$ and $|\psi^\perp\rangle=\bar a|\Pi\rangle-a|\Pi^\perp\rangle$. The endpoint states are understood as rays. Define $Z_\psi=|\psi\rangle\langle\psi|-|\psi^\perp\rangle\langle\psi^\perp|$ and $Z_\Pi=|\Pi\rangle\langle\Pi|-|\Pi^\perp\rangle\langle\Pi^\perp|$. A complex polynomial $P$ is Pellian if there is a polynomial $Q$ of the opposite fixed parity such that $|P(x)|^2+(1-x^2)|Q(x)|^2=1$ for every $x\in[-1,1]$. A real polynomial is semi-Pellian if it is the coefficientwise real part of a Pellian polynomial.

There is an absolute constant $C>0$ such that, for every Pellian or semi-Pellian polynomial $P$, an oracle instrument can be chosen independently of $a$ and of the orthonormal basis. Given one copy of any of the four states and its known classical label, the instrument outputs a bit $b_P$ satisfying

$$\Pr[b_P=1]=|P(a)|^2.$$

It also returns a classical label $L$ for a retained signal state. For each joint outcome $(b_P,L)$ of probability $p$, the unnormalized signal density matrix is exactly $p|L\rangle\langle L|$, with $L\in\{\psi,\psi^\perp,\Pi,\Pi^\perp\}$. This includes both sampled-bit outcomes. The total number of oracle calls, including the oracle-assisted final basis measurement, is at most $C(\deg P+1)$ for every input label. Pellian sampling uses arbitrary-angle rotations $e^{i\phi Z_\psi},e^{i\phi Z_\Pi}$, with the controlled measurement access used in the proof. Semi-Pellian sampling uses the distinct primitives $|0\rangle\langle0|\otimes e^{i\phi Z}+|1\rangle\langle1|\otimes e^{-i\phi Z}$ for each basis. Ancilla preparation and known ancilla gates are free in this query model.

The retained-state guarantee allows successive polynomial samples from the same signal system, without requiring that each invocation restore the original state.

Formalization Note The completed Grover-space model includes $a=0,1$ and uses density matrices to ignore global phase. The asymptotic query claim is expressed with a uniform additive degree-zero allowance. Controlled access for the Pellian basis measurement is the operational convention of the source's proof; it is not derived from a strictly uncontrolled black box.

Target

§1.4, Theorem 6, equation (39)

Let $a\in[0,1]$ be an unknown amplitude in the completed two-dimensional Grover space. Choose an orthonormal pair $|\Pi\rangle,|\Pi^\perp\rangle$, set $\bar a=\sqrt{1-a^2}$, and write $|\psi\rangle=a|\Pi\rangle+\bar a|\Pi^\perp\rangle$ and $|\psi^\perp\rangle=\bar a|\Pi\rangle-a|\Pi^\perp\rangle$. The endpoint states are understood as rays. Define $Z_\psi=|\psi\rangle\langle\psi|-|\psi^\perp\rangle\langle\psi^\perp|$ and $Z_\Pi=|\Pi\rangle\langle\Pi|-|\Pi^\perp\rangle\langle\Pi^\perp|$. A complex polynomial $P$ is Pellian if there is a polynomial $Q$ of the opposite fixed parity such that $|P(x)|^2+(1-x^2)|Q(x)|^2=1$ for every $x\in[-1,1]$. A real polynomial is semi-Pellian if it is the coefficientwise real part of a Pellian polynomial.

There is an absolute constant $C>0$ such that, for every Pellian or semi-Pellian polynomial $P$, an oracle instrument can be chosen independently of $a$ and of the orthonormal basis. Given one copy of any of the four states and its known classical label, the instrument outputs a bit $b_P$ satisfying

$$\Pr[b_P=1]=|P(a)|^2.$$

It also returns a classical label $L$ for a retained signal state. For each joint outcome $(b_P,L)$ of probability $p$, the unnormalized signal density matrix is exactly $p|L\rangle\langle L|$, with $L\in\{\psi,\psi^\perp,\Pi,\Pi^\perp\}$. This includes both sampled-bit outcomes. The total number of oracle calls, including the oracle-assisted final basis measurement, is at most $C(\deg P+1)$ for every input label. Pellian sampling uses arbitrary-angle rotations $e^{i\phi Z_\psi},e^{i\phi Z_\Pi}$, with the controlled measurement access used in the proof. Semi-Pellian sampling uses the distinct primitives $|0\rangle\langle0|\otimes e^{i\phi Z}+|1\rangle\langle1|\otimes e^{-i\phi Z}$ for each basis. Ancilla preparation and known ancilla gates are free in this query model.

The retained-state guarantee allows successive polynomial samples from the same signal system, without requiring that each invocation restore the original state.

Formalization Note The completed Grover-space model includes $a=0,1$ and uses density matrices to ignore global phase. The asymptotic query claim is expressed with a uniform additive degree-zero allowance. Controlled access for the Pellian basis measurement is the operational convention of the source's proof; it is not derived from a strictly uncontrolled black box.

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

• Amplitude Estimation from Quantum Signal Processing, arXiv:2207.08628v3. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Single-shot decoding of good quantum LDPC codes establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Fix code parameters $\rho,d_r,\kappa\in(0,1)$ and decoder parameters $0<2\delta<\varepsilon<1$. For all sufficiently large degrees $\Delta$ (with the threshold depending only on these fixed parameters), let $G$ be a finite group with symmetric generating sets $A,B$ of size $\Delta$, whose left and right Cayley graphs are Ramanujan in the paper's sense: their second largest adjacency eigenvalue is at most $2\sqrt{\Delta-1}$. Let the binary local codes $C_A,C_B$ have exact rates $\rho,1-\rho$, respectively. Each of $C_A,C_B,C_A^\perp,C_B^\perp$ has distance at least $d_r\Delta$, and both dual tensor codes $C_A\boxplus C_B$ and $C_A^\perp\boxplus C_B^\perp$ are $\kappa$-product-expanding.

Construct the quadripartite quantum Tanner code on $Q=G\times A\times B$, with $n=|G|\Delta^2$ qubits, X checks from $C_A\otimes C_B$ at $V_{00}\cup V_{11}$ and Z checks from $C_A^\perp\otimes C_B^\perp$ at $V_{01}\cup V_{10}$. Let $d$ be its actual CSS distance. Let $e\in\mathbb F_2^Q$ be an X error and $D$ a binary error on the vertex-labelled Z checks. Write $|e|_R=\min_{s\in C_X^\perp}|e+s|$ and let $|D|_V$ count vertices with at least one nonzero syndrome-error bit. Define

$$A_\varepsilon=\frac{24}{\kappa\Delta(1-\varepsilon)},\quad B_\varepsilon=\frac{3\Delta}{\kappa(1-\varepsilon)},\quad C_\delta=\frac{d_r^2\delta^3\kappa}{2^{12}\Delta^2},\quad c_1=\frac{\varepsilon-2\delta}{\varepsilon(1-\delta)},\quad c_2=\frac2\varepsilon.$$

If

$$A_\varepsilon|e|_R+B_\varepsilon|D|_V\le\min(C_\delta n,d/\Delta),$$

then Algorithm 1, receiving only $\widetilde\sigma=H_Ze+D$ and parameter $\varepsilon$, terminates and every lawful output $\widehat f$ satisfies

$$|e+\widehat f|_R\le\left(1+\frac{2c_2}{\kappa c_1}\right)\Delta^2|D|_V.$$

Local minimum-weight choices are fixed consistently before the input; infeasible local syndromes use the zero fallback. Algorithm 2 starts with zero accumulators, uses the stated weight-decrease test and minimum column/row decomposition, and halts only at zero mismatch or when no permitted move exists. Algorithm 1 returns $\sum_{v\in V_{01}}\widetilde\varepsilon_v+\widehat C_1+\widehat R_0$.

This is the quantitative adversarial single-shot guarantee for the sequential Tanner decoder. With $D=0$, the residual is a stabilizer, rather than necessarily the zero vector.

Formalization Note The printed theorem leaves decoder domains implicit; the range above is inherited from pp.14 and 22. The distance is an extended natural minimum; when both logical-error sets are empty it is infinite, and the threshold uses only $C_\delta n$. Termination is represented by existence of a terminal execution together with the bound for every lawful terminal execution. No stochastic residual support law is asserted.

Target

Theorem 4.17 (Main Theorem for the Sequential Decoder)

Fix code parameters $\rho,d_r,\kappa\in(0,1)$ and decoder parameters $0<2\delta<\varepsilon<1$. For all sufficiently large degrees $\Delta$ (with the threshold depending only on these fixed parameters), let $G$ be a finite group with symmetric generating sets $A,B$ of size $\Delta$, whose left and right Cayley graphs are Ramanujan in the paper's sense: their second largest adjacency eigenvalue is at most $2\sqrt{\Delta-1}$. Let the binary local codes $C_A,C_B$ have exact rates $\rho,1-\rho$, respectively. Each of $C_A,C_B,C_A^\perp,C_B^\perp$ has distance at least $d_r\Delta$, and both dual tensor codes $C_A\boxplus C_B$ and $C_A^\perp\boxplus C_B^\perp$ are $\kappa$-product-expanding.

Construct the quadripartite quantum Tanner code on $Q=G\times A\times B$, with $n=|G|\Delta^2$ qubits, X checks from $C_A\otimes C_B$ at $V_{00}\cup V_{11}$ and Z checks from $C_A^\perp\otimes C_B^\perp$ at $V_{01}\cup V_{10}$. Let $d$ be its actual CSS distance. Let $e\in\mathbb F_2^Q$ be an X error and $D$ a binary error on the vertex-labelled Z checks. Write $|e|_R=\min_{s\in C_X^\perp}|e+s|$ and let $|D|_V$ count vertices with at least one nonzero syndrome-error bit. Define

$$A_\varepsilon=\frac{24}{\kappa\Delta(1-\varepsilon)},\quad B_\varepsilon=\frac{3\Delta}{\kappa(1-\varepsilon)},\quad C_\delta=\frac{d_r^2\delta^3\kappa}{2^{12}\Delta^2},\quad c_1=\frac{\varepsilon-2\delta}{\varepsilon(1-\delta)},\quad c_2=\frac2\varepsilon.$$

If

$$A_\varepsilon|e|_R+B_\varepsilon|D|_V\le\min(C_\delta n,d/\Delta),$$

then Algorithm 1, receiving only $\widetilde\sigma=H_Ze+D$ and parameter $\varepsilon$, terminates and every lawful output $\widehat f$ satisfies

$$|e+\widehat f|_R\le\left(1+\frac{2c_2}{\kappa c_1}\right)\Delta^2|D|_V.$$

Local minimum-weight choices are fixed consistently before the input; infeasible local syndromes use the zero fallback. Algorithm 2 starts with zero accumulators, uses the stated weight-decrease test and minimum column/row decomposition, and halts only at zero mismatch or when no permitted move exists. Algorithm 1 returns $\sum_{v\in V_{01}}\widetilde\varepsilon_v+\widehat C_1+\widehat R_0$.

This is the quantitative adversarial single-shot guarantee for the sequential Tanner decoder. With $D=0$, the residual is a stabilizer, rather than necessarily the zero vector.

Formalization Note The printed theorem leaves decoder domains implicit; the range above is inherited from pp.14 and 22. The distance is an extended natural minimum; when both logical-error sets are empty it is infinite, and the threshold uses only $C_\delta n$. Termination is represented by existence of a terminal execution together with the bound for every lawful terminal execution. No stochastic residual support law is asserted.

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

• Single-shot decoding of good quantum LDPC codes, arXiv:2306.12470v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Fast Estimation of Sparse Quantum Noise establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Fix a sparsity exponent $0<\delta<1/2$. There are positive constants $C,c,\beta$ and a threshold $n_0\ge1$, depending only on this fixed exponent and public design/code choices, and a public construction of the subsampling and peeling protocol for every $n\ge n_0$ and integer $s=4^{\delta n}$.

The labels of the $N=4^n$ phase-free $n$-qubit Paulis are $a=(a_x,a_z)\in\mathbb F_2^{2n}$. Let $K$ be uniform among the size-$s$ subsets of these labels. For each possible $K$, assign arbitrary nonnegative rates $p^{(K)}$ with total mass one, support exactly $K$, and $p^{(K)}_a\ge\epsilon_0>0$ on $K$. This assignment is independent of the protocol's public randomness and observation noise. The associated channel is $\mathcal E(\rho)=\sum_a p_aP_a\rho P_a$, and its eigenvalues are

$$\lambda_a=\sum_b(-1)^{a_x\cdot b_z+a_z\cdot b_x}p_b.$$

The observed eigenvalue vector has independent centered Gaussian errors of variance $\xi^2$, with $\xi\ge0$, independent of the support and the public design. Repeated reads use the same indexed observation and are counted as queries.

The construction chooses $B=2^b$ bins with $s\le B\le Cs$, constantly many subsampling groups, and $P_1,P_2=\Theta(n)$ offsets. Random offsets and binary hash matrices are sampled independently and uniformly before the hidden input. Coded offsets use a full-rank binary linear code with positive constant relative distance and a public, query-free, linear-time decoder. The decoder's realization, correction property and time bound are conclusions of the construction. Assume

$$\xi^2\le\min\!\left(\frac{B}{s^2},1\right), \qquad \epsilon_0\ge\frac{2\xi}{\sqrt B}.$$

Algorithms 2–4 produce a list of distinct labels with support exactly $K$ and estimated rates $\widehat p$, zero off the reported support, satisfying

$$\Pr\!\left[ \operatorname{supp}(\widehat p)=K \ \text{and}\ \|\widehat p-p\|_\infty\le\frac{2\xi}{\sqrt B} \right]\ge1-e^{-cn}.$$

The probability averages over the uniform support, public design, Gaussian observations, and any internal decoder randomness. Every execution uses at most $Csn$ eigenvalue reads and $Csn^2$ classical arithmetic/indexing instructions. The computed conditional success probabilities are measurable.

This result recovers both the locations and values of sparse Pauli errors from noisy eigenvalues. It does not assert a quantum measurement sample complexity.

Formalization Note The frozen, independently reviewed program composition is used directly. It separates the ordinary $b$-bit WHT from the symplectic $2n$-bit label pairing, resolves the printed dimensional inconsistencies as approved in the definition review, and retires peeled bins according to the graph description. The theorem does not assume successful bin detection, favorable graph events, accuracy, runtime, or independence of overlapping bin errors.

Target

Theorem 1; Assumptions 1, Algorithms 2–4

Fix a sparsity exponent $0<\delta<1/2$. There are positive constants $C,c,\beta$ and a threshold $n_0\ge1$, depending only on this fixed exponent and public design/code choices, and a public construction of the subsampling and peeling protocol for every $n\ge n_0$ and integer $s=4^{\delta n}$.

The labels of the $N=4^n$ phase-free $n$-qubit Paulis are $a=(a_x,a_z)\in\mathbb F_2^{2n}$. Let $K$ be uniform among the size-$s$ subsets of these labels. For each possible $K$, assign arbitrary nonnegative rates $p^{(K)}$ with total mass one, support exactly $K$, and $p^{(K)}_a\ge\epsilon_0>0$ on $K$. This assignment is independent of the protocol's public randomness and observation noise. The associated channel is $\mathcal E(\rho)=\sum_a p_aP_a\rho P_a$, and its eigenvalues are

$$\lambda_a=\sum_b(-1)^{a_x\cdot b_z+a_z\cdot b_x}p_b.$$

The observed eigenvalue vector has independent centered Gaussian errors of variance $\xi^2$, with $\xi\ge0$, independent of the support and the public design. Repeated reads use the same indexed observation and are counted as queries.

The construction chooses $B=2^b$ bins with $s\le B\le Cs$, constantly many subsampling groups, and $P_1,P_2=\Theta(n)$ offsets. Random offsets and binary hash matrices are sampled independently and uniformly before the hidden input. Coded offsets use a full-rank binary linear code with positive constant relative distance and a public, query-free, linear-time decoder. The decoder's realization, correction property and time bound are conclusions of the construction. Assume

$$\xi^2\le\min\!\left(\frac{B}{s^2},1\right), \qquad \epsilon_0\ge\frac{2\xi}{\sqrt B}.$$

Algorithms 2–4 produce a list of distinct labels with support exactly $K$ and estimated rates $\widehat p$, zero off the reported support, satisfying

$$\Pr\!\left[ \operatorname{supp}(\widehat p)=K \ \text{and}\ \|\widehat p-p\|_\infty\le\frac{2\xi}{\sqrt B} \right]\ge1-e^{-cn}.$$

The probability averages over the uniform support, public design, Gaussian observations, and any internal decoder randomness. Every execution uses at most $Csn$ eigenvalue reads and $Csn^2$ classical arithmetic/indexing instructions. The computed conditional success probabilities are measurable.

This result recovers both the locations and values of sparse Pauli errors from noisy eigenvalues. It does not assert a quantum measurement sample complexity.

Formalization Note The frozen, independently reviewed program composition is used directly. It separates the ordinary $b$-bit WHT from the symplectic $2n$-bit label pairing, resolves the printed dimensional inconsistencies as approved in the definition review, and retires peeled bins according to the graph description. The theorem does not assume successful bin detection, favorable graph events, accuracy, runtime, or independence of overlapping bin errors.

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

• Fast Estimation of Sparse Quantum Noise, arXiv:2007.07901v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Provably efficient machine learning for quantum many-body problems establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Fix a finite spatial dimension $d$, bounds on the number and geometric radius of sites in each Hamiltonian term, a local-term density bound $b_d+c_dr^d$, a spectral gap $\gamma>0$, an observable locality bound $q$, and a confidence parameter $\delta\in(0,1)$. Consider $n$-qubit Hamiltonians $H(x)=\sum_j h_j(x)$, smoothly parametrized by $x\in[-1,1]^m$. Each term is Hermitian, obeys $\|h_j(x)\|_\infty\le1$, and has directional derivative of operator norm at most one in every Euclidean unit parameter direction. These properties hold throughout the cube; smoothness at its boundary uses a local smooth extension. Every Hamiltonian has an excited energy and a gap at least $\gamma$ above its entire ground eigenspace. Let $\rho(x)$ be the normalized projector onto that eigenspace, allowing degeneracy.

For a fixed Hermitian observable $O=\sum_{i=1}^L O_i$, each term supported on at most $q$ qubits (not necessarily neighboring), choose a norm budget $B\ge1$ satisfying $\sum_i\|O_i\|_\infty\le B$. A smaller norm budget may be replaced by one. There are uniform positive constants, depending only on the fixed physical bounds, $q$, and $\delta$, such that for every fixed mean-squared error tolerance $\varepsilon\in(0,1]$ and all sufficiently large $m$, public sample counts, cutoffs, and actual classical arithmetic/RAM programs can be selected before the unknown Hamiltonian family, training draw, observable entries, and test parameter. The training set consists of $N$ independent uniform parameter draws, with one fresh-copy randomized Pauli snapshot $S_\ell$ at each point. Pauli axes are independently uniform; the joint measurement outcomes obey the Born law.

The named predictor is

$$\widehat{\sigma}_N(x)=\frac1N\sum_{\ell=1}^N\kappa_\Lambda(x,x_\ell)S_\ell,\qquad \kappa_\Lambda(x,y)=\sum_{\substack{k\in\mathbb Z^m\\\|k\|_2\le\Lambda}} \cos\!\bigl(\pi k\cdot(x-y)\bigr).$$

For each observable fixed before the training draw,

$$\Pr_{\mathcal T}\!\left[ \mathbb E_{x\sim\mathrm{Unif}[-1,1]^m} \left|\operatorname{tr}\!\left(O\widehat{\sigma}_N(x)\right) -\operatorname{tr}\!\left(O\rho(x)\right)\right|^2 \le\varepsilon\right]\ge1-\delta,$$

with $N\le C B^2m^{C B^2/\varepsilon}$ and computed classical training and prediction work $O((n+L)B^2m^{O(B^2/\varepsilon)})$. The compact representation stores $mN$ real parameter words and $nN$ six-valued labels, encodable in $3nN$ bits. The programs read and store those data and compute the observable value; they do not materialize the represented matrix. Ground-state preparation and data generation are excluded from this classical work.

For every fixed subsystem $A$ of at most $q$ qubits, separately with confidence at least $1-\delta$,

$$\mathbb E_x\left\|\operatorname{tr}_{A^{\mathrm c}} \bigl(\widehat{\sigma}_N(x)-\rho(x)\bigr)\right\|_1 \le\sqrt{4^q\varepsilon}.$$

Thus taking $\varepsilon=\eta^2/4^q$ gives the informal constant trace-norm error $\eta$ on a fixed few-body reduced matrix. This conversion uses the finite Pauli expansion and allocates confidence $\delta/4^q$ to its coefficients; it leaves the polynomial-in-$m$, linear-in-$n$ conclusion intact at fixed accuracy and locality.

This result describes generalization in population average for the source's compact shadow predictor. It asserts neither pointwise error nor simultaneous accuracy on all observables or subsystems, and does not require the predicted representation to be positive or trace one.

Formalization Note Theorem 3 on PDF pp.29–30 explicitly identifies itself as the detailed restatement of Theorem 1. Its Eq. (F3) prints exact ground-state labels, whereas its premise and Eqs. (2), (E3), and (F27) specify shadow labels; the latter determine the model above. This discrepancy and the nonperiodic-boundary gap in Lemma 2 are recorded for independent source moderation, without adding periodicity or a gradient bound as hypotheses.

Target

Theorem 1; detailed Theorem 3, PDF pp.29–30

Fix a finite spatial dimension $d$, bounds on the number and geometric radius of sites in each Hamiltonian term, a local-term density bound $b_d+c_dr^d$, a spectral gap $\gamma>0$, an observable locality bound $q$, and a confidence parameter $\delta\in(0,1)$. Consider $n$-qubit Hamiltonians $H(x)=\sum_j h_j(x)$, smoothly parametrized by $x\in[-1,1]^m$. Each term is Hermitian, obeys $\|h_j(x)\|_\infty\le1$, and has directional derivative of operator norm at most one in every Euclidean unit parameter direction. These properties hold throughout the cube; smoothness at its boundary uses a local smooth extension. Every Hamiltonian has an excited energy and a gap at least $\gamma$ above its entire ground eigenspace. Let $\rho(x)$ be the normalized projector onto that eigenspace, allowing degeneracy.

For a fixed Hermitian observable $O=\sum_{i=1}^L O_i$, each term supported on at most $q$ qubits (not necessarily neighboring), choose a norm budget $B\ge1$ satisfying $\sum_i\|O_i\|_\infty\le B$. A smaller norm budget may be replaced by one. There are uniform positive constants, depending only on the fixed physical bounds, $q$, and $\delta$, such that for every fixed mean-squared error tolerance $\varepsilon\in(0,1]$ and all sufficiently large $m$, public sample counts, cutoffs, and actual classical arithmetic/RAM programs can be selected before the unknown Hamiltonian family, training draw, observable entries, and test parameter. The training set consists of $N$ independent uniform parameter draws, with one fresh-copy randomized Pauli snapshot $S_\ell$ at each point. Pauli axes are independently uniform; the joint measurement outcomes obey the Born law.

The named predictor is

$$\widehat{\sigma}_N(x)=\frac1N\sum_{\ell=1}^N\kappa_\Lambda(x,x_\ell)S_\ell,\qquad \kappa_\Lambda(x,y)=\sum_{\substack{k\in\mathbb Z^m\\\|k\|_2\le\Lambda}} \cos\!\bigl(\pi k\cdot(x-y)\bigr).$$

For each observable fixed before the training draw,

$$\Pr_{\mathcal T}\!\left[ \mathbb E_{x\sim\mathrm{Unif}[-1,1]^m} \left|\operatorname{tr}\!\left(O\widehat{\sigma}_N(x)\right) -\operatorname{tr}\!\left(O\rho(x)\right)\right|^2 \le\varepsilon\right]\ge1-\delta,$$

with $N\le C B^2m^{C B^2/\varepsilon}$ and computed classical training and prediction work $O((n+L)B^2m^{O(B^2/\varepsilon)})$. The compact representation stores $mN$ real parameter words and $nN$ six-valued labels, encodable in $3nN$ bits. The programs read and store those data and compute the observable value; they do not materialize the represented matrix. Ground-state preparation and data generation are excluded from this classical work.

For every fixed subsystem $A$ of at most $q$ qubits, separately with confidence at least $1-\delta$,

$$\mathbb E_x\left\|\operatorname{tr}_{A^{\mathrm c}} \bigl(\widehat{\sigma}_N(x)-\rho(x)\bigr)\right\|_1 \le\sqrt{4^q\varepsilon}.$$

Thus taking $\varepsilon=\eta^2/4^q$ gives the informal constant trace-norm error $\eta$ on a fixed few-body reduced matrix. This conversion uses the finite Pauli expansion and allocates confidence $\delta/4^q$ to its coefficients; it leaves the polynomial-in-$m$, linear-in-$n$ conclusion intact at fixed accuracy and locality.

This result describes generalization in population average for the source's compact shadow predictor. It asserts neither pointwise error nor simultaneous accuracy on all observables or subsystems, and does not require the predicted representation to be positive or trace one.

Formalization Note Theorem 3 on PDF pp.29–30 explicitly identifies itself as the detailed restatement of Theorem 1. Its Eq. (F3) prints exact ground-state labels, whereas its premise and Eqs. (2), (E3), and (F27) specify shadow labels; the latter determine the model above. This discrepancy and the nonperiodic-boundary gap in Lemma 2 are recorded for independent source moderation, without adding periodicity or a gradient bound as hypotheses.

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

• Provably efficient machine learning for quantum many-body problems, arXiv:2106.12627v4. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Foundations for learning from noisy quantum experiments establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Fix a positive finite dimension $d$ and finite labelled sets $X,Y,Z,B$ of preparation actions, dynamics actions, measurement actions, and measurement outcomes. Let $\mathcal Q$ be any set of world models $W=(\{\rho_x\}_{x\in X},\{\mathcal E_y\}_{y\in Y},\{M_{zb}\}_{z\in Z,b\in B})$ on $\mathbb C^d$: every preparation is a density matrix, every dynamics action is a CPTP map, and each measurement is a POVM. The model class may be uncountable and may contain equivalent descriptions.

Suppose every $W\in\mathcal Q$ is universal: some preparation is pure; some finite collection of dynamics actions implements exact unitary channels whose representatives generate a dense subgroup of $\mathrm{SU}(d)$; and some measurement effect is not proportional to the identity. These witnessing actions and their physical descriptions are unknown and may vary between worlds. Mathematical inverses enter the generated subgroup; physical access to inverse actions is not assumed.

Then there exists a fixed family $(L_k)_{k\in\mathbb N}$ of finite classical experimental procedures, chosen before the unknown world. Each procedure adaptively chooses experiments that freshly prepare $\rho_x$, apply a finite word of the available dynamics actions, and measure one of the available POVMs. Its description output is denoted $\widehat W^{(k)}=(\{\widehat\rho_x^{(k)}\},\{\widehat{\mathcal E}_y^{(k)}\},\{\widehat M_{zb}^{(k)}\})$. For every $W\in\mathcal Q$, every $\epsilon>0$, and every $0<\delta<1$, there exists $k_0$ such that for all $k\ge k_0$ there is one unitary or anti-unitary gauge $\mathcal G$ satisfying

$$\begin{aligned} \Pr_W\!\left[\|\rho_x-\mathcal G(\widehat\rho_x^{(k)})\|_1\le\epsilon\right]&\ge1-\delta &&(x\in X),\\ \Pr_W\!\left[\|\mathcal E_y-\mathcal G\circ\widehat{\mathcal E}_y^{(k)}\circ\mathcal G^{-1}\|_\diamond\le\epsilon\right]&\ge1-\delta &&(y\in Y),\\ \Pr_W\!\left[\|M_{zb}-\mathcal G(\widehat M_{zb}^{(k)})\|_1\le\epsilon\right]&\ge1-\delta &&(z\in Z,\ b\in B). \end{aligned}$$

Here $\Pr_W$ is computed from the experimental outcome probabilities and internal classical randomization of $L_k$. A unitary gauge has the form $\mathcal G(A)=UAU^\dagger$; an anti-unitary gauge has the form $\mathcal G(A)=U\overline A U^\dagger$. The same gauge is fixed outside all three collections of probability clauses. Both norms are unhalved. The output estimates need not themselves be lawful quantum objects.

The result establishes learnability of all labelled operations from untrusted experiments under universality. It gives eventual accuracy for each world, with no uniform sample bound, polynomial complexity guarantee, or certified accuracy-based stopping rule.

Formalization Note The finite-action scope is explicit in Theorem D.1 (PDF p.21), although the main-text Theorem 2 does not explicitly restrict the action sets. The stage-indexed interpretation follows the precision-halving procedure in D.2 (p.23) and D.7 (p.33).

Target

Theorem 2; formal restatement Theorem D.1 (PDF p.21)

Fix a positive finite dimension $d$ and finite labelled sets $X,Y,Z,B$ of preparation actions, dynamics actions, measurement actions, and measurement outcomes. Let $\mathcal Q$ be any set of world models $W=(\{\rho_x\}_{x\in X},\{\mathcal E_y\}_{y\in Y},\{M_{zb}\}_{z\in Z,b\in B})$ on $\mathbb C^d$: every preparation is a density matrix, every dynamics action is a CPTP map, and each measurement is a POVM. The model class may be uncountable and may contain equivalent descriptions.

Suppose every $W\in\mathcal Q$ is universal: some preparation is pure; some finite collection of dynamics actions implements exact unitary channels whose representatives generate a dense subgroup of $\mathrm{SU}(d)$; and some measurement effect is not proportional to the identity. These witnessing actions and their physical descriptions are unknown and may vary between worlds. Mathematical inverses enter the generated subgroup; physical access to inverse actions is not assumed.

Then there exists a fixed family $(L_k)_{k\in\mathbb N}$ of finite classical experimental procedures, chosen before the unknown world. Each procedure adaptively chooses experiments that freshly prepare $\rho_x$, apply a finite word of the available dynamics actions, and measure one of the available POVMs. Its description output is denoted $\widehat W^{(k)}=(\{\widehat\rho_x^{(k)}\},\{\widehat{\mathcal E}_y^{(k)}\},\{\widehat M_{zb}^{(k)}\})$. For every $W\in\mathcal Q$, every $\epsilon>0$, and every $0<\delta<1$, there exists $k_0$ such that for all $k\ge k_0$ there is one unitary or anti-unitary gauge $\mathcal G$ satisfying

$$\begin{aligned} \Pr_W\!\left[\|\rho_x-\mathcal G(\widehat\rho_x^{(k)})\|_1\le\epsilon\right]&\ge1-\delta &&(x\in X),\\ \Pr_W\!\left[\|\mathcal E_y-\mathcal G\circ\widehat{\mathcal E}_y^{(k)}\circ\mathcal G^{-1}\|_\diamond\le\epsilon\right]&\ge1-\delta &&(y\in Y),\\ \Pr_W\!\left[\|M_{zb}-\mathcal G(\widehat M_{zb}^{(k)})\|_1\le\epsilon\right]&\ge1-\delta &&(z\in Z,\ b\in B). \end{aligned}$$

Here $\Pr_W$ is computed from the experimental outcome probabilities and internal classical randomization of $L_k$. A unitary gauge has the form $\mathcal G(A)=UAU^\dagger$; an anti-unitary gauge has the form $\mathcal G(A)=U\overline A U^\dagger$. The same gauge is fixed outside all three collections of probability clauses. Both norms are unhalved. The output estimates need not themselves be lawful quantum objects.

The result establishes learnability of all labelled operations from untrusted experiments under universality. It gives eventual accuracy for each world, with no uniform sample bound, polynomial complexity guarantee, or certified accuracy-based stopping rule.

Formalization Note The finite-action scope is explicit in Theorem D.1 (PDF p.21), although the main-text Theorem 2 does not explicitly restrict the action sets. The stage-indexed interpretation follows the precision-halving procedure in D.2 (p.23) and D.7 (p.33).

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

• Foundations for learning from noisy quantum experiments, arXiv:2204.13691v1. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Robust shadow estimation establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Consider Protocol 1 of Chen, Yu, Zeng and Flammia on $n\ge 1$ qubits, with Hilbert space dimension $d=2^n$. The same completely positive, trace-preserving noise channel $\Lambda$ acts after each ideal global Clifford gate; fixed computational-basis measurement noise is absorbed into $\Lambda$. Calibration perfectly prepares $|0\rangle^{\otimes n}$. The full Clifford group modulo global phase is sampled uniformly and calibration shots are independent and identically distributed.

Let $\varepsilon>0$ and $0<\delta\le 1$. Define the Z-basis average fidelity by $F_Z(\Lambda)=d^{-1}\sum_b\langle b|\Lambda(|b\rangle\langle b|)|b\rangle$, and suppose $F_Z(\Lambda)>1/d$. Set

$$A=\frac{(1+\varepsilon^2)(1+1/d)^2}{\varepsilon^2(F_Z(\Lambda)-1/d)^2}.$$

The printed sample scale in Theorem 7 is $R_{\rm printed}=136\ln(2/\delta)A$. Interpret its real-valued batch parameters operationally as positive integers $N\ge\lceil68A\rceil$ and $K\ge\lceil2\ln(2/\delta)\rceil$, with actual calibration count $R=NK$.

For each recorded ideal Clifford $U$ and noisy outcome $b$, compute $\widehat f^{(r)}=(d|\langle b|U(|0\rangle^{\otimes n})|^2-1)/(d-1)$. Let $\widehat f$ be the median of the $K$ means of batches of $N$ such scores. The estimated inverse sends an operator $X$ to $(\operatorname{Tr}X/d)I+\widehat f^{-1}(X-(\operatorname{Tr}X/d)I)$. Let $\widetilde{\mathcal M}(X)=\mathbb E_U[U^\dagger\mathcal M_Z(\Lambda(UXU^\dagger))U]$, where $\mathcal M_Z$ removes off-diagonal computational-basis entries, and let $O_0=O-(\operatorname{Tr}O/d)I$.

With probability at least $1-\delta$ over calibration records, $\widehat f\ne0$ and the subsequent single-shot retrieval expectation satisfies, simultaneously for every Hermitian observable $O$ and every density matrix $\rho$,

$$\left|\mathbb E_{U,b\mid\rho}[\operatorname{Tr}(O\widehat{\mathcal M}^{-1}(U^\dagger|b\rangle\langle b|U))]-\operatorname{Tr}(O\rho)\right| =\left|\operatorname{Tr}(O\widehat{\mathcal M}^{-1}\widetilde{\mathcal M}(\rho))-\operatorname{Tr}(O\rho)\right| \le\varepsilon\|O_0\|_\infty.$$

Here $\|\cdot\|_\infty$ is the operator norm, and the expectation is conditional on the calibration result. This guarantee controls the systematic, asymptotic bias of robust shadow retrieval; it applies to all observables and states on the same successful calibration event.

Formalization Note The statement retains the printed $1+\varepsilon^2$ factor. The source proof's substitution instead gives $(1+\varepsilon)^2$ from the stated variance bound; this discrepancy and the integer rounding interpretation remain subject to independent source moderation. The product of rounded batch parameters is not asserted to equal, or be bounded above by the ceiling of, the printed total scale. The frozen calibration probability law, overlap scores, median and retrieval expectation compute the named protocol directly.

Target

Theorem 7, Eqs. (B24)-(B25), Protocol 1

Consider Protocol 1 of Chen, Yu, Zeng and Flammia on $n\ge 1$ qubits, with Hilbert space dimension $d=2^n$. The same completely positive, trace-preserving noise channel $\Lambda$ acts after each ideal global Clifford gate; fixed computational-basis measurement noise is absorbed into $\Lambda$. Calibration perfectly prepares $|0\rangle^{\otimes n}$. The full Clifford group modulo global phase is sampled uniformly and calibration shots are independent and identically distributed.

Let $\varepsilon>0$ and $0<\delta\le 1$. Define the Z-basis average fidelity by $F_Z(\Lambda)=d^{-1}\sum_b\langle b|\Lambda(|b\rangle\langle b|)|b\rangle$, and suppose $F_Z(\Lambda)>1/d$. Set

$$A=\frac{(1+\varepsilon^2)(1+1/d)^2}{\varepsilon^2(F_Z(\Lambda)-1/d)^2}.$$

The printed sample scale in Theorem 7 is $R_{\rm printed}=136\ln(2/\delta)A$. Interpret its real-valued batch parameters operationally as positive integers $N\ge\lceil68A\rceil$ and $K\ge\lceil2\ln(2/\delta)\rceil$, with actual calibration count $R=NK$.

For each recorded ideal Clifford $U$ and noisy outcome $b$, compute $\widehat f^{(r)}=(d|\langle b|U(|0\rangle^{\otimes n})|^2-1)/(d-1)$. Let $\widehat f$ be the median of the $K$ means of batches of $N$ such scores. The estimated inverse sends an operator $X$ to $(\operatorname{Tr}X/d)I+\widehat f^{-1}(X-(\operatorname{Tr}X/d)I)$. Let $\widetilde{\mathcal M}(X)=\mathbb E_U[U^\dagger\mathcal M_Z(\Lambda(UXU^\dagger))U]$, where $\mathcal M_Z$ removes off-diagonal computational-basis entries, and let $O_0=O-(\operatorname{Tr}O/d)I$.

With probability at least $1-\delta$ over calibration records, $\widehat f\ne0$ and the subsequent single-shot retrieval expectation satisfies, simultaneously for every Hermitian observable $O$ and every density matrix $\rho$,

$$\left|\mathbb E_{U,b\mid\rho}[\operatorname{Tr}(O\widehat{\mathcal M}^{-1}(U^\dagger|b\rangle\langle b|U))]-\operatorname{Tr}(O\rho)\right| =\left|\operatorname{Tr}(O\widehat{\mathcal M}^{-1}\widetilde{\mathcal M}(\rho))-\operatorname{Tr}(O\rho)\right| \le\varepsilon\|O_0\|_\infty.$$

Here $\|\cdot\|_\infty$ is the operator norm, and the expectation is conditional on the calibration result. This guarantee controls the systematic, asymptotic bias of robust shadow retrieval; it applies to all observables and states on the same successful calibration event.

Formalization Note The statement retains the printed $1+\varepsilon^2$ factor. The source proof's substitution instead gives $(1+\varepsilon)^2$ from the stated variance bound; this discrepancy and the integer rounding interpretation remain subject to independent source moderation. The product of rounded batch parameters is not asserted to equal, or be bounded above by the ceiling of, the printed total scale. The frozen calibration probability law, overlap scores, median and retrieval expectation compute the named protocol directly.

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

• Robust shadow estimation, arXiv:2011.09636v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

A Grand Unification of Quantum Algorithms establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Fix a nonnegative integer $l$, put $d=2l+1$, and choose real phases $\phi_0,\ldots,\phi_{d-1}$. There are complex polynomials $P,Q$, depending only on these phases and $l$, with $\deg P\le d$, $\deg Q\le d-1$, and respective parities $d$ and $d-1$ modulo $2$, such that

$$|P(x)|^2+(1-x^2)|Q(x)|^2=1 \qquad\text{for every }x\in[-1,1].$$

For every finite quantum register, every pair of normalized pure states $|A_0\rangle,|B_0\rangle$ in that register, and every unitary $U$ with a real nonzero amplitude $a=\langle A_0|U|B_0\rangle$, define the available exact rank-one phase shifts $A_\phi=e^{i\phi|A_0\rangle\langle A_0|}$ and $B_\phi=e^{i\phi|B_0\rangle\langle B_0|}$ for real $\phi$. Then

$$\langle A_0|A_{\phi_0}\left[\prod_{k=1}^{l}U B_{\phi_{2k-1}}U^\dagger A_{\phi_{2k}}\right]U|B_0\rangle=P(a).$$

The product is written in increasing $k$ from left to right, and its rightmost $U$ acts first. Normalization and unitarity imply $a\in[-1,1]$; the endpoints $a=\pm1$ are allowed. Parity means $P(-x)=(-1)^dP(x)$ and $Q(-x)=(-1)^{d-1}Q(x)$.

This construction applies one uniform polynomial to a privileged transition amplitude and connects amplitude amplification with quantum signal processing.

Formalization Note The finite register is a Euclidean space over an arbitrary finite basis type. The frozen positive-sign rank-one phase shifts and sequence encode Eq. (13) exactly. The complementary polynomial is existentially quantified with $P$ before the register, states, unitary and amplitude. The zero polynomial is allowed as $Q$, including when $l=0$.

Target

Theorem 2 (Amplitude Amplification), Section II B, Eq. (13)

Fix a nonnegative integer $l$, put $d=2l+1$, and choose real phases $\phi_0,\ldots,\phi_{d-1}$. There are complex polynomials $P,Q$, depending only on these phases and $l$, with $\deg P\le d$, $\deg Q\le d-1$, and respective parities $d$ and $d-1$ modulo $2$, such that

$$|P(x)|^2+(1-x^2)|Q(x)|^2=1 \qquad\text{for every }x\in[-1,1].$$

For every finite quantum register, every pair of normalized pure states $|A_0\rangle,|B_0\rangle$ in that register, and every unitary $U$ with a real nonzero amplitude $a=\langle A_0|U|B_0\rangle$, define the available exact rank-one phase shifts $A_\phi=e^{i\phi|A_0\rangle\langle A_0|}$ and $B_\phi=e^{i\phi|B_0\rangle\langle B_0|}$ for real $\phi$. Then

$$\langle A_0|A_{\phi_0}\left[\prod_{k=1}^{l}U B_{\phi_{2k-1}}U^\dagger A_{\phi_{2k}}\right]U|B_0\rangle=P(a).$$

The product is written in increasing $k$ from left to right, and its rightmost $U$ acts first. Normalization and unitarity imply $a\in[-1,1]$; the endpoints $a=\pm1$ are allowed. Parity means $P(-x)=(-1)^dP(x)$ and $Q(-x)=(-1)^{d-1}Q(x)$.

This construction applies one uniform polynomial to a privileged transition amplitude and connects amplitude amplification with quantum signal processing.

Formalization Note The finite register is a Euclidean space over an arbitrary finite basis type. The frozen positive-sign rank-one phase shifts and sequence encode Eq. (13) exactly. The complementary polynomial is existentially quantified with $P$ before the register, states, unitary and amplitude. The zero polynomial is allowed as $Q$, including when $l=0$.

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

• A Grand Unification of Quantum Algorithms, arXiv:2105.02859v5. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Motivation

Quantum Expander Codes establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Fix positive integer degrees $\Delta_A,\Delta_B$ and positive real constants $\gamma_A,\delta_A,\gamma_B,\delta_B$, with $\delta_A,\delta_B<1/6$. There are a deterministic classical decoder, a constant $C>0$, and an integer $n_0$, all chosen before the graph sizes and inputs, with the following properties.

Let $G=(A\sqcup B,E)$ be any finite simple bipartite graph with $1\le n_B=|B|\le n_A=|A|$, left degree $\Delta_A$ and right degree $\Delta_B$. For every $S\subseteq A$ with $|S|\le\gamma_A n_A$, require $|\Gamma(S)|\ge(1-\delta_A)\Delta_A|S|$, where $\Gamma(S)$ denotes its neighboring vertices. Require the corresponding right expansion for every $S\subseteq B$ with $|S|\le\gamma_B n_B$.

Form the self hypergraph-product CSS code on the tagged coordinates $Q=(A\times A)\sqcup(B\times B)$, of length $n=n_A^2+n_B^2$. Write $H$ for the binary incidence matrix with rows $B$ and columns $A$, and set $H_X=[I_A\otimes H\mid H^{\mathsf T}\otimes I_B]$, $H_Z=[H\otimes I_A\mid I_B\otimes H^{\mathsf T}]$. Let $R_X$ and $R_Z$ be their respective binary row spaces.

On every syndrome input, the decoder terminates and realizes the Section 3 small-set-flip algorithm, treating the two components independently. Each step flips a nonempty subset of an opposite generator's support, strictly reduces syndrome weight, and maximizes the decrease divided by the number of flipped coordinates. The deterministic implementation fixes its choices among the finitely many tied candidates. A zero syndrome returns the accumulated correction; a nonzero syndrome with no improving flip returns failure. Whenever $n\ge n_0$, its total uniform-cost word-machine instruction count, together with the cost of loading its adjacency-list and syndrome input, is at most $Cn$.

For every binary error pair $e=(e_X,e_Z)$ on $Q$, let $w(e)$ count coordinates on which at least one component is nonzero. If

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

then on the exact syndrome $(H_Xe_X,H_Ze_Z)$ the decoder returns a correction $(c_X,c_Z)$ satisfying

$$c_X+e_X\in R_Z,\qquad c_Z+e_Z\in R_X.$$

Correctness holds at every admissible finite size. This is an exact adversarial decoding guarantee for the associated quantum code, with linear classical runtime when degrees are fixed.

Formalization Note The positive-degree, nonempty-part convention used in the paper's proof is explicit. Equation (6)'s mixed coordinate names are read as the supports of the $H_X$ rows fixed by Equation (1) and the incidence formulas. These source clarifications are disclosed for independent moderation; the strict threshold and all constants in it are unchanged. Runtime and realization are conclusions about an executable classical machine; no progress or minimum-distance assertion is a hypothesis.

Target

Theorem 2

Fix positive integer degrees $\Delta_A,\Delta_B$ and positive real constants $\gamma_A,\delta_A,\gamma_B,\delta_B$, with $\delta_A,\delta_B<1/6$. There are a deterministic classical decoder, a constant $C>0$, and an integer $n_0$, all chosen before the graph sizes and inputs, with the following properties.

Let $G=(A\sqcup B,E)$ be any finite simple bipartite graph with $1\le n_B=|B|\le n_A=|A|$, left degree $\Delta_A$ and right degree $\Delta_B$. For every $S\subseteq A$ with $|S|\le\gamma_A n_A$, require $|\Gamma(S)|\ge(1-\delta_A)\Delta_A|S|$, where $\Gamma(S)$ denotes its neighboring vertices. Require the corresponding right expansion for every $S\subseteq B$ with $|S|\le\gamma_B n_B$.

Form the self hypergraph-product CSS code on the tagged coordinates $Q=(A\times A)\sqcup(B\times B)$, of length $n=n_A^2+n_B^2$. Write $H$ for the binary incidence matrix with rows $B$ and columns $A$, and set $H_X=[I_A\otimes H\mid H^{\mathsf T}\otimes I_B]$, $H_Z=[H\otimes I_A\mid I_B\otimes H^{\mathsf T}]$. Let $R_X$ and $R_Z$ be their respective binary row spaces.

On every syndrome input, the decoder terminates and realizes the Section 3 small-set-flip algorithm, treating the two components independently. Each step flips a nonempty subset of an opposite generator's support, strictly reduces syndrome weight, and maximizes the decrease divided by the number of flipped coordinates. The deterministic implementation fixes its choices among the finitely many tied candidates. A zero syndrome returns the accumulated correction; a nonzero syndrome with no improving flip returns failure. Whenever $n\ge n_0$, its total uniform-cost word-machine instruction count, together with the cost of loading its adjacency-list and syndrome input, is at most $Cn$.

For every binary error pair $e=(e_X,e_Z)$ on $Q$, let $w(e)$ count coordinates on which at least one component is nonzero. If

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

then on the exact syndrome $(H_Xe_X,H_Ze_Z)$ the decoder returns a correction $(c_X,c_Z)$ satisfying

$$c_X+e_X\in R_Z,\qquad c_Z+e_Z\in R_X.$$

Correctness holds at every admissible finite size. This is an exact adversarial decoding guarantee for the associated quantum code, with linear classical runtime when degrees are fixed.

Formalization Note The positive-degree, nonempty-part convention used in the paper's proof is explicit. Equation (6)'s mixed coordinate names are read as the supports of the $H_X$ rows fixed by Equation (1) and the incidence formulas. These source clarifications are disclosed for independent moderation; the strict threshold and all constants in it are unchanged. Runtime and realization are conclusions about an executable classical machine; no progress or minimum-distance assertion is a hypothesis.

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

• Quantum Expander Codes, arXiv:1504.00822v1. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.