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.