Value decomposition — approximating the value of a joint state by a sum of per-agent local values — is a staple of multi-agent dynamic programming and reinforcement learning, from index policies for restless bandits to modern MARL architectures, yet it is normally used without justification. Chen and Peng (arXiv:2506.02385) supply one. They show a multi-agent MDP admits an exact value decomposition precisely when its transition matrix is not entangled — a notion built in direct analogy with quantum entanglement — and then turn that qualitative characterisation into a quantitative one: a measure of Markov entanglement bounds the decomposition error in general. This mission formalizes that core theory. The goal is Theorem 6, the general N-agent bound in the occupancy-weighted norm; the milestones are the equivalence between separability and exact decomposition, the perturbation machinery that carries a one-step transition error into a value-function error, and the extensions to shared global state and shared rewards. The paper's restless-bandit application, which needs mean-field machinery of its own, is left to a second mission in the series.

Motivation

Whether the gravitational field must be quantized is a long-standing foundational question. A well-known family of arguments tries to settle it by consistency alone: if a classical field were coupled to a quantum system, some basic principle — momentum conservation, the uncertainty relations, or the impossibility of superluminal signalling — would allegedly be violated. The two best-known versions are the gedanken experiment of Eppley and Hannah (1977) and the measurement-theoretic argument of DeWitt (1962).

Albers, Kiefer and Reginatto (Phys. Rev. D 78, 064051 (2008)) re-examine both arguments. Their paper is largely conceptual, but several of its steps are precise, checkable mathematical claims. This mission collects those claims and makes them machine-checkable.

Timeline.

• 1962 — DeWitt's measurement analysis of the gravitational field, using Peierls brackets and a "universal principle" for apparatus uncertainties.
• 1977 — Eppley and Hannah's gedanken experiment: a classical gravitational wave scattered off a quantum particle would imply momentum non-conservation, a violation of the uncertainty principle, or superluminal signalling.
• 2008 — Albers, Kiefer and Reginatto argue that neither gedanken experiment forces quantization, and exhibit a consistent hybrid classical–quantum model.

Setting

Photon pair and detector (Sec. II). Each photon carries a polarization qubit with orthonormal basis $|\uparrow\rangle$ (horizontal) and $|\downarrow\rangle$ (vertical). A detector with state space $\mathcal H$ (an arbitrary complex inner-product space) is coupled to photon 1. Before the measurement the joint state of photon 1, photon 2 and the detector is

and after the detector has measured photon 1 it is

The reduced density operator of photon 2 is obtained from $|\Psi\rangle\langle\Psi|$ by tracing out photon 1 and the detector; the paper asserts that for both states it equals

Mass cube and gravitational wave (Sec. III B). The disturbance $\delta T^{\mathrm{GW}}_{00}$ of the averaged energy density of the scattered wave depends on the cube's edge length $a$ and speed $v$, with sensitivities $T_a = \partial\,\delta T^{\mathrm{GW}}_{00}/\partial a$ and $T_v = \partial\,\delta T^{\mathrm{GW}}_{00}/\partial v$. With $\Delta a \approx \Delta x$ and $\Delta v \gtrsim \hbar/(2m\Delta x)$ the uncertainty $\Delta T^{\mathrm{GW}}_{00} = \sqrt{(T_a\Delta a)^2 + (T_v\Delta v)^2}$ has a strictly positive lower bound.

DeWitt's argument (Sec. V). A system observable $s$ reconstructed from apparatus data has uncertainty $\Delta s^2 = \Delta A^2/g^2 + g^2(\Delta D_\Omega s)^2$, where $g$ is the coupling constant.

Formalization targets

Goal — no signalling through photon 2 (Eq. (3))

For all unit vectors $\Phi_0, \Phi_\uparrow, \Phi_\downarrow \in \mathcal H$,

Milestones

1. Eq. (1) ⇒ (3): $\rho_2(\Psi_0) = \hat\rho$.
2. Eq. (2) ⇒ (3): $\rho_2(\Psi) = \hat\rho$.
3. Sec. III B lower bound: $\Delta T^{\mathrm{GW}}_{00} \ge \sqrt{\tfrac{\hbar}{m} T_v T_a}$ whenever $\Delta x > 0$ and $\Delta v \ge \hbar/(2m\Delta x)$.
4. Sec. III B optimum: the function $\Delta x \mapsto \sqrt{(T_a\Delta x)^2 + (T_v\hbar/(2m\Delta x))^2}$ attains its minimum over $\Delta x>0$ at $\Delta x_{\min} = \sqrt{\tfrac{\hbar}{2m}\tfrac{T_v}{T_a}}$, with value $\sqrt{\tfrac{\hbar}{m}T_vT_a}$.
5. Eq. (61): $\min_{g\ne0}\sqrt{\Delta A^2/g^2 + g^2\Delta D^2} = \sqrt{2\,\Delta A\,\Delta D}$.
6. Eq. (64): if $\Delta A\,\Delta C \ge \hbar/2$ then $\sqrt{\hbar\,|D_s s|} \le \sqrt{2\,\Delta A\,\Delta C\,|D_s s|}$.

Significance

The goal is the precise content of the paper's rebuttal of the superluminal-signalling branch of the Eppley–Hannah argument: the state of photon 2 accessible to a probe (such as a classical gravitational wave) is the same whether or not photon 1 has been measured, so a probe of photon 2 alone cannot tell whether photon 1 was measured. Milestones 3–6 are the quantitative estimates the paper uses in Sec. III B (a coupling to a test body obeying the uncertainty principle transfers a minimum uncertainty to the classical wave) and Sec. V (DeWitt's limitation on a single observable, Eq. (64)).

The results are elementary once stated; the value of the mission is to pin the paper's claims down exactly, including the hypotheses under which they hold. None of the statements has, to our knowledge, a machine-checked proof on the platform.

Difficulty

The goal and Milestones 1–2 need a workable representation of the partial trace over a factor that is an arbitrary (possibly infinite-dimensional) inner-product space; the cross terms between the two branches vanish because the two branches are orthogonal on photon 1, not because of any property of the detector states. Milestones 3–6 are single-variable optimization statements; the main care is in the side conditions (positivity, excluding $g=0$ and $\Delta x = 0$).

Formalization scope

• The joint space $\mathbb C^2\otimes\mathbb C^2\otimes\mathcal H$ is represented by functions $\{0,1\}\times\{0,1\}\to\mathcal H$ (component $\Psi_{ij}$ along $|i\rangle_1|j\rangle_2$; index $0 = \uparrow$, $1 = \downarrow$). The reduced density matrix of photon 2 has entries $\rho_2(j,j') = \sum_i \langle \Psi_{ij'}, \Psi_{ij}\rangle_{\mathcal H}$, and $\hat\rho$ is a $2\times2$ complex matrix.
• The detector states are only assumed to be unit vectors. Orthogonality of $|\Phi_\uparrow\rangle$ and $|\Phi_\downarrow\rangle$ (a physical property of a detector that records the outcome) is not assumed, because Eq. (3) does not depend on it.
• In Sec. III B the sensitivities $T_a, T_v$, the mass $m$ and $\hbar$ are positive reals; the paper's approximate relations $\Delta a\approx\Delta x$ and $\Delta p\gtrsim\hbar/\Delta x$ are encoded as $\Delta a = \Delta x$ and the hypothesis $\Delta v \ge \hbar/(2m\Delta x)$.
• In Eq. (61) the coupling constant ranges over all non-zero reals.
• Sections IV (hybrid classical–quantum ensembles for Nordström gravity) and the appendices are out of scope for this mission.

Selected references

• M. Albers, C. Kiefer, M. Reginatto, Measurement analysis and quantum gravity, Phys. Rev. D 78, 064051, 2008. https://doi.org/10.1103/PhysRevD.78.064051
• K. Eppley, E. Hannah, The necessity of quantizing the gravitational field, Found. Phys. 7, 51–68, 1977. https://doi.org/10.1007/BF00715241
• B. S. DeWitt, Definition of commutators via the uncertainty principle, J. Math. Phys. 3, 619, 1962. https://doi.org/10.1063/1.1724265

Motivation

The security of the RSA cryptosystem rests on the assumed difficulty of factoring large integers, and the best known classical algorithms for factoring run in super-polynomial time. In 1994 Peter Shor showed that a quantum computer can factor an $n$-digit integer in time polynomial in $n$ (Shor, SIAM J. Comput. 1997; conference version FOCS 1994). The algorithm has two parts. A classical reduction, due to Miller (1976), turns factoring into order finding: given $x$ coprime to $n$, find the least $r \ge 1$ with $x^r \equiv 1 \pmod n$. The quantum part solves order finding.

This mission formalizes the quantum part as Shor analyzes it in §5 of the journal paper: the construction of the quantum state, the probability of each measurement outcome, and the classical post-processing that reads $r$ off the measured value. The paper's claim is that one run of this procedure returns $r$ with probability at least $\varphi(r)/3r$.

Timeline:

• 1976: Miller reduces factoring to order finding (with randomization).
• 1985–1994: Deutsch, Bernstein–Vazirani and Simon give the quantum Fourier sampling ideas the algorithm builds on.
• 1994: Shor's FOCS paper introduces the factoring and discrete logarithm algorithms.
• 1997: the SIAM J. Comput. version gives the analysis formalized here, with $q$ the power of $2$ in $[n^2, 2n^2)$.

Setting

Fix an integer $n \ge 2$ and an integer $x$ coprime to $n$. Its order $r$ is the least $r \ge 1$ with $x^r \equiv 1 \pmod n$; since $x$ is a unit, $r \le \varphi(n) < n$. Let $q = 2^l$ be the power of $2$ with $n^2 \le q < 2n^2$.

A quantum state on two registers, the first holding $0 \le a < q$ and the second a residue $y \in \mathbb{Z}/n$, is a complex vector $\psi(a, y)$ indexed by the basis states $|a, y\rangle$. Measuring it returns $|a, y\rangle$ with probability $|\psi(a, y)|^2$.

The Fourier matrix $A_q$ is the $q \times q$ matrix with entries $(A_q)_{a,c} = q^{-1/2}\exp(2\pi i a c/q)$, with rows indexing inputs and columns outputs. The algorithm

1. prepares $\frac{1}{q^{1/2}}\sum_{a=0}^{q-1}|a\rangle|x^a \bmod n\rangle$ (eq. (5.2)),
2. applies $A_q$ to the first register, obtaining $\frac1q\sum_{a,c}\exp(2\pi iac/q)|c\rangle|x^a \bmod n\rangle$ (eq. (5.4)),
3. measures, obtaining some $|c, y\rangle$,
4. rounds $c/q$ to the nearest fraction with denominator smaller than $n$.

The observed $c$ gives us $r$ if some fraction with lowest-terms denominator below $n$ is within $1/2q$ of $c/q$, and every such fraction has lowest-terms denominator exactly $r$. In the Lean development these objects are preFourierState, finalState, outcomeProb and yieldsOrder, in the namespace ShorAlgorithms.OrderFinding, and the shared definition ShorAlgorithms.Shared.fourierMatrix.

Formalization targets

Goal: success probability at least $\varphi(r)/3r$

For all sufficiently large $n$, with $x$, $r$ and $q$ as above,

where $\Psi$ is the state (5.4). The threshold on $n$ is uniform in $x$ and $q$; it is the paper's "for sufficiently large $n$" from the per-state bound.

Milestones

1. Eqs. (5.5)–(5.6). For $0 \le k < r$, the probability of $|c, x^k\rangle$ equals $\left|\frac1q\sum_{b=0}^{\lfloor (q-k-1)/r\rfloor}\exp(2\pi i(br+k)c/q)\right|^2$.
2. Eq. (5.11). For $n$ past a threshold, every $|c, x^k\rangle$ with $-r/2 \le rc - dq \le r/2$ for some integer $d$ has probability at least $1/3r^2$.
3. Eq. (5.13). If $n^2 \le q$, at most one fraction with denominator below $n$ lies within $1/2q$ of $c/q$.
4. p. 1500. Such a fraction is a convergent of the continued fraction of $c/q$.
5. p. 1501. At least $\varphi(r)$ values of $c$ are within $1/2q$ of some $d/r$ with $\gcd(d, r) = 1$; with the $r$ distinct values of $x^k$ this gives at least $r\varphi(r)$ states $|c, x^k\rangle$, and each such $c$ gives us $r$.

Significance

The goal is the quantitative statement behind "order finding is in bounded-error quantum polynomial time": since $\varphi(r)/r \ge \delta/\log\log r$ for a constant $\delta$ (Hardy and Wright, Thm. 328), $O(\log\log r)$ repetitions find $r$ with high probability, and Miller's reduction then factors $n$. Without the bound, the algorithm is a procedure with no guarantee.

The result is proved, in the paper and in textbooks (Nielsen and Chuang, 2000, §5.3), usually with a phase-estimation analysis rather than Shor's direct count. What this mission adds is a machine-checked proof of Shor's own argument, with his choice of $q$ and his constants, starting from the state built by applying $A_q$ to (5.2). Formal proofs of idealized versions exist elsewhere, for instance in the exact-period model where $r$ divides $q$ and the output is uniform on $r$ peaks, but that model removes the approximation that the $1/3r^2$ bound is about. Legendre's theorem on continued fractions is already on the platform (FamousTheorems.legendre_continued_fraction_theorem) and is included as a reference item.

Difficulty

The obvious route is to compute the output distribution in closed form. That works only when $r$ divides $q$; here $q$ is a power of $2$ and $r$ is arbitrary, so the amplitudes are geometric sums of $\lfloor (q-k-1)/r\rfloor + 1$ terms whose phases do not cancel exactly. The per-state bound $1/3r^2$ requires a lower bound on such a sum that is uniform in $r$, $c$ and $k$, with error terms of order $1/q$ controlled against a main term of order $1/r^2$. The constant $1/3$ leaves only a small margin below the limiting value $4/\pi^2 \approx 0.405$, so the errors must be bounded explicitly, not merely shown to vanish.

The second difficulty is the counting: distinct coprime numerators $d$ must give distinct outcomes $c$ in $[0, q)$, and each good $c$ must determine $r$ uniquely, which uses $r < n$ and $n^2 \le q$.

Formalization scope

Conventions the statements commit to:

• States are functions Fin q × ZMod n → ℂ; the matrix convention is row = input, so applying $A_q$ to the first register gives the amplitude $\sum_a \psi(a, y)(A_q)_{a,c}$ at $(c, y)$.
• The final state is built by applying $A_q$ to the state (5.2); the closed forms (5.5) and (5.6) are theorems, not definitions. No normalization hypothesis is assumed.
• Probabilities are squared moduli; the probability of the event "$c$ gives us $r$" sums over all $y \in \mathbb{Z}/n$, which is exact because $y$ that are not powers of $x$ have probability zero.
• $x$ is a natural number with $\gcd(x, n) = 1$; $r$ is orderOf (x : ZMod n). $q$ enters through the three hypotheses $q = 2^l$, $n^2 \le q$, $q < 2n^2$, not through a function of $n$.
• Fractions are rationals, and "in lowest terms" is Rat.den.
• Thresholds "for sufficiently large $n$" are $\exists N,\ \forall n \ge N$, with $N$ quantified before $x$, $q$, $c$ and $k$.
• Condition (5.11) is stated in its equivalent form (5.12), with an integer $d$.
• Printed slip. Eq. (5.13)'s justification says "Because $q > n^2$", but $q$ was chosen with $n^2 \le q$, and $q = n^2$ when $n$ is a power of $2$. The uniqueness claim holds under $n^2 \le q$, and that is what is stated.

Typing the closed form (5.4)–(5.6) in as the definition of the final state would make milestone 1 trivial and hide whether the probability model is the paper's; the definitions exclude this by construction.

Not stated: the polynomial running time of any step, the $O(\log\log r)$ repetition count (no explicit constant), the reversible modular exponentiation of §3, and the post-processing heuristics on p. 1501. Needed infrastructure: bounds on geometric exponential sums, Euler's totient, Diophantine approximation by fractions with bounded denominator, and Mathlib's continued fractions. Lemmas on geometric sums of roots of unity and on the order of units mod $n$ are reusable in the companion discrete logarithm mission.

Selected references

• P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172
• P. W. Shor, Algorithms for quantum computation: discrete logarithms and factoring, Proc. 35th FOCS, 1994. https://doi.org/10.1109/SFCS.1994.365700
• G. L. Miller, Riemann's hypothesis and tests for primality, J. Comput. System Sci. 13(3):300–317, 1976. https://doi.org/10.1016/S0022-0000(76)80043-8
• G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 5th ed., Oxford, 1979 (Ch. X, continued fractions; Thm. 328).
• M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge, 2000. https://doi.org/10.1017/CBO9780511976667

Motivation

The spectral gap of a quantum many-body Hamiltonian is the difference between the energy of its ground state and the energy of its first excited state, in the limit of infinitely many particles. Whether a given microscopic interaction produces a gapped or a gapless system decides much of the macroscopic physics: gapped systems have exponentially decaying correlations and well-defined quantum phases, gapless systems sit at critical points and can display algebraically decaying correlations. Several long-standing questions — the Haldane conjecture for antiferromagnetic spin chains, the existence of gapped topological spin liquids, and the Yang–Mills mass gap — are instances of the question "given the interaction, is the system gapped?".

Cubitt, Pérez-García and Wolf proved that this question, posed for families of two-dimensional translationally invariant nearest-neighbour spin models, admits no algorithmic answer: the spectral gap problem is undecidable (Nature 528, 207–211 (2015); full version: Forum of Mathematics, Pi 10:e14 (2022), also arXiv:1502.04573).

Timeline of the ingredients the proof rests on: Turing's undecidability of the halting problem (1936); Berger's undecidability of the domino problem (1966) and Robinson's aperiodic tile set (Inventiones 12, 177–209 (1971)); Feynman's and Kitaev's circuit-to-Hamiltonian constructions, which turn a computation into a ground state; Gottesman and Irani's translationally invariant one-dimensional Hamiltonians encoding computation (FOCS 2009); and Bitansky–Vadhan-style quantum Turing machine engineering from Bernstein and Vazirani (SIAM J. Comput. 26, 1411–1473 (1997)). The 2015 result was later sharpened to one-dimensional chains by Bausch, Cubitt, Lucia and Pérez-García (PRX 10, 031038 (2020)).

Setting

Fix a local dimension $d$ and, for each side length $L$, the square lattice $\Lambda(L)=\{1,\dots,L\}^2$ with open boundary conditions. Each site carries a copy of $\mathbb{C}^d$, so the state space of the lattice has the standard product basis indexed by assignments of a level in $\{1,\dots,d\}$ to each site. A model is specified by three Hermitian matrices: an on-site term $h_1$ of size $d\times d$, and two interactions $h_{\mathrm{row}},h_{\mathrm{col}}$ of size $d^2\times d^2$ acting on horizontally and vertically adjacent pairs. The Hamiltonian of the finite lattice is

the same three matrices being used at every edge and every site, which is what translational invariance means here. The quantity $\max\{\|h_1\|,\|h_{\mathrm{row}}\|,\|h_{\mathrm{col}}\|\}$ is the local interaction strength.

Write $\lambda_0(H^{\Lambda(L)})\le\lambda_1(H^{\Lambda(L)})\le\cdots$ for the eigenvalues and $\Delta(H^{\Lambda(L)})=\lambda_1-\lambda_0$ for the finite-size gap. The family $\{H^{\Lambda(L)}\}_L$ is

• gapped (Definition 1 of the source) if there are $\gamma>0$ and $L_0$ such that for all $L>L_0$ the ground state of $H^{\Lambda(L)}$ is non-degenerate and $\Delta(H^{\Lambda(L)})\ge\gamma$;
• gapless (Definition 2 of the source) if there is $c>0$ such that for every $\varepsilon>0$ there is an $L_0$ with: for all $L>L_0$, every point of $[\lambda_0,\lambda_0+c]$ lies within $\varepsilon$ of the spectrum of $H^{\Lambda(L)}$.

These two conditions are not negations of each other; the construction guarantees that every instance falls into one of them. The ground state energy density is $E_\rho=\lim_{L\to\infty}\lambda_0(H^{\Lambda(L)})/L^2$.

Formalization targets

Goal — Theorem 3 of the source

For a fixed universal machine and every $n$, one explicit family of interactions, built from fixed integer-valued matrices $A,A',B,C,D,D'$, a diagonal projector $\Pi$, a rational $\beta>0$ that may be taken arbitrarily small, and an algebraic $\alpha(n)\le 2\beta$,

with $\varphi=\varphi(n)$ the rational whose binary expansion after the point is the binary expansion of $n$ reversed, satisfies: the local interaction strength is at most $1$; if the machine halts on input $n$ the family is gapped with gap at least $1$; and if it does not halt the family is gapless. Since halting is undecidable, no algorithm decides gappedness, even with the promise that exactly one of the two alternatives holds and even at fixed local dimension $d$.

Milestones

The milestone list follows the numbering of the full version: Lemma 8 and Theorem 9 (reduction of halting to ground state energy and to arbitrary low-energy properties), Corollary 7 (the same undecidability for unconstrained local dimension, with rational interactions), Proposition 53 and Corollary 54 (the diverging ground state energy and its promise version), and Theorem 5 (undecidability of the ground state energy density).

Significance

The result rules out a general algorithm — and therefore any complete general method — for deciding gappedness from the interaction matrices, however much computing power is available; the property genuinely depends on arbitrarily large system sizes. It also implies, via the standard link between undecidability and independence, that there are concrete finite-dimensional models whose gap is independent of the axioms of any consistent recursively axiomatized formal system (Corollary 4 of the source), and it transfers to other low-energy properties such as the existence of algebraically decaying ground-state correlations.

The theorem is proved; none of it is formalized. This mission produces the machine-checked version. The reusable infrastructure it forces into existence is substantial on its own: a formal model of translationally invariant lattice Hamiltonians and their thermodynamic-limit spectral behaviour, the tiling layer, and computational-history-state Hamiltonians. Each milestone is a self-contained statement that can be attacked without the others.

Difficulty

The obvious approach — encode a halting computation as an energy penalty — gives the ground state energy of a finite lattice, not a property of the limit; this is exactly what Lemma 8 achieves, and it is not enough, because a gap is a statement about the sequence of spectra as $L\to\infty$ and is insensitive to any single lattice size. The construction must make the halting information visible at all sufficiently large sizes at once while a fixed finite local dimension carries every instance $n$. That forces three separate difficulties: an aperiodic (Robinson) tiling to create squares of every size $2^n$ inside one translationally invariant model; a quantum phase-estimation Turing machine whose transition amplitudes encode $n$ in a single phase $e^{i\pi\varphi(n)}$, so that the instance index does not inflate the local dimension; and a history-state Hamiltonian whose low-energy spectrum can be controlled well enough that a positive energy density in the halting case turns into a genuine spectral gap, and a vanishing one into a dense spectrum above the ground state.

Formalization scope

The development commits to the following conventions, all of which are visible in the definition items of this mission.

1. Lattices are finite: sites are pairs of indices in $\{0,\dots,L-1\}$, edges are consecutive pairs within a row or a column (open boundary conditions; the periodic case of Section 6.3 of the source is out of scope).
2. Operators are complex matrices indexed by product-basis configurations; the interactions are embedded by acting as the given matrix on the two sites of an edge and as the identity elsewhere.
3. The spectrum is taken as the set of real numbers in the matrix spectrum, and $\lambda_0$ is its infimum; every statement carries the Hermiticity hypotheses that make this the usual spectrum. Multiplicities are dimensions of eigenspaces, which is how the "identity of spectra as multisets" of Theorem 9 is expressed.
4. Gapped, gapless and the energy density are properties of the whole family $\{H^{\Lambda(L)}\}_L$ generated by a fixed triple of matrices, exactly as in Definitions 1 and 2.
5. Operator norms are $\ell_2$ operator norms; the local interaction strength is the maximum of the three.
6. Machines are represented by partial recursive codes: "halts on input $n$" is definedness of the evaluation, and "has not halted after $L$ steps" is the step-bounded evaluation returning nothing. The explicit local-dimension bounds of Lemma 8 and Theorem 9, which are stated in the source in terms of the number of internal states and the alphabet size of a Turing machine, are replaced by the existence of a finite local dimension.

Degenerate readings are excluded: a zero local dimension satisfies none of the statements, since a non-degenerate ground state requires a one-dimensional eigenspace and the gapless condition requires a non-empty spectrum; and every existential statement fixes the matrices before quantifying over all instances $n$ and all lattice sizes $L$.

Contributions are welcome at any milestone, and also on the infrastructure the milestones need — Wang tilings and the Robinson tile set, Gottesman–Irani history-state Hamiltonians, and quantum Turing machines in the Bernstein–Vazirani sense — which are needed for Theorem 6 and Lemma 47 of the source and are not yet part of this mission's item list.

Selected references

• T. S. Cubitt, D. Pérez-García, M. M. Wolf, Undecidability of the Spectral Gap (full version), Forum of Mathematics, Pi 10:e14, 1–102 (2022). https://doi.org/10.1017/fmp.2021.15 — the version all statements of this mission are formalized against; preprint: https://arxiv.org/abs/1502.04573
• T. S. Cubitt, D. Pérez-García, M. M. Wolf, Undecidability of the spectral gap, Nature 528, 207–211 (2015). https://doi.org/10.1038/nature16059
• R. M. Robinson, Undecidability and nonperiodicity for tilings of the plane, Inventiones Mathematicae 12, 177–209 (1971). https://doi.org/10.1007/BF01418780
• D. Gottesman, S. Irani, The quantum and classical complexity of translationally invariant tiling and Hamiltonian problems, FOCS 2009. https://arxiv.org/abs/0905.2419
• E. Bernstein, U. Vazirani, Quantum complexity theory, SIAM J. Comput. 26, 1411–1473 (1997). https://doi.org/10.1137/S0097539796300921
• J. Bausch, T. S. Cubitt, A. Lucia, D. Pérez-García, Undecidability of the spectral gap in one dimension, Phys. Rev. X 10, 031038 (2020). https://doi.org/10.1103/PhysRevX.10.031038

Parallel repetition for quantum games

Nonlocal games

A nonlocal game is played between a classical referee and two or more cooperating players who are not allowed to communicate during the game. In the two-player, one-round setting, the referee samples a pair of questions $(x,y)$ from a distribution $\mu$, sends $x$ to Alice and $y$ to Bob, and receives answers $a$ and $b$. The players win when a predicate $V(x,y,a,b)$ accepts. Before the game begins they may agree on a strategy and share a resource, but after receiving their questions they are isolated from one another.

Nonlocal games occupy a useful interface between complexity theory and quantum information. From the perspective of complexity theory, they are the basic objects underlying multiprover interactive proofs: a verifier delegates a computation to separated provers and uses the consistency of their answers to distinguish valid from invalid claims. Classical two-prover games play a central role in the PCP theorem, hardness of approximation, and soundness amplification. Allowing the provers to share entanglement leads to the class $\mathrm{MIP}^*$ and to a substantially richer theory. The theorem $\mathrm{MIP}^*=\mathrm{RE}$ shows how dramatically entanglement changes this landscape: even estimating the entangled value of a nonlocal game can encode undecidable computation Ji--Natarajan--Vidick--Wright--Yuen 2020.

From the perspective of quantum information, nonlocal games are operational formulations of Bell experiments. A separation between classical and entangled values witnesses correlations that cannot be explained by a local hidden-variable model. The same framework supports self-testing, in which near-optimal behavior certifies the underlying state and measurements up to local equivalence, and device-independent cryptography, in which security or randomness is certified from observed input-output statistics rather than a trusted description of the devices. Representative references include Cleve--Høyer--Toner--Watrous 2004, Reichardt--Unger--Vazirani 2013, and Pironio et al. 2010. The survey of Palazuelos--Vidick 2016 describes further connections among nonlocal games, Bell inequalities, operator spaces, and quantum information.

Thus the value of a nonlocal game is simultaneously a complexity-theoretic soundness parameter and a quantitative measure of the power of nonclassical correlations. Understanding how this value changes under natural operations on games is important in both subjects.

Entangled strategies and value

We take the finite answer alphabets to be nonempty. In a classical strategy, Alice's answer depends only on $x$, Bob's answer depends only on $y$, and the players may coordinate using shared randomness. In a finite-dimensional entangled strategy, the players share a bipartite state $\rho$ and use POVM measurement operators

for their respective questions. The probability of producing answers $(a,b)$ on questions $(x,y)$ is

The supremum of the winning probability over all such finite-dimensional strategies is the entangled value $\omega^*(G)$. This optimization ranges over arbitrary local dimensions, shared states, and local measurements, which is one reason even apparently elementary questions about nonlocal games can be difficult.

Parallel repetition

For a positive integer $n$, the repeated game $G^n$ consists of $n$ independently sampled copies of $G$ played simultaneously. Alice receives $(x_1,\ldots,x_n)$, Bob receives $(y_1,\ldots,y_n)$, and they answer with tuples $(a_1,\ldots,a_n)$ and $(b_1,\ldots,b_n)$. They win only if

for every coordinate $i$.

Parallel repetition is a basic method of soundness amplification. Starting from a game that dishonest players cannot win with certainty, the verifier repeats the test in the hope of driving the optimal success probability rapidly toward zero. The difficulty is that independence in the verifier's sampling does not force independence in the players' strategy. Alice may choose her entire answer tuple as a function of all her questions, Bob may do the same, and an entangled strategy may use a single state and joint measurements spanning all coordinates. In particular, one cannot obtain an upper bound on $\omega^*(G^n)$ merely by analyzing the strategy that plays each coordinate independently.

For classical games, Raz's parallel repetition theorem gives exponential decay whenever the one-shot value is below one Raz 1998. Establishing the corresponding behavior for entangled games has been a long-running problem. A general polynomial bound was proved in Yuen 2016, implying for the first time that $\omega^*(G^n)$ tends to zero for every finite two-player entangled game with $\omega^*(G)<1$.

The full exponential-decay theorem was recently settled by OpenAI. In Chapter 6 of Ten Advances in Mathematics and Theoretical Computer Science, OpenAI proves that for every finite two-player entangled game $G$ with $\omega^*(G)<1$, there is a constant $c_G>0$ such that

for every positive $n$. OpenAI also released a Lean certificate for the result. This resolves the general quantum parallel-repetition conjecture, but it does not end the study of the problem. The proof introduces quantitative losses and a substantial technical apparatus, and there remains considerable value in finding alternative arguments, isolating the essential mechanism, improving the dependence on the one-shot gap and answer size, and producing shorter or more conceptual formal proofs.

A hierarchy of formalization targets

This mission develops a reusable Lean framework for parallel repetition rather than formalizing only one paper. Its targets are organized by the strength of the asserted decay.

Qualitative decay

The main mission theorem is the fundamental asymptotic statement:

Equivalently, for every $\delta>0$, all sufficiently large $n$ satisfy $\omega^*(G^n)<\delta$. This statement deliberately specifies no rate. It is a stable top-level theorem that can be recovered from any sufficiently strong quantitative bound.

Polynomial decay

A stronger target asks for game-dependent constants $C>0$ and $\alpha>0$ such that

The abstract formulation avoids fixing a particular exponent or logarithmic correction. More refined formalizations can record explicit dependence on the gap $1-\omega^*(G)$, the answer alphabet, or other game parameters. Yuen's 2016 theorem is one important result at this level.

Exponential decay

The exponential target asks for game-dependent constants $C,c>0$ such that

Following OpenAI's recent resolution, this target is now a theorem rather than an open conjecture. Within this mission it remains a central milestone: contributors may formalize the released argument in the mission's common interface, construct an independent proof, seek a more elegant or modular proof, or establish sharper quantitative variants.

These levels do not exhaust the project. The same framework can accommodate explicit finite-$n$ inequalities, stretched-exponential estimates, bounds for structured classes of games, improved parameter dependence, and reductions showing that one decay statement implies another.

Formalization scope

The foundational Lean development represents a game by finite question sets $X,Y$, finite answer sets $A,B$, a nonnegative normalized question distribution $\mu(x,y)$, and a Boolean verification predicate $V(x,y,a,b)$. The parallel-repetition theorems explicitly assume that $A$ and $B$ are nonempty. The development defines finite-dimensional entangled strategies using density matrices and POVM measurement operators, defines the repeated game on tuples, and takes the entangled value as a supremum over all finite-dimensional strategies. Repeated strategies are indexed by complete question tuples and are not required to factor coordinatewise.

A complete development will draw on formal libraries for finite probability, tensor products, positive semidefinite matrices, density matrices, POVMs, trace norms, fidelity, entropy, mutual information, and correlated sampling. These components should be formulated for reuse and should expose the dependence of each bound on the relevant game parameters.

The goal is both to verify parallel-repetition theorems and to build a dependable language for nonlocal games in Lean. Formalization forces distinctions that are easy to suppress on paper: whether constants depend on the game, whether a bound holds for all $n$ or only asymptotically, which strategy model is optimized over, and which hypotheses are needed for a particular rate. The mission welcomes reconstructions of known proofs as well as new, shorter, or conceptually different proofs.

Selected references

• R. Cleve, P. Høyer, B. Toner, and J. Watrous, Consequences and limits of nonlocal strategies, CCC 2004.
• R. Raz, A parallel repetition theorem, SIAM Journal on Computing 27(3), 1998.
• H. Yuen, A parallel repetition theorem for all entangled games, ICALP 2016.
• Z. Ji, A. Natarajan, T. Vidick, J. Wright, and H. Yuen, $\mathrm{MIP}^*=\mathrm{RE}$, Communications of the ACM 64(11), 2021.
• OpenAI, Ten Advances in Mathematics and Theoretical Computer Science, Chapter 6, 2026; accompanying Lean formalization.

Motivation

The discrete logarithm problem modulo a prime asks, given a prime $p$, a generator $g$ of the multiplicative group modulo $p$, and a nonzero residue $x$, for the exponent $r$ with $g^r\equiv x \pmod p$. Its presumed classical hardness underlies Diffie–Hellman key exchange, ElGamal encryption and the Digital Signature Algorithm. The best classical algorithm known when Shor wrote, Gordon's adaptation of the number field sieve, runs in time $\exp(O((\log p)^{1/3}(\log\log p)^{2/3}))$.

In §6 of Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer (SIAM J. Comput. 26(5), 1997; doi:10.1137/S0097539795293172, arXiv:quant-ph/9508027), Shor gave a quantum algorithm that uses two modular exponentiations and two quantum Fourier transforms and outputs, with constant probability, a pair from which $r$ can be computed. The quantitative core of that analysis is a single number: the circuit produces a "good" output with probability at least $1/480$. This mission formalizes that bound and the three estimates it is assembled from.

Setting

Let $p$ be a prime and $g$ a generator of $(\mathbb Z/p\mathbb Z)^\times$, so that $1,g,\dots,g^{p-2}$ are all the nonzero residues. Fix the unknown $r$ with $0\le r<p-1$ and put $x=g^r$. Let $q=2^l$ be the power of $2$ with $p<q<2p$.

The Fourier matrix $A_q$ is the $q\times q$ matrix with entries $(A_q)_{a,c}=q^{-1/2}\exp(2\pi i\,ac/q)$ for $0\le a,c<q$ (§4, eq. (4.1)). Rows index input basis vectors and columns output basis vectors.

The algorithm uses three registers: two holding numbers $0\le a,b<q$ and one holding a nonzero residue modulo $p$. It starts from the state

(preFourierState), applies $A_q$ to each of the first two registers (finalState), and measures all three registers. The probability of observing $|c,d,y\rangle$ is the squared modulus of its amplitude (outcomeProb).

For integers $z$ and $q>0$, the symmetric residue $\{z\}_q$ is the residue of $z$ modulo $q$ in $(-q/2,q/2]$ (symmRes). Put

An observed state $|c,d,y\rangle$ is good (IsGood) when

Goodness depends only on $(c,d)$.

Formalization targets

Goal: a good output with probability at least $1/480$ (§6, p. 1504)

The constant is the one the page carries forward. The goal fixes no threshold on $p$: it is stated for every prime $p$ that admits a power of two strictly between $p$ and $2p$.

Milestones

1. The output distribution, eq. (6.4). For $0\le k<p-1$,

2. Each good state is likely, eq. (6.17). If $(c,d)$ is good, then $\Pr[c,d,y]\ge 1/(20q^2)$ for every $y$.
3. Many good pairs (p. 1504). At least $q/12$ pairs $(c,d)$ are good.
4. Each good $c$ is likely (p. 1504). If $(c,d)$ is good for some $d$, then $\sum_{d',y}\Pr[c,d',y]\ge(p-1)/(20q^2)\ge1/(40q)$.

Significance

The result. The bound $1/480$ is what turns the circuit into an algorithm. Repeating the circuit $O(1)$ times in expectation yields a good output, and from a good pair $(c,d)$ one reads off an equation that determines $r$ modulo divisors of $p-1$ (§6, eqs. (6.18)–(6.20)). Together with the quantum Fourier transform circuit and reversible modular exponentiation, this places the discrete logarithm modulo a prime in quantum polynomial time. Every later analysis of quantum attacks on discrete-logarithm cryptography starts from this success probability or a sharpened version of it.

Formalizing it. The result has been proved since 1994–1997 and is textbook material; it is not open. As far as is known, no machine-checked proof of Shor's discrete-logarithm analysis exists. The paper's proof of eq. (6.17) replaces a sum by an integral with an error term $O(W/(pq))$ whose constant is not given, yet states $1/(20q^2)$ for every prime. A formal proof must therefore either control that error explicitly or find another argument, and so settles a point the paper leaves informal. Numerically, the smallest value of $q^2\Pr[c,d,y]$ over good states is about $0.49$ for all primes $p<90$, so the unconditional claim is not in doubt for small $p$. The page also contains two small slips, recorded under Formalization scope; a complete development pins down exactly what is true.

Difficulty

The exponential sum (6.4) runs over pairs $(a,b)$ satisfying a congruence modulo $p-1$, while the phases are taken modulo $q$. The two moduli are unrelated: $q$ is a power of two and $p-1$ is arbitrary. Eliminating $a$ through the congruence introduces a floor function $\lfloor(br+k)/(p-1)\rfloor$, and the resulting phase is not linear in $b$. The obvious estimate treats the sum as a geometric series in $b$ and bounds it by its first-order phase; this fails because the floor term perturbs every phase by an amount of size up to $|\{c(p-1)\}_q|$. Condition (6.11) only keeps this perturbation within $\pi/6$ of the main phase; it does not remove it. The per-state bound must survive this perturbation uniformly in $p$, $r$ and $k$, including small primes where the paper's integral approximation gives no explicit control.

The count of good pairs needs a separate argument about how often a multiple $c(p-1)$ lies within $q/12$ of a multiple of $q$ when $\gcd(p-1,q)$ is large.

Formalization scope

• States are functions Fin q × Fin q × (ZMod p)ˣ → ℂ. The first two registers range over $\{0,\dots,q-1\}$; the third over the units modulo $p$.
• Matrix convention. Following §2, rows are inputs, so the amplitude of $|c,d,y\rangle$ after the transforms is $\sum_{a,b}\psi(a,b,y)(A_q)_{a,c}(A_q)_{b,d}$. finalState is defined this way from (6.1) and $A_q$. It is not typed in as the closed form (6.3) or (6.4). A formalization that defined the final state by (6.4) directly would make milestone 1 trivial, and is ruled out.
• Probability of a basis state is the squared norm of its amplitude, with no normalization hypothesis.
• Parameters. $p$ is prime (Fact p.Prime). The generator is encoded as orderOf g = p - 1. $r<p-1$ is a parameter, with $x=g^r$. $q$ is given by q = 2 ^ l together with $p<q<2p$. No large-$p$ threshold is added anywhere.
• Arithmetic. $x^{-b}$ is x⁻¹ ^ b in the unit group. $p-1$ is computed in $\mathbb Z$ and $\mathbb R$ inside $T$ and the congruences, and as natural-number subtraction only where $p\ge2$ makes it exact. $T$ is real.
• Condition (6.10) is stated as "some integer $j$ has $|T-jq|\le\frac12$". Because $q\ge4$, this is equivalent to the page's form with $j$ the closest integer to $T/q$.
• Not formalized. The preparation of (6.1) by testing and restarting is not formalized; the state (6.1) is taken as displayed. The printed test "whether the number is less than $p$" should read $p-1$, as the sums in (6.1) show. Also out of scope: the recovery of $r$ (eqs. (6.18)–(6.20)), the repetition count "$480t$", and all running-time claims.
• Printed slips.
  • The page asserts that for each $c$ there is exactly one $d$ satisfying (6.10). At a tie $\{T\}_q=\pm\frac12$ there can be two such $d$. Milestone 3 states only the count, which needs at least one.
  • The page's intermediate bound "at least $p/(240q)$" should be $(p-1)/(240q)$. The conclusion $1/480$ is unaffected, since $q$ and $2p$ are both even and so $q\le 2(p-1)$. Only $1/480$ is stated.

Needed infrastructure: finite exponential sums and their modulus, the symmetric residue and its basic properties, and counting multiples in residue classes of $\mathbb Z/q$. The exponential-sum estimates of milestones 1 and 2 are reusable in the order-finding analysis of §5 of the same paper. Proofs of any milestone, of the normalization $\sum\Pr=1$, and of auxiliary lemmas about symmRes are welcome.

Selected references

• P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172 (preprint: https://arxiv.org/abs/quant-ph/9508027)
• D. M. Gordon, Discrete logarithms in GF(p) using the number field sieve, SIAM J. Discrete Math. 6(1):124–138, 1993. https://doi.org/10.1137/0406010
• W. Diffie and M. E. Hellman, New directions in cryptography, IEEE Trans. Inform. Theory 22(6):644–654, 1976. https://doi.org/10.1109/TIT.1976.1055638
• M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000. https://doi.org/10.1017/CBO9780511976667

Motivation

Shor's factoring and discrete logarithm algorithms (Shor 1997) reduce both problems to sampling from the output of a quantum Fourier transform: a register holding a superposition with a hidden period is transformed, then measured, and the measured value carries information about the period. The whole speed-up rests on one engineering fact: for $q = 2^l$ the $q \times q$ Fourier matrix, which has $q^2 = 4^l$ entries, can be applied by a quantum circuit of only $O(l^2)$ elementary gates, each acting on one or two bits.

That circuit was found independently by Coppersmith (IBM RC 19642, 1994) and Deutsch, and Shor's §4 presents it following Ekert and Jozsa (Rev. Mod. Phys. 68, 1996). It is the quantum analogue of the radix-2 fast Fourier transform, and it reappears in phase estimation, in the hidden subgroup algorithms for abelian groups, and in every textbook account of quantum computation. This mission formalizes Shor's statement that the circuit computes the Fourier matrix, up to a reversal of the output bits, together with the two displayed steps of its verification.

Setting

A register of $l$ bits has one basis state $|a\rangle = |a_{l-1} a_{l-2} \dots a_0\rangle$ for every bit string, with $a_0$ the least significant bit; the string encodes the integer

A state is a vector of complex amplitudes, one per basis state. A gate is a matrix whose rows are indexed by input basis vectors and whose columns are indexed by output basis vectors (§2, p. 1489). A gate on some of the bits acts on those bits through its matrix and leaves the others alone (§2, p. 1490): the output amplitude at a string $b$ is the sum, over the possible input values $u$ of the acted-on bits, of the input amplitude at $b$ with those bits replaced by $u$, times the matrix entry from $u$ to the corresponding bits of $b$.

The Fourier matrix $A_q$ (eq. (4.1)) is the $q \times q$ matrix with $(a, c)$ entry $q^{-1/2}\exp(2\pi i\,ac/q)$; it takes $|a\rangle$ to $q^{-1/2}\sum_{c=0}^{q-1}\exp(2\pi i\,ac/q)\,|c\rangle$.

The circuit uses two gates (eqs. (4.2), (4.3)):

• $R_j$ acts on bit $j$ with matrix $\frac{1}{\sqrt 2}\begin{pmatrix} 1 & 1 \\ 1 & -1\end{pmatrix}$;
• $S_{j,k}$, for $j < k$, acts on bits $j$ and $k$ with matrix $\mathrm{diag}(1, 1, 1, e^{i\theta_{k-j}})$, where $\theta_{k-j} = \pi / 2^{k-j}$; it multiplies the amplitude of a basis state by $e^{i\theta_{k-j}}$ when bits $j$ and $k$ are both $1$.

The circuit is the gate sequence (4.4), applied from left to right:

that is, for $j = l-1, \dots, 0$ it applies $S_{j,l-1}, \dots, S_{j,j+1}$ and then $R_j$. On three bits it is $R_2 S_{1,2} R_1 S_{0,2} S_{0,1} R_0$.

The bit reversal of a string $b$ is the string $c$ with $c_k = b_{l-1-k}$.

Formalization targets

Goal: the circuit computes $A_q$ up to bit reversal (§4, p. 1496)

For every $l \ge 0$ and every basis state $|a\rangle$, with $q = 2^l$,

The sum runs over all $l$-bit strings $b$. Reading the output register in reverse order therefore yields $A_q|a\rangle$.

Milestone 1: the amplitude along the circuit (§4, eq. (4.5), p. 1496)

The amplitude of $|b\rangle$ in $\text{circuit}\,|a\rangle$ is

Milestone 2: the phase identity (§4, eqs. (4.6)–(4.10), pp. 1496–1497)

For bit strings $a, b$, with $c$ the bit reversal of $b$ and $a, c$ their values,

Significance

The result. The goal says that $A_q$, a dense unitary on $2^l$ amplitudes, is realized by $l$ one-bit gates and $l(l-1)/2$ two-bit gates, followed by a relabelling of the output. This is what makes the Fourier sampling step of the factoring algorithm (§5) and of the discrete logarithm algorithm (§6) polynomial in the number of bits. Without it, the analyses of those sections describe measurements of states that no efficient circuit is known to prepare. The bit reversal is a real part of the statement: the circuit does not compute $A_q$ itself for $l \ge 2$, and an implementation must either permute the output bits or read them in reverse order.

Formalizing it. The identity is classical and its proof is short on paper; its content lies in bookkeeping that is easy to get wrong: which bit a gate touches, which of the input or output value a bit holds when a phase gate acts, and the order in which the gates are applied. A machine-checked version fixes all of these conventions explicitly and yields a reusable model of gate-level circuits on bit strings. To the drafter's knowledge there is no Lean formalization of this circuit on Prove2Me; the platform's FastFourierTransform rows state the classical Cooley–Tukey recursion for the unnormalized transform with the opposite sign, which is a different object.

Difficulty

Multiplying out the gate matrices is not an argument beyond tiny $l$: the difficulty is to control the whole product of $l(l+1)/2$ gates symbolically. The paper's argument (§4, p. 1496) is informal at exactly the points a formal proof must make precise: that only one sequence of intermediate basis states from $|a\rangle$ to $|b\rangle$ carries nonzero amplitude, and that at the moment $S_{j,k}$ acts, bit $k$ already holds its output value $b_k$ while bit $j$ still holds its input value $a_j$. Both facts depend on the order (4.4); applying the same gates in the reverse order gives a different unitary, whose phase pairs $b_j$ with $a_k$. The phase identity then holds only modulo $2\pi$, not as an equality of real numbers, so it cannot be closed by rearranging sums alone.

Formalization scope

• States. A bit string on $l$ bits is Fin l → Fin 2, with bit j equal to $a_j$ and value $\sum_j 2^j a_j$ (least significant bit first). A state is a function from bit strings to ℂ. The case $l = 0$ ($q = 1$, empty circuit) is included.
• Gate application follows the row = input convention: a one-bit gate $M$ on bit $j$ sends $\psi$ to $b \mapsto \sum_u \psi(b[j\mapsto u])\,M_{u, b_j}$, and a two-bit gate acts analogously on the pair (bit $j$, bit $k$).
• The circuit is the gate list (4.4) — an explicit list of constructors R j and S j k — run by a left fold, so the leftmost gate acts first. It is not defined as the matrix $A_q$ or by its entries; a definition of that kind would make the goal true by unfolding and is ruled out.
• Angles. $\theta_{k-j} = \pi/2^{k-j}$ uses natural-number subtraction, which is exact because the list only contains $S_{j,k}$ with $j < k$.
• Normalization. The prefactor $q^{-1/2}$ is written $(\sqrt{2^l})^{-1}$.
• Basis form. The goal is stated on basis states, as on the page; by linearity it determines the circuit on every state.
• Not stated. The gate count: the paper's sentence "we thus need to use $l(l-1)/2$ quantum gates" (p. 1496) counts only the gates $S_{j,k}$; the sequence (4.4) also contains the $l$ gates $R_j$, $l(l+1)/2$ gates in all. The approximate transform of Coppersmith and the one-bit construction of Griffiths and Niu (p. 1497) are out of scope, as is the polynomial-time claim.

Welcome contributions: proofs of the two milestones and the goal; general lemmas about one- and two-bit gate actions on Fin l → Fin 2 states (commutation of gates on disjoint bits, linearity, action on basis states), which are reusable for any gate-level circuit; and a proof that the circuit is unitary.

Selected references

• P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172
• D. Coppersmith, An approximate Fourier transform useful in quantum factoring, IBM Research Report RC 19642, 1994. https://arxiv.org/abs/quant-ph/0201067
• A. Ekert and R. Jozsa, Quantum computation and Shor's factoring algorithm, Rev. Mod. Phys. 68:733–753, 1996. https://doi.org/10.1103/RevModPhys.68.733
• R. B. Griffiths and C.-S. Niu, Semiclassical Fourier transform for quantum computation, Phys. Rev. Lett. 76:3228–3231, 1996. https://doi.org/10.1103/PhysRevLett.76.3228

Motivation

A quantum computer manipulates superpositions of many degrees of freedom, and every gate it applies is imperfect. Before 1996 it was widely argued that this fragility is fatal: the accuracy demanded of each elementary operation appeared to grow with the length of the computation, so that arbitrarily long computations would require arbitrarily perfect hardware. The discovery of quantum error-correcting codes, of fault tolerant syndrome extraction, and of transversally encoded operations changed that picture, but the first fault tolerant schemes still required the error per operation to shrink as the computation grew.

Knill, Laflamme and Zurek, Resilient Quantum Computation: Error Models and Thresholds (arXiv:quant-ph/9702058), together with the independent work of Kitaev and of Aharonov and Ben-Or, removed that requirement: they exhibited a fixed threshold value such that any physical error rate below it permits arbitrarily accurate encoded computation, at an overhead that is only polylogarithmic in the length of the computation. Their paper is also the one that pushes past independent stochastic noise: its thresholds are proved for quasi-independent error models, which accommodate coherent over-rotation and weak residual couplings between neighbouring qubits.

This mission formalizes the quantitative engine of that paper: the concatenation recursion, the error-model bounds it is applied to, the threshold it produces, and the resulting overhead.

Setting

Fix a physical implementation in which each gate, state preparation and idle memory step carries an error location. A noisy network with error locations indexed by a finite set $\mathrm{locs}$ is described through an error expansion; each summand fails at a set of locations, and the model constrains how probable simultaneous failures are.

Write $\mu$ for the underlying probability measure and $F_i$ for the event that location $i$ has failed. Two models from Section I.B of the paper are used here.

• Quasi-independent stochastic model with error probability $p$: for every set $S \subseteq \mathrm{locs}$ of error locations,

• Quasi-independent monotonic model with constant $C$ and parameter $p$: the same quantity is bounded by $C\,p^{|S|}$.

The fault tolerant construction of Section I turns physical qubits into encoded qubits: each encoded gate is a transversal operation preceded by fault tolerant recovery networks built from the $7$-qubit Steane code. The analysis of Section II declares an encoded gate failed according to an explicit combinatorial rule, and shows that a failure requires two failures among a set of $f$ minimal pairs of physical error locations. Consequently one level of encoding maps a failure parameter $p$ to $f p^{2}$.

Iterating this reduction is concatenation. Define the level-$h$ failure parameter by

written $E_h = \texttt{levelError}\,f\,p\,h$ in the Lean development. Let $K$ bound the number of qubits and time steps at the level below that are consumed by one encoded gate, so that one computational gate at level $h$ costs $K^{h}$ physical resources.

Formalization targets

Goal — threshold theorem with polylogarithmic overhead

For $f \ge 1$, $K \ge 2$, $0 \le p < 1/f$, and every gate count $n$ and target failure probability $q$ with $0 < q < n$, there exists a level $h$ with

The first clause is resilience: a computation of $n$ encoded gates can be made to fail with probability below any prescribed $q$. The second is the cost: the overhead per computational gate is polylogarithmic in $n/q$, with exponent $\log_2 K$. The threshold itself is the hypothesis $p < 1/f$; no numerical value is hard-coded, so the statement survives any improvement of the paper's count $f \le 337195$ and of the resulting bounds $3.0 \times 10^{-6}$ and $1.3 \times 10^{-6}$.