Algebra·Captain: wenxinzhang

Existence of complete sets of mutually unbiased basesOpen Problem

Motivation

Two orthonormal bases of C^d are mutually unbiased when every transition amplitude has squared modulus 1/d. At most d+1 such bases can coexist, and complete families are known in prime-power dimensions through finite-field constructions. Dimension six is the smallest famous composite case where existence of the complete seven-base family remains unknown.

This mission turns CUHK-Shenzhen AI Math Problem 16, Existence of complete sets of mutually unbiased bases, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.

Setting

Construct seven 6 by 6 unitary-column matrices whose every distinct pair has all transition amplitudes of squared modulus 1/6. The baseline milestone constructs three pairwise mutually unbiased bases, a known lower bound that tests all matrix conventions.

Significance

Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in quantum information theory, mutually unbiased bases, finite fields, Hilbert spaces. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.

Difficulty

The equations are a large coupled system of polynomial equalities over complex phases, modulo substantial gauge symmetry. Numerical near-solutions do not certify exact existence, while nonexistence would require a global obstruction beyond currently known bounds. Dimension six lacks the finite-field structure that supplies complete prime-power constructions.

Suggested attack route

Formalize standard gauge reductions: fix the first basis to the identity and dephase transition Hadamard matrices. Verify a three-basis tensor-product construction. Then encode additional bases through complex Hadamard matrices and study algebraic constraints, Gröbner-style eliminations, semidefinite bounds, or exact certificates. Computational searches may guide conjectures, but uploaded proofs must convert numerical evidence to exact algebraic identities or certified inequalities.

Formalization scope

The Lean target is exact: column orthonormality is U-adjoint times U equals identity, and mutual unbiasedness uses Mathlib complex norm squared. Seven bases are indexed by Fin 7. No quotient by phase, permutation, or global unitary is built into the statement, since these symmetries preserve the predicate and can be used within proofs.

The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.

Milestones

Publish an exact three-basis construction in dimension six, then formalize dephasing and obstruction lemmas for extending a partial family.

The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.

Timeline and literature status

The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.

Acceptance criteria

A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.

The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.

Formal verification policy

The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.

Selected references

14 thms5 active usersReviewed

Completed

Machine Learning Operations Research Stochastic Systems·Captain: tianyipeng

Markov Entanglement: Value Decomposition Error in Multi-agent MDPsResearch Paper

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.

25 thms5 active usersReviewed

Completed

Mathematical Physics Probability·Captain: Lucas

Hardy 2001 I: Five Reasonable Axioms — Degrees of Freedom K = N^rResearch Paper

Motivation

In the usual textbook presentation, quantum theory starts from postulates that have no obvious operational meaning: states are density operators on a complex Hilbert space, measurements are positive operators, and probabilities are given by the trace formula $p=\mathrm{tr}(\hat A\hat\rho)$ . In Quantum Theory From Five Reasonable Axioms (Hardy 2001), Lucien Hardy asks whether this structure can instead be derived from simple statements about preparations, transformations and measurements, in the same way that classical probability theory can be set up by pure thought. He proposes five axioms (probabilities, simplicity, subspaces, composite systems, continuity) and argues that they single out finite- and countably-infinite-dimensional quantum theory. Dropping a single word, "continuous" in Axiom 5, leaves classical probability theory instead.

The paper is one of the starting points of the operational or generalized probabilistic theory (GPT) approach to the foundations of quantum mechanics. It was followed by reconstructions that replace the simplicity axiom, e.g. Dakić–Brukner 2009, Masanes–Müller 2011 and Chiribella–D'Ariano–Perinotti 2011.

Setting

A system is described by two integers. The dimension $N$ is the maximum number of states that can be distinguished in a single-shot measurement. The number of degrees of freedom $K$ is the minimum number of probability measurements needed to determine the state. The state is the vector $p=(p^1,\dots,p^K)\in\mathbb R^K$ of the probabilities of $K$ fiducial measurements. States are not assumed normalized: the null state $p=0$ (no system present) is allowed. The set $S$ of allowed states is convex, and its pure states are its extremal points other than $0$ .

The five axioms are:

Probabilities. Relative frequencies converge to the same limit for every ensemble prepared by a given preparation.
Simplicity. $K=K(N)$ is a function of $N=1,2,\dots$ , and for each $N$ it takes the minimum value consistent with the axioms.
Subspaces. A system whose state is constrained to an $M$ -dimensional subspace behaves like a system of dimension $M$ .
Composite systems. A composite of systems $A$ and $B$ has $N=N_AN_B$ and $K=K_AK_B$ .
Continuity. Between any two pure states there is a continuous reversible transformation.

A probability theory can be summarized by its signature $x=(x_1,x_2,\dots)$ , defined through

K=Nx_1+\tfrac1{2!}N(N-1)x_2+\tfrac1{3!}N(N-1)(N-2)x_3+\cdots=\sum_{k\ge1}\binom Nk x_k .

Classical probability theory has $x=(1,0,0,\dots)$ and $K=N$ . Complex quantum theory has $x=(1,2,0,\dots)$ and $K=N^2$ . Real and quaternionic quantum theory have $x=(1,1,0,\dots)$ and $x=(1,4,0,\dots)$ .

Formalization targets

Goal: $K(N)=N^r$

Section 8.1 shows that Axiom 3 forces $K(N+1)\ge K(N)+1$ , and Axiom 4 forces $K(N_AN_B)=K(N_A)K(N_B)$ . The goal theorem is the purely arithmetic consequence (Eq. (57)):

K(N+1)\ge K(N)+1\ \text{ and }\ K(N_AN_B)=K(N_A)K(N_B)\ \ (N,N_A,N_B\ge1)\quad\Longrightarrow\quad \exists r\in\{1,2,3,\dots\}:\ K(N)=N^r\ \ \forall N\ge1 .

Milestones

The milestones follow the paper's own steps, in the paper's numbering:

Appendix 2: a strictly increasing, completely multiplicative $K$ on the positive integers satisfies $K(n)=n^\alpha$ . Section 8.1: if every $n^\alpha$ is an integer, then $\alpha$ is a positive integer.
Section 6.6 / Appendix 1: measured probabilities are linear in the state, $p_{\rm meas}=r\cdot p$ . Section 6.7: transformations act as matrices, $p\mapsto Zp$ . Section 7: reversible transformations send pure states to pure states.
Section 4 / 8.5: in classical probability theory the pure states are exactly the $N$ basis states, and no continuous path of pure states joins two distinct ones. The equations $\sum_k(p^k)^2=1$ , $0\le p^k\le1$ , $\sum_kp^k=1$ force a basis vector.
Sections 5 and 8.1: the signatures of the classical, quantum, real, quaternionic and $K=N^3$ theories, and the failure of $K=K_AK_B$ for real (too many) and quaternionic (too few) composites.
Section 5: the $N^2$ projectors $|n\rangle\langle n|$ , $|mn\rangle_x\langle mn|$ , $|mn\rangle_y\langle mn|$ are linearly independent over $\mathbb R$ and span the Hermitian operators.
Sections 5 and 8.6 ( $N=2$ ): the overlap formula (35) for $c$ ; $\det D>0 \iff c_-<c<c_+$ ; the decomposition $r^TDr'=\vec v^{\,T}A\vec v'+\mu\mu'/2$ ; $A$ positive definite $\iff c_-<c<c_+$ ; the Bloch matrix (87).
Section 8.7 ( $N=3$ ): the $9\times9$ matrix $D_{ij}=\mathrm{tr}(\hat P_i\hat P_j)$ with $h=1/2$ , $q=1/4$ .

Significance

The goal is the step at which the two structural axioms (subspaces and composites) cut the space of possible theories down to a single integer parameter $r$ . Combined with Section 8.5, which rules out $r=1$ by continuity, and with the simplicity axiom, it gives $K=N^2$ . Everything after that in the paper (the Bloch sphere, general $N$ , the trace formula, complete positivity) is carried out inside the $K=N^2$ case. The milestones on signatures make precise in which sense real and quaternionic quantum theory are excluded: their degree-of-freedom counts are not multiplicative under composition.

The paper's argument is informal physics. This mission isolates the mathematically precise statements that the argument relies on, so that they can be proved independently of the physical interpretation. It does not formalize the axioms themselves as a single Lean structure.

Difficulty

The arithmetic goal is an instance of a classical question about monotone completely multiplicative functions. Complete multiplicativity alone fixes $K$ only through its values at the primes, which are a priori unrelated to one another, and monotonicity is the only link between different primes. The step from a real exponent $\alpha$ to an integer exponent is a separate integrality argument that the paper does not spell out. The linearity milestones need care because the hypotheses hold only on a convex set containing $0$ , not on all of $\mathbb R^K$ . The $N=2$ milestones are explicit but delicate algebra with square roots and boundary cases $a,b\in\{0,1\}$ .

Formalization scope

All theorems live in the namespace HardyFiveAxioms. State vectors are functions Fin K → ℝ. Indices are $0$ -based, so the paper's fiducial vector $k$ is index $k-1$ .
$K(N)$ is a function ℕ → ℕ (goal) or ℕ → ℝ (Appendix 2), constrained only at arguments $\ge1$ . The value at $0$ is irrelevant.
The signature is a finite list [x₁, …, x_L], and $\frac1{k!}N(N-1)\cdots(N-k+1)$ is written as the binomial coefficient $\binom Nk$ .
Pure states are Set.extremePoints ℝ S \ {0}. The classical state space is $\{p\ge0,\ \sum_np_n\le1\}$ .
The quantum projectors are explicit matrices vecMulVec v (star v) over ℂ, and the qubit matrices $D$ , $C$ , $A$ and the roots $c_\pm$ are explicit definitions.
Axiom 5's "continuous reversible transformation" enters only through the classical milestone, as a continuous path unitInterval → ℝᴺ that stays inside the pure states.
The goal does not assume the conclusion in disguise. Its hypotheses are the two consequences of Axioms 3 and 4 derived in Section 8.1. It is not vacuous: $K(N)=N^r$ satisfies both hypotheses for every $r\ge1$ .

Contributions are welcome on any milestone. The linearity, extreme-point and positive-definiteness lemmas are reusable beyond this mission.

Selected references

L. Hardy, Quantum Theory From Five Reasonable Axioms, arXiv:quant-ph/0101012v4, 2001. https://arxiv.org/abs/quant-ph/0101012
B. Dakić, Č. Brukner, Quantum Theory and Beyond: Is Entanglement Special?, 2009. https://arxiv.org/abs/0911.0695
Ll. Masanes, M. P. Müller, A derivation of quantum theory from physical requirements, New J. Phys. 13, 063001, 2011. https://arxiv.org/abs/1004.1483
G. Chiribella, G. M. D'Ariano, P. Perinotti, Informational derivation of quantum theory, Phys. Rev. A 84, 012311, 2011. https://arxiv.org/abs/1011.6451

25 thms4 active usersReviewed

Completed

Mathematical Physics·Captain: Lucas

Albers–Kiefer–Reginatto 2008: Measurement Analysis and Quantum GravityResearch Paper

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

|\Psi_0\rangle = \tfrac{1}{\sqrt2}\bigl(|\uparrow\rangle_1|\downarrow\rangle_2 - |\downarrow\rangle_1|\uparrow\rangle_2\bigr)|\Phi_0\rangle, \qquad (1)

and after the detector has measured photon 1 it is

|\Psi\rangle = \tfrac{1}{\sqrt2}\bigl(|\uparrow\rangle_1|\downarrow\rangle_2|\Phi_\uparrow\rangle - |\downarrow\rangle_1|\uparrow\rangle_2|\Phi_\downarrow\rangle\bigr). \qquad (2)

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

\hat\rho = \tfrac12\bigl(|\uparrow\rangle_2\langle\uparrow|_2 + |\downarrow\rangle_2\langle\downarrow|_2\bigr). \qquad (3)

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$ ,

\rho_2(\Psi_0) = \hat\rho \quad\text{and}\quad \rho_2(\Psi) = \hat\rho .

Milestones

Eq. (1) ⇒ (3): $\rho_2(\Psi_0) = \hat\rho$ .
Eq. (2) ⇒ (3): $\rho_2(\Psi) = \hat\rho$ .
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)$ .
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}$ .
Eq. (61): $\min_{g\ne0}\sqrt{\Delta A^2/g^2 + g^2\Delta D^2} = \sqrt{2\,\Delta A\,\Delta D}$ .
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

8 thms4 active usersReviewed

Theoretical Computer Science·Captain: Goku

Stabilizer Rank of Magic StatesOpen Problem

Motivation

Quantum circuits built from Clifford gates alone are classically simulable in polynomial time. Universality is recovered by adding copies of a magic state, and the fastest known classical simulators of such circuits work by writing the magic-state input as a short linear combination of stabilizer states. The length of the shortest such combination -- the stabilizer rank -- is therefore the exponent governing classical simulation of quantum computation in this model, and lower bounds on it are among the very few unconditional obstructions to classical simulation available at all.

A timeline of what is established for the standard magic state $|H\rangle$ :

2016. Bravyi, Smith and Smolin exhibit a decomposition giving $\chi(|H^{\otimes 6}\rangle)\le 7$ , hence $\chi(|H^{\otimes n}\rangle)\le 7^{\,n/6}\le 2^{\,0.468n}$ , and prove a lower bound of order $\sqrt{n}$ .
2020. Huang, Newman and Szegedy show that hardness assumptions stronger than $\mathrm{P}\neq\mathrm{NP}$ , such as the exponential time hypothesis, imply $\chi(|H^{\otimes n}\rangle)=2^{\Omega(n)}$ (arXiv link).
2022. Peleg, Shpilka and Volk improve the unconditional lower bound to $\Omega(n)$ and give the first non-trivial bound for the approximate rank (arXiv:2106.03214).
2024. A quadratic lower bound is obtained for the approximate stabilizer rank (arXiv:2305.10277).

Between the linear unconditional lower bound and the $2^{0.468n}$ upper bound lies the open problem this mission targets.

Setting

Index the computational basis of an $n$ -qubit system by bit strings $x\in\{0,1\}^n$ , so a state is a vector $\psi\in\mathbb{C}^{2^n}$ with coordinates $\psi(x)$ .

The Pauli operators are $X^aZ^b$ for $a,b\in\{0,1\}^n$ , acting by $X^aZ^b|x\rangle=(-1)^{\,b\cdot x}|x\oplus a\rangle$ , where $b\cdot x$ counts the coordinates on which both are $1$ and $\oplus$ is bitwise addition; the Pauli group is the set of $4\cdot 4^n$ operators $i^cX^aZ^b$ . A unitary $U$ is a Clifford unitary when $UPU^\dagger$ lies in the Pauli group for every Pauli group element $P$ , and a stabilizer state is a vector $U|0\cdots0\rangle$ for some Clifford $U$ . There are $2^n\prod_{k=1}^{n}(2^k+1)$ of them up to phase -- six for a single qubit.

The stabilizer rank $\chi(\psi)$ is the least $r$ admitting coefficients $c_1,\dots,c_r\in\mathbb{C}$ and stabilizer states $\varphi_1,\dots,\varphi_r$ with $\psi=\sum_{j\le r}c_j\varphi_j$ .

The magic state is $|H\rangle=\cos(\pi/8)|0\rangle+\sin(\pi/8)|1\rangle$ , and $|H^{\otimes n}\rangle$ its $n$ -fold tensor power, with coordinates $\cos(\pi/8)^{\,n-|x|}\sin(\pi/8)^{\,|x|}$ where $|x|$ is the Hamming weight of $x$ .

Target

The goal is a super-polynomial lower bound: for every exponent $d$ and constant $C$ there exists $n$ with

\chi\bigl(|H^{\otimes n}\rangle\bigr)\;>\;C\,n^{d},

equivalently, $\chi(|H^{\otimes n}\rangle)$ is not $O(n^d)$ for any fixed $d$ .

Stronger statements are expected but are deliberately not the goal. An exponential bound $\chi=2^{\Omega(n)}$ is believed and follows from hardness assumptions, but a goal naming a specific growth rate would be superseded by the next improvement; super-polynomiality is the weakest statement that settles the question of principle.

Significance

The result itself. A super-polynomial lower bound would unconditionally rule out efficient classical simulation of Clifford-plus-magic-state circuits by stabilizer decomposition, currently the leading such technique. The converse direction shows how much is at stake: a polynomial upper bound on $\chi(|H^{\otimes n}\rangle)$ would imply $\mathrm{BPP}=\mathrm{BQP}$ , and via postselection $\mathrm{P}=\mathrm{NP}$ . There is also a purely classical payoff -- improving the known bound even to super-linear would produce a Boolean function computable in polynomial time requiring a super-linear number of summands in any decomposition into exponentials of quadratic forms over $\mathbb{F}_2$ , resolving a separate open question.

Formalizing it. The goal is open, so no known proof is being transcribed. What the mission produces is a machine-checked statement of the problem together with formalizations of the established bounds, none of which has a machine-checked proof anywhere. It also produces the first Pauli/Clifford/stabilizer layer in Lean: no existing Lean library contains the $n$ -qubit Pauli group, the Clifford group, or stabilizer states, and that layer is reusable for stabilizer error correction, magic monotones, and Clifford simulation generally.

Difficulty

Counting settles the problem for random states: the stabilizer states are too few for short combinations to cover a generic state, so almost every state has exponential stabilizer rank. This says nothing about $|H^{\otimes n}\rangle$ , which is a single explicit, highly structured vector, and the entire difficulty is that lower bounds must be proved for that specific state rather than for a typical one. Every newcomer proposes the counting argument; it does not apply.

The known techniques reduce the question to statements about decompositions of explicit Boolean functions into quadratic-form exponentials, and the barrier is quantitative: the available arguments lose a factor that caps them at linear bounds. The source of the current record documents explicitly why its method cannot pass super-linear, and the fact that going beyond linear would resolve an independent open problem in Boolean function complexity indicates the obstruction is not merely technical.

Formalization scope

State vectors are functions $\{0,1\}^n\to\mathbb{C}$ and are not required to be normalised; normalisation does not affect the rank, and stabilizer states are unit vectors automatically as Clifford images of $|0\cdots0\rangle$ . The Pauli group is given by the explicit parametrisation $i^cX^aZ^b$ rather than an abstract presentation, and the Clifford group is characterised as its unitary normaliser, equivalent to the usual generated-by- $H,S,\mathrm{CNOT}$ description. Because $e^{i\theta}U$ normalises the Pauli group whenever $U$ does, the stabilizer states are closed under global phase; this is harmless, as the coefficients are arbitrary complex numbers.

One trivialising reading must be excluded. The rank is defined as an infimum over a set of natural numbers, and Lean gives the empty infimum the value $0$ ; if no decomposition existed the rank would be $0$ for every state and the goal would be false rather than merely unproved. The milestone $\chi(\psi)\le 2^n$ is what certifies the set is nonempty, making the rank a genuine minimum, and it should be proved first. Separately, the goal quantifies $C$ over all reals including negative values, for which the inequality is trivially satisfiable; the content lies in large positive $C$ .

A complete development needs, beyond the published definitions, the correspondence between stabilizer states and affine subspaces carrying quadratic phase functions, on which all known lower-bound arguments rest. Contributions of any milestone are welcome, as are function-level reformulations of the rank and the equivalent characterisation of stabilizer states via maximal abelian Pauli subgroups.

Selected references

S. Peleg, A. Shpilka, B. L. Volk, Lower Bounds on Stabilizer Rank, Quantum 6 (2022) 652; arXiv:2106.03214.
S. Bravyi, G. Smith, J. Smolin, Trading Classical and Quantum Computational Resources, Phys. Rev. X 6 (2016) 021043; arXiv:1506.01396.
C. Huang, M. Newman, M. Szegedy, Explicit Lower Bounds on Strong Quantum Simulation, IEEE Trans. Inf. Theory 66(9) (2020) 5585--5600.
Quadratic Lower Bounds on the Approximate Stabilizer Rank: A Probabilistic Approach, STOC 2024; arXiv:2305.10277.

5 thms4 active usersReviewed

Information Theory Linear algebra·Captain: mikedeng1

Reversing quantum dynamics with near-optimal quantum and classical fidelity II: The Pretty Good Measurement Errs at Most the Weighted Sum of Bures–Uhlmann FidelitiesResearch Paper

Motivation

Quantum communication and computation often require a receiver to infer which preparation was sent after it has passed through a noisy quantum process. When possible preparations are mixed states, their overlap makes exact identification impossible. A measurement is then judged by its average probability of a correct label. The pretty good measurement gives a concrete measurement from the ensemble itself, without first solving the optimization over all measurements. Barnum and Knill related it to a general reversal operation for noisy dynamics and bounded its error through pairwise state fidelities in their preprint, §V–VI. The bound is useful when the overlaps are easier to estimate than the measurement's success probability.

The present mission addresses the preprint's second main result. The source is arXiv:quant-ph/0004088v2, not the later journal pagination. The preprint also strengthens its Theorem 3 relative to the published text, as its acknowledgment explains; this mission concerns Theorem 5 and the calculation around it.

Setting

An ensemble is a finite family of output density matrices $\hat\rho_j$ with probabilities $p_j\geq0$ satisfying $\sum_jp_j=1$ . A density matrix is a positive semidefinite complex matrix with trace one. For each label $j$ , fix an orthonormal eigenbasis $v_{ij}$ and nonnegative eigenvalues $\lambda_{ij}$ such that

\hat\rho_j=\sum_i\lambda_{ij}|v_{ij}\rangle\langle v_{ij}|, \qquad \sum_i\lambda_{ij}=1.

The eigenpair index $i$ runs over a finite output basis $O$ ; zero eigenvalues are allowed. The input labels form a finite basis $J$ . A label distribution is represented by $\rho=\sum_jp_j|j\rangle\langle j|$ .

The paper's classicizing channel $A$ has Kraus operators $A_{ij}=\sqrt{\lambda_{ij}}|v_{ij}\rangle\langle j|$ . Acting on an input matrix $X$ , its value is $A(X)=\sum_{i,j}A_{ij}X A_{ij}^{\dagger}$ . In particular, its output on $\rho$ is $\rho_{\mathrm{out}}=\sum_jp_j\hat\rho_j$ . The paper assumes $\rho_{\mathrm{out}}$ has full support when it writes its reversal operation. For a general Kraus family $A_a$ , that operation has operators

(R_{A,\rho})_a=\rho^{1/2}A_a^\dagger A(\rho)^{-1/2}.

The inverse square root is spectral: invert nonzero eigenvalues and leave zero eigenvalues at zero. With full support, it is the usual inverse square root.

For an input label $j$ , classical fidelity is the chance that the composite operation returns the same label. Averaging gives

F_{\mathrm{cl}}(\rho,K)= \sum_jp_j\langle j|K(|j\rangle\langle j|)|j\rangle.

The Bures–Uhlmann fidelity used here is the unsquared quantity $F_{\mathrm{BU}}(\sigma,\tau)=\operatorname{tr}\sqrt{\sqrt\sigma\,\tau\,\sqrt\sigma}$ . For the classicizing channel, the reversal operation realizes the pretty good measurement, as shown by equation (36) and the discussion after equation (37) in the preprint, p. 10.

Formalization targets

Recovery error

The goal, in the reading established by the paper's proof, is

F_{\mathrm{cl}}(\rho,R_{A,\rho}A) \geq 1-\sum_{\substack{i,j\in J\\i\ne j}} \sqrt{p_ip_j}\,F_{\mathrm{BU}}(\hat\rho_i,\hat\rho_j).

The sum is over ordered pairs; each unordered pair of distinct labels is counted twice. The coefficient is exactly one. The goal applies to every finite ensemble with the spectral data above and a full-support output. It does not fix the number of labels or the dimension of the output.

The milestones are the reversal formula (36), the classical-fidelity identities in (38), the unit squared Frobenius norm (40), the diagonal-block expression (41), the off-diagonal trace-norm identity following (42), and the two-block estimate of Lemma 6. They record the paper's mathematical statements and keep the attack path tied to the authors' displayed results.

Significance

The result bounds a measurement's probability of error using only pairwise similarities of the possible output states and their prior probabilities. For nearly distinguishable states, the weighted fidelity sum is small, so this particular measurement succeeds with high probability. The theorem therefore gives a usable guarantee for a specified recovery procedure, rather than only asserting that some procedure exists. In the preprint, §VII, Barnum and Knill describe quantum-information applications of such recovery bounds.

The mathematical result is already proved in the paper, subject to the correction explained below. The formalization work is to make the mixed-state channel, its recovery, the finite-dimensional spectral conventions, and the block-matrix norm estimate precise in Lean. The published Prove2Me definitions for Kraus updates and trace norm supply reusable starting points. A complete proof of this mission would add a checked mixed-state pretty-good-measurement bound; the local statements here compile as open theorems, and no proof is claimed.

Difficulty

The obvious pairwise-overlap estimate does not by itself express the error of the recovery channel. The recovery's classical fidelity is initially a channel evaluation on basis states, while the bound uses trace norms of blocks of a Gram matrix. The key obstacle is controlling the off-diagonal Frobenius mass of the positive square root of that Gram matrix by the trace norms of the corresponding blocks of the Gram matrix itself. Lemma 6 states the needed two-block comparison, including rectangular blocks. The matrix dimension and block labels must remain consistent when it is applied across a larger array.

Formalization scope

All systems and index sets are finite, with matrices over $\mathbb C$ and real probabilities. A general completely positive map is represented by an unbundled finite family of Kraus matrices. The classicizing family has rectangular matrices from the input-label space to the output space; the reversal has matrices in the opposite direction. Composite Kraus families are indexed by pairs. The classical fidelity is defined from the channel action in equation (10); the goal does not define it using the desired overlap bound. The reversal is defined by equation (12) for a general family, so its specialized formula remains a theorem.

The spectral hypotheses include nonnegative probabilities and eigenvalues, unit sums, and orthonormal eigenvectors. Full support of $\rho_{\mathrm{out}}$ is an explicit hypothesis wherever the reversal appears, following page 7. Empty input or output types cannot satisfy the normalized data together with these hypotheses. The Bures–Uhlmann expression is the unsquared trace of a positive square root; using the squared fidelity would change the constant and is outside this mission. Lemma 6 is independent of the ensemble and can be reused for finite block-matrix estimates. Contributions to the spectral identities, the array equalities, and the block-norm argument are welcome.

Equation (39) prints the square of the optimal success probability on its left. The first line of (38) compares that quantity with the recovery fidelity in the opposite direction to Corollary 4. The proof on pages 12–13 concludes the displayed bound for $F_{\mathrm{cl}}(\rho,R_{A,\rho}A)$ . This mission states that proved conclusion and records the printed discrepancy in its item and audit notes.

Selected references

Howard Barnum and Emanuel Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, arXiv:quant-ph/0004088v2, 2000/2026 version. arXiv
Howard Barnum and Emanuel Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, Journal of Mathematical Physics 43 (2002), 2097–2106. DOI

11 thms3 active usersReviewed

Probability Theoretical Computer Science·Captain: mikedeng1

Quantum Amplitude Amplification and Estimation: Est_Amp(A, χ, M) Outputs ã with |ã − a| ≤ 2πk√(a(1−a))/M + k²π²/M² with Probability ≥ 8/π² for k = 1 and > 1 − 1/(2(k−1)) for k ≥ 2Research Paper

Motivation

Many quantum algorithms end in a measurement that succeeds only with some probability $a$ . Two questions follow: how to raise that probability, and how to learn its value. G. Brassard, P. Høyer, M. Mosca and A. Tapp answered both in Quantum Amplitude Amplification and Estimation (arXiv:quant-ph/0005055, 2000; Contemporary Mathematics 305, 2002). Amplitude amplification generalizes Grover's search (Grover 1996) to an arbitrary algorithm $\mathcal A$ and an arbitrary notion of success. Amplitude estimation combines amplification with the quantum Fourier transform to estimate $a$ with error of order $1/M$ after $M$ applications of $\mathcal A$ , where classical sampling needs order $1/M^2$ samples. Quantum counting, quantum Monte Carlo integration (Montanaro 2015) and many quantum speedups for statistics and finance rest on this estimation step.

Timeline:

1996: Grover's search algorithm.
1997: Brassard and Høyer (arXiv:quant-ph/9704027) introduce the amplification operator $\mathbf Q$ for a general algorithm.
1998: Brassard, Høyer and Tapp (arXiv:quant-ph/9805082) give quantum counting.
2000: the paper formalized here presents amplification, estimation and counting in a unified form with explicit constants.

Setting

Let $\mathcal H = \mathbb C^\iota$ be a finite-dimensional Hilbert space with computational basis $\{|x\rangle : x\in\iota\}$ and a distinguished zero state $|0\rangle$ . A quantum algorithm without measurements is a unitary matrix $\mathcal A$ on $\mathcal H$ , and a Boolean function $\chi:\iota\to\{0,1\}$ calls a basis state good when $\chi(x)=1$ . Write $|\Psi\rangle=\mathcal A|0\rangle=|\Psi_1\rangle+|\Psi_0\rangle$ for the splitting into the projections onto the good and the bad subspaces. The initial success probability is $a=\langle\Psi_1|\Psi_1\rangle$ , the probability that measuring $|\Psi\rangle$ gives a good state, and $\theta_a\in[0,\pi/2]$ is the angle with $\sin^2\theta_a=a$ .

The operator $\mathbf S_\chi$ flips the sign of the amplitudes of good states, $\mathbf S_0$ flips the sign of the amplitude of $|0\rangle$ , and the amplification operator is

\mathbf Q=-\mathcal A\,\mathbf S_0\,\mathcal A^{-1}\,\mathbf S_\chi .

For an integer $M\ge1$ , the quantum Fourier transform is $F_M:|x\rangle\mapsto\frac1{\sqrt M}\sum_{y=0}^{M-1}e^{2\pi\imath xy/M}|y\rangle$ , and the controlled power is $\Lambda_M(U):|j\rangle|y\rangle\mapsto|j\rangle U^j|y\rangle$ . The phase state is $|S_M(\omega)\rangle=\frac1{\sqrt M}\sum_y e^{2\pi\imath\omega y}|y\rangle$ , and $d(\omega_0,\omega_1)=\min_{z\in\mathbb Z}|z+\omega_1-\omega_0|$ is the circular distance. The algorithm $\mathbf{Est\_Amp}(\mathcal A,\chi,M)$ applies $(F_M^{-1}\otimes I)\,\Lambda_M(\mathbf Q)\,(F_M\otimes I)$ to $|0\rangle\mathcal A|0\rangle$ , measures the first register to obtain $y\in\{0,\dots,M-1\}$ , and outputs $\tilde a=\sin^2(\pi y/M)$ .

Formalization targets

Goal: Theorem 12 (Amplitude Estimation)

For every positive integer $k$ , the event

|\tilde a-a|\le 2\pi k\frac{\sqrt{a(1-a)}}{M}+k^2\frac{\pi^2}{M^2}

has probability at least $8/\pi^2$ when $k=1$ , and greater than $1-\frac1{2(k-1)}$ when $k\ge2$ . If $a=0$ then $\tilde a=0$ with certainty. If $a=1$ and $M$ is even, then $\tilde a=1$ with certainty.

Milestones, in attack order

Lemma 1: $\mathbf Q$ acts on $|\Psi_1\rangle$ and $|\Psi_0\rangle$ by an explicit $2\times2$ matrix.
Equations (3)–(5): for $0<a<1$ , $|\Psi_\pm\rangle$ are orthonormal eigenvectors of $\mathbf Q$ with eigenvalues $e^{\pm\imath2\theta_a}$ .
Equation (6): $|\Psi\rangle$ in that eigenbasis.
Lemma 7: the error in the angle controls the error in $\sin^2$ .
Lemma 10: the overlap $|\langle S_M(\omega_0)|S_M(\omega_1)\rangle|^2$ .
Theorem 11: the exact law of phase estimation and its two tail bounds.
Two steps of the proof of Theorem 12 (p. 20): the state after $\Lambda_M(\mathbf Q)$ , and the outcome law as an even mixture of two phase-estimation laws.

Further statements from the same development are included as companion targets: the success probability $\sin^2((2m+1)\theta_a)$ after $m$ rounds, Theorem 2 (quadratic speedup), Lemma 5 (the phase-generalized $\mathbf Q$ ), Theorem 13 (counting) and Corollary 14.

Significance

Theorem 12 is the quantitative core of quantum estimation algorithms. Its error bound scales as $1/M$ in the number of applications of $\mathbf Q$ , and that scaling is the quadratic speedup behind quantum counting (Theorem 13), quantum mean estimation, and quantum Monte Carlo methods for option pricing and risk analysis. The exact clauses for $a\in\{0,1\}$ make the estimator usable as a zero-error test for the existence of a good state.

All results here are proved in the paper and widely reproduced in textbooks; none is open. What the mission adds is a machine-checked account with the paper's constants: $8/\pi^2$ , the strict tail bound $1-1/(2(k-1))$ , and the additive term $k^2\pi^2/M^2$ . It also covers every modulus $M\ge1$ , not only powers of two, and arbitrary $\mathcal A$ and $\chi$ , not only uniform search. Related statements are posed on the platform but unproved:

QAlgorithms.Nannicini.amplitudeEstimation_error is the special case $k=1$ , $M=2^m$ , with a bit-string presentation of the algorithm.
QAlgorithms.Nannicini.groverOperator_eigenstates states (3)–(4) for an abstract reflection.
QAlgorithms.DeWolf.amplitudeAmplification covers (8) and the $1-a$ half of Theorem 2.

The Grover theorems already proved on the platform treat a single marked item with a uniform start.

Difficulty

The obvious argument has two parts: $\mathbf Q$ rotates a plane by $2\theta_a$ , and phase estimation reads off $\theta_a$ . Neither part settles the measurement law. The outcome probability is a sum over the second register of the squared amplitudes of an entangled state. Reducing it to two independent phase-estimation laws requires orthonormality of $|\Psi_\pm\rangle$ , and that holds only for $0<a<1$ . The goal does not assume this: the degenerate cases $a\in\{0,1\}$ , where $|\Psi_\pm\rangle$ do not exist, must be handled separately.

On the phase-estimation side, the tail bound for $k\ge2$ must be strict and must hold for every $M\ge1$ . The bound $8/\pi^2$ for $k=1$ relies on a minimization over $\Delta\in[0,1/M]$ that needs $M>2$ , while the goal has no such hypothesis, so the small cases $M\le2$ need their own argument. Finally, the second eigenphase appears as $1-\theta_a/\pi$ , and the matching outcome $M-y$ wraps to $0$ at $y=0$ .

Formalization scope

States are vectors $\iota\to\mathbb C$ over a finite type $\iota$ (the paper writes $\chi:\mathbb Z\to\{0,1\}$ ), operators are matrices, and $\{0,1\}$ is Bool. $\mathcal A$ is assumed unitary and $\mathcal A^{-1}$ is written $\mathcal A^\dagger$ . The second register is Fin M with $M\ge1$ ; $F_M$ is the platform's published Fourier matrix ShorAlgorithms.Shared.fourierMatrix (same sign and normalization as (13)), $F_M^{-1}$ is its conjugate transpose, and $\Lambda_M$ is an explicit matrix on Fin M × ι. The outcome law is the sum over the second register of squared moduli of the final state, and an event's probability is the sum of the outcome probabilities over it. $a$ is computed from $\mathcal A$ , $\chi$ and $|0\rangle$ , and $\theta_a=\arcsin\sqrt a$ . The goal assumes neither $0<a<1$ nor $M>2$ , and it keeps the strict inequality for $k\ge2$ . The step "after step 2, ignoring global phase" is stated with its phase $-\imath$ written out.

A formalization that takes $a$ or $\theta_a$ as a free parameter, assumes the mixture form of the outcome law, or reasons about $|\Psi_\pm\rangle$ without deriving them from $\mathcal A$ and $\chi$ would make the goal trivial. The statements here do none of these: every quantity is computed from $\mathcal A$ , $\chi$ , $|0\rangle$ and $M$ . The clauses "uses exactly $M$ evaluations of $f$ " (Theorem 12) and "requires exactly $\lceil\sqrt N\rceil$ evaluations" (Corollary 14) are not formalized, because the matrix model has no oracle whose calls could be counted. Theorem 13 is stated for any unitary sending $|0\rangle$ to the uniform superposition, which includes $F_N$ , as the paper allows on p. 20.

A complete development needs:

geometric sums of roots of unity;
the Fejér-kernel identity of Lemma 10;
the inequality $\sin x\ge 2x/\pi$ on $[0,\pi/2]$ ;
a bound on $\sum_{j\ge k}1/j^2$ ;
Kronecker-product bookkeeping for two-register states.

The phase-estimation part (Lemma 10, Theorem 11) does not depend on amplification and can be reused by any later formalization of Fourier-based phase estimation. Proofs of individual milestones, and lemmas on Fin M Fourier sums, are welcome.

Selected references

G. Brassard, P. Høyer, M. Mosca, A. Tapp, Quantum Amplitude Amplification and Estimation, in Quantum Computation and Information, Contemporary Mathematics 305, AMS, 2002, pp. 53–74. arXiv:quant-ph/0005055
G. Brassard, P. Høyer, An exact quantum polynomial-time algorithm for Simon's problem, ISTCS 1997. arXiv:quant-ph/9704027
G. Brassard, P. Høyer, A. Tapp, Quantum counting, ICALP 1998. arXiv:quant-ph/9805082
L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. arXiv:quant-ph/9605043
A. Montanaro, Quantum speedup of Monte Carlo methods, Proc. R. Soc. A 471, 2015. arXiv:1504.06987

14 thms3 active usersReviewed

Completed

Linear algebra Numerical Analysis·Captain: mikedeng1

Quantum Algorithm for Systems of Linear Equations with Exponentially Improved Dependence on Precision I: A Truncated Odd Chebyshev Series Is 2ε-Close to 1/x on [−1, −1/κ] ∪ [1/κ, 1]Research Paper

Motivation

The quantum linear systems problem asks, given a sparse Hermitian $N \times N$ matrix $A$ with condition number $\kappa$ and a procedure preparing a state $|b\rangle$ , to prepare a state close to $A^{-1}|b\rangle / \|A^{-1}|b\rangle\|$ . Harrow, Hassidim and Lloyd (2009) gave a quantum algorithm whose running time is polynomial in $\log N$ and $\kappa$ but grows like $1/\varepsilon$ in the target precision $\varepsilon$ , because it estimates eigenvalues by phase estimation. Childs, Kothari and Somma (arXiv:1511.02306, SIAM J. Comput. 46(6), 2017) reduced the precision dependence to $\mathrm{poly}\log(1/\varepsilon)$ , an exponential improvement.

The reduction has two parts. A quantum part implements a linear combination of unitaries applied to $A$ , and turns any function that is $\varepsilon$ -close to $1/x$ on the spectrum of $A$ into an approximate preparation of the solution state (Corollary 10 and Proposition 9 of the paper). An analytic part supplies such a function with small degree and small coefficient weight. The paper gives two analytic constructions: a Fourier expansion (Section 3) and an expansion in Chebyshev polynomials (Section 4). This mission formalizes the analytic core of the Chebyshev construction, the input to the paper's Theorem 4. The quantum algorithms and their query and gate counts are not formalized here.

Setting

For a real number $\kappa \ge 1$ (a condition number: the ratio of the largest to the smallest singular value), the domain is

D_\kappa := [-1, -1/\kappa] \cup [1/\kappa, 1].

A function $g$ is $\varepsilon$ -close to $h$ on a set $D \subseteq \mathbb R$ if $|g(x) - h(x)| \le \varepsilon$ for all $x \in D$ .

The Chebyshev polynomials of the first kind are $\mathcal T_0(x) = 1$ , $\mathcal T_1(x) = x$ and $\mathcal T_{n+1}(x) = 2x\mathcal T_n(x) - \mathcal T_{n-1}(x)$ ; those of the second kind $\mathcal U_n$ satisfy the same recursion with $\mathcal U_0 = 1$ , $\mathcal U_1 = 2x$ .

For natural numbers $b, j$ let

c_{b,j} := \frac{1}{2^{2b}} \sum_{i=j+1}^{b} \binom{2b}{b+i},

the probability of more than $b+j$ heads in $2b$ fair coin flips. The tamed inverse (74) is $f_b(x) = (1 - (1-x^2)^b)/x$ , and the odd Chebyshev series is

S_{b,n}(x) := 4 \sum_{j=0}^{n-1} (-1)^j c_{b,j}\, \mathcal T_{2j+1}(x).

In Lean these are Dκ, coeff b j, fTamed b, and chebSum b n in the namespace QuantumLinSys.Chebyshev; bOf κ ε and j0Of b ε are the parameters $b$ and $j_0$ below.

Formalization targets

Goal: Lemma 14 (p. 16)

With $b = \kappa^2 \log(\kappa/\varepsilon)$ and $j_0 = \sqrt{b\log(4b/\varepsilon)}$ , the truncated series

g(x) = 4\sum_{j=0}^{j_0} (-1)^j c_{b,j}\, \mathcal T_{2j+1}(x)

is $2\varepsilon$ -close to $1/x$ on $D_\kappa$ , for every $\kappa \ge 1$ and $\varepsilon > 0$ .

Milestones, in the order the proof uses them

Lemma 17 (p. 19). For integers $d \ge 1$ and $b \ge (\kappa d)^2\log(\kappa d/\varepsilon)$ , $f_b$ is $\varepsilon$ -close to $1/x$ on $D_{\kappa d}$ .
Lemma 18 (p. 19). On $[-1,1]$ , $f_b = S_{b,b}$ exactly:

\frac{1-(1-x^2)^b}{x} = 4\sum_{j=0}^{b-1}(-1)^j c_{b,j}\,\mathcal T_{2j+1}(x).

Display (89) (p. 21). $c_{b,j} \le e^{-j^2/b}$ .
Lemma 19 (p. 21). The series truncated at $j_0 = \sqrt{b\log(4b/\varepsilon)}$ is $\varepsilon$ -close to $f_b$ on $[-1,1]$ .

Two further statements of the same approach are included as companion theorems: Lemma 16 (p. 17), the closed form of the $n$ -th power of the $2\times 2$ rotation block in terms of $\mathcal T_n$ and $\mathcal U_{n-1}$ , and Proposition 9 (p. 9), the $4\varepsilon$ perturbation bound for normalized states.

Significance

Lemma 14 provides a polynomial of degree $O(\kappa\log(\kappa/\varepsilon))$ whose Chebyshev coefficients have total weight $O(\sqrt{b\log(b/\varepsilon)})$ , approximating $1/x$ uniformly on the region where a well-conditioned matrix has its eigenvalues. Applied to a Hermitian matrix through a quantum walk, whose powers implement $\mathcal T_n$ (Lemma 16), it gives the query complexity $O(d\kappa^2\log^2(d\kappa/\varepsilon))$ of Theorem 4. The same polynomial approximation of $1/x$ reappears in later work on quantum singular value transformation and matrix inversion.

All results of this mission are proved in the paper. None of them is machine-checked in Mathlib or on the platform, as far as a search found: Mathlib has the Chebyshev polynomials and the identity $\mathcal T_n(\cos\theta) = \cos n\theta$ , but no Chebyshev expansion of a rational function, no binomial tail bound in this form, and no approximation theorem for $1/x$ . The formalization produces a checked uniform approximation of $1/x$ with explicit, non-asymptotic parameters.

Difficulty

The exact identity (Lemma 18) has no slack: every coefficient, sign and summation bound of (77) must be right for all $b$ , and an off-by-one in the inner sum or in the Chebyshev index makes it false. Mathlib's Chebyshev library offers evaluation facts but no expansion of a given polynomial in the Chebyshev basis. The bound (89) is a Chernoff–Hoeffding tail bound for a symmetric binomial distribution, which must be stated for sums of binomial coefficients rather than for random variables. The goal then needs both approximation errors at the page's specific parameters, including the corner cases in which $\log(\kappa/\varepsilon)$ or $\log(4b/\varepsilon)$ is negative.

Formalization scope

All functions are real functions of one real variable. Chebyshev polynomials are Mathlib's Polynomial.Chebyshev.T ℝ and Polynomial.Chebyshev.U ℝ, indexed by integers. The sum $\sum_{j=0}^{n-1}$ is over Finset.range n, so the series of (55)/(88) truncated at $j_0$ is chebSum b (j₀ + 1) and the full series (77) is chebSum b b.

The formalization commits to the following conventions, each disclosed in the item it affects.

$\kappa \ge 1$ on every statement that mentions $D_\kappa$ , and $d \ge 1$ in Lemma 17. Below these values the domain is empty or contains $0$ .
$\varepsilon > 0$ . No upper bound on $\varepsilon$ is imposed in this mission.
The paper's real $b = \kappa^2\log(\kappa/\varepsilon)$ is rounded up to a natural number in the goal, and the truncation index $j_0$ is rounded down, the sum running over $j = 0,\dots,\lfloor j_0\rfloor$ .
In Lemmas 17–19 $b$ is a natural number. The page's "integer" exponent cannot be negative without making $(1-x^2)^b$ singular.
At $x = 0$ , $f_b(0)$ is Lean's $0/0 = 0$ , which is the value of its continuous extension. Lemma 18 is therefore stated on all of $[-1,1]$ .
Proposition 9 is stated for continuous linear operators on $\mathbb C^N$ , with $\|C^{-1}\| \le 1$ given as a two-sided inverse of norm at most $1$ , and for unit vectors $\psi$ .

A trivializing reading is ruled out: the goal fixes the page's $b$ , $j_0$ and constant $2\varepsilon$ , so neither an arbitrarily large truncation nor a weaker constant satisfies it, and the domain $D_\kappa$ excludes the origin, where Lean's $1/0 = 0$ would make closeness to $1/x$ meaningless.

Useful infrastructure, reusable beyond this mission: Chebyshev expansions of polynomials on $[-1,1]$ , binomial tail bounds, and uniform approximation of $1/x$ . Contributions of general lemmas of this kind are welcome.

Selected references

A. M. Childs, R. Kothari and R. D. Somma, Quantum algorithm for systems of linear equations with exponentially improved dependence on precision, SIAM J. Comput. 46(6), 2017; arXiv:1511.02306v2. https://arxiv.org/abs/1511.02306
A. W. Harrow, A. Hassidim and S. Lloyd, Quantum algorithm for linear systems of equations, Phys. Rev. Lett. 103, 150502, 2009. https://arxiv.org/abs/0811.3171
D. W. Berry, A. M. Childs and R. Kothari, Hamiltonian simulation with nearly optimal dependence on all parameters, FOCS 2015. https://arxiv.org/abs/1501.01715
W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58, 1963. https://doi.org/10.1080/01621459.1963.10500830

6 thms3 active usersReviewed

Completed

Quantum Gravity·Captain: Alien60

Oreshkov–Costa–Brukner 2012: Quantum Correlations with No Causal OrderResearch Paper

Motivation

In ordinary quantum mechanics, and in quantum field theory on a fixed spacetime, events happen in a definite causal order: an operation either precedes another, follows it, or the two are spacelike separated. Attempts to combine quantum theory with general relativity call this assumption into question. In general relativity the causal structure is dynamical, and a quantum theory of gravity may allow it to be indefinite. Oreshkov, Costa and Brukner (Nat. Commun. 3, 1092 (2012), arXiv:1105.4464) turned this question into a precise mathematical one. They assume that quantum mechanics holds locally in each laboratory and make no assumption about any global causal order. Within that framework they ask which correlations between two laboratories are possible. They find correlations that no definite causal order can produce: these correlations violate a causal inequality, which every causally ordered scenario satisfies.

Timeline.

2005: Hardy proposes probabilistic theories with dynamic causal structure as a framework for quantum gravity (arXiv:gr-qc/0509120).
2009: Chiribella, D'Ariano and Perinotti introduce quantum combs, which describe quantum networks with a fixed causal order (Phys. Rev. A 80, 022339). Chiribella, D'Ariano, Perinotti and Valiron introduce the quantum switch, a superposition of gate orders (arXiv:0912.0195, Phys. Rev. A 88, 022318 (2013)).
2012: Oreshkov, Costa and Brukner define process matrices and the causal inequality $p_{succ} \le 3/4$ . They exhibit a four-qubit process matrix reaching $p_{succ} = (2+\sqrt2)/4$ , and show that classical processes are always causally separable.
2015–2016: Araújo et al. introduce witnesses of causal nonseparability (arXiv:1506.03776). Branciard et al. classify the simplest causal inequalities and their quantum violations (arXiv:1508.01704). Oreshkov and Giarmatzi extend causal separability to more parties (arXiv:1506.05449). Procopio et al. realize the quantum switch with photons (arXiv:1412.4006).

Setting

Alice's laboratory has an input system $A_1$ and an output system $A_2$ , and Bob's has $B_1$ and $B_2$ . All four are finite-dimensional, with dimensions $d_{A_1}, d_{A_2}, d_{B_1}, d_{B_2}$ , and operators on $A_1A_2B_1B_2$ are complex matrices indexed by $(a_1\times a_2)\times(b_1\times b_2)$ .

A local operation of Alice is described by its Choi–Jamiołkowski (CJ) matrix $M^{A_1A_2}$ . The operation is a completely positive trace-preserving (CPTP) map exactly when

M^{A_1A_2} \ge 0, \qquad \operatorname{Tr}_{A_2} M^{A_1A_2} = \mathbb 1^{A_1}.

A process matrix is a matrix $W^{A_1A_2B_1B_2}$ satisfying

W \ge 0,\qquad \operatorname{Tr}\big[W\,(M^{A_1A_2}\otimes M^{B_1B_2})\big] = 1 \ \text{ for all CJ matrices of CPTP maps}

(Eqs. (4)–(5) of the source). The probability of a pair of local outcomes is $P = \operatorname{Tr}[W(M^{A_1A_2}\otimes M^{B_1B_2})]$ (Eq. (3)).

The task (Eq. (1)). Alice, Bob and a second bit for Bob receive independent uniform bits $a$ , $b$ and $b'$ . Alice uses an instrument $\{M^A(x\mid a)\}_x$ to produce a guess $x$ , and Bob uses $\{M^B(y\mid b,b')\}_y$ to produce a guess $y$ . If $b'=0$ Bob must communicate $b$ to Alice, and if $b'=1$ Alice must communicate $a$ to Bob:

p_{succ} = \tfrac12\big[P(x=b\mid b'=0) + P(y=a\mid b'=1)\big].

Causal separability (Eq. (6)). A process matrix of the form $\mathbb 1^{A_2}\otimes W^{A_1B_1B_2}$ allows no signalling from Alice to Bob, written $A\not\preceq B$ . One of the form $\mathbb 1^{B_2}\otimes W^{A_1A_2B_1}$ allows none from Bob to Alice. $W$ is causally separable if $W = q\,W^{B\not\preceq A} + (1-q)\,W^{A\not\preceq B}$ for some $0\le q\le 1$ .

Formalization targets

Goal: violation of the causal inequality

\exists\, W,\ \{M^A(x\mid a)\},\ \{M^B(y\mid b,b')\} \text{ on four qubits}:\quad W \text{ is a process matrix and } p_{succ} > \tfrac34 .

The goal states only that a violation exists, with no hard-coded value. The specific value $(2+\sqrt2)/4$ is a milestone.

Milestones (in source order)

Eq. (2): every causally separable $W$ satisfies $p_{succ} \le 3/4$ , for every choice of local instruments and in every finite dimension.
Eq. (7): the four-qubit matrix

W = \tfrac14\Big[\mathbb 1 + \tfrac{1}{\sqrt2}\big(\sigma_z^{A_2}\sigma_z^{B_1} + \sigma_z^{A_1}\sigma_x^{B_1}\sigma_z^{B_2}\big)\Big]

is a process matrix. 3. Eq. (8): with the instruments of Eqs. (20)–(23), this $W$ gives $p_{succ} = (2+\sqrt2)/4$ , for every state $\rho^{B_2}$ that Bob may prepare. 4. p. 5: the matrix of Eq. (7) is not causally separable. 5. Appendix F: every process matrix that is diagonal in a product basis (a classical process) is causally separable. 6. Appendix C, Fig. 3: for Hermitian $W$ , the normalization condition (5) holds if and only if $\operatorname{Tr}W = d_{A_2}d_{B_2}$ and $W$ has no Hilbert–Schmidt component of type $A_2$ , $B_2$ , $A_1A_2$ , $B_1B_2$ , $A_2B_2$ , $A_1A_2B_2$ , $A_2B_1B_2$ or $A_1A_2B_1B_2$ . 7. Appendix E, Eq. (26): $P(y\mid a,b,b'=1) = \tfrac12\big[1 + (-1)^{y+a}/\sqrt2\big]$ , and $P(x=b\mid b'=0) = (2+\sqrt2)/4$ .

Significance

The result. Milestones 1 and 3 together show that quantum mechanics, applied locally in each laboratory, does not by itself imply a definite causal order. The causal inequality is a device-independent test of causal order, analogous to a Bell inequality for local realism. Milestone 5 shows that indefinite causal order disappears in the classical limit, and the source reads this as a hint that spacetime causal structure may emerge in a quantum-to-classical transition. The process-matrix framework has since become standard for indefinite causal order. Milestone 6 is the characterization that later work on witnesses and causal inequalities relies on.

Formalizing it. All seven milestones and the goal are proved in the source; none are open mathematics. This mission produces machine-checked versions in a common vocabulary: process matrices, CJ instruments, causal separability and Hilbert–Schmidt type analysis. That vocabulary can be reused for later results such as witnesses of causal nonseparability, multipartite causal separability and the quantum switch.

Status honesty. The formal statements are about matrices. Whether causal-inequality violations can occur in nature is not settled. Laboratory realizations of the quantum switch certify causal nonseparability with witnesses, not with a causal-inequality violation, and the source leaves open whether $(2+\sqrt2)/4$ is the largest possible violation.

Difficulty

The violation itself (milestones 2, 3 and 7) is finite linear algebra on $16\times16$ matrices, but the irrational entries $1/\sqrt2$ rule out a purely computational check. Positivity of $W$ is the nontrivial part of milestone 2. The two Pauli strings in $W$ anticommute, which fixes its spectrum, but this has to be turned into a positive-semidefiniteness proof.

Milestone 1 needs more than inspecting the definitions. The bound has to be shown for each no-signalling form separately and then carried through convex mixtures, with instruments of arbitrary dimension.

Milestone 4 is a non-existence statement over all decompositions. A direct search is hopeless; it follows from milestones 1 and 3.

Milestone 5 (Appendix F) is the deepest: it builds the two positive parts of the decomposition by an eigenvalue-shifting procedure.

Milestone 6 needs orthogonality computations with arbitrary Hilbert–Schmidt bases on four tensor factors.

Formalization scope

Representation. Finite index types, complex matrices, and Mathlib's Kronecker product ⊗ₖ with tensor order $(A_1\times A_2)\times(B_1\times B_2)$ . Local operations are represented directly by their CJ matrices, so the transpose in the source's CJ convention never enters the statements. Bits are Bool (false ↦ 0). Probabilities are real parts of traces, which are real whenever all inputs are positive semidefinite.
Definitions. These live in OCB2012_defs: partial trace ptrace₂, IsCPTP_CJ, IsProcessMatrix, prob, IsAliceInstrument, IsBobInstrument, pSucc, the no-signalling forms, IsCausallySeparable, the Pauli matrices, W7, the instruments ξ and η, the structure HSBasis and the predicate AllowedType. Density matrices come from the published PeresTerno.IsDensityMatrix.
Hilbert–Schmidt bases. Milestone 6 quantifies over every basis satisfying the source's conditions: $\sigma_0=\mathbb 1$ , Hermitian, traceless, and $\operatorname{Tr}\sigma_\mu\sigma_\nu = d\,\delta_{\mu\nu}$ . Hermiticity matches the source's use of real coefficients.
Not trivial. Instruments range only over positive semidefinite CJ matrices whose outcome sum is CPTP. The goal, milestones 2–4 and milestone 7 are stated on qubits, so no hypothesis can be vacuous.
Out of scope. The source's derivation of Eq. (2) in Appendix A uses events in a partially ordered causal structure and a free-choice assumption, and it has no faithful matrix-level counterpart. Milestone 1 is the process-matrix form of the bound, which the source applies on p. 4. The closed-timelike-curve model of Appendix D is not formalized.
Contributions welcome. Reusable lemmas on partial traces of Kronecker products, positive semidefiniteness of Pauli-string combinations, and expansions in Hilbert–Schmidt bases.

Selected references

O. Oreshkov, F. Costa, Č. Brukner, Quantum correlations with no causal order, Nat. Commun. 3, 1092 (2012). doi:10.1038/ncomms2076, arXiv:1105.4464
L. Hardy, Probability theories with dynamic causal structure: a new framework for quantum gravity (2005). arXiv:gr-qc/0509120
G. Chiribella, G. M. D'Ariano, P. Perinotti, Theoretical framework for quantum networks, Phys. Rev. A 80, 022339 (2009). arXiv:0904.4483
G. Chiribella, G. M. D'Ariano, P. Perinotti, B. Valiron, Quantum computations without definite causal structure, Phys. Rev. A 88, 022318 (2013). arXiv:0912.0195
M. Araújo, C. Branciard, F. Costa, A. Feix, C. Giarmatzi, Č. Brukner, Witnessing causal nonseparability, New J. Phys. 17, 102001 (2015). arXiv:1506.03776
C. Branciard, M. Araújo, A. Feix, F. Costa, Č. Brukner, The simplest causal inequalities and their violation, New J. Phys. 18, 013008 (2016). arXiv:1508.01704
O. Oreshkov, C. Giarmatzi, Causal and causally separable processes, New J. Phys. 18, 093020 (2016). arXiv:1506.05449
L. M. Procopio et al., Experimental superposition of orders of quantum gates, Nat. Commun. 6, 7913 (2015). arXiv:1412.4006

27 thms3 active usersReviewed

Completed

Mathematical Physics·Captain: Lucas

Drezet 2023: GHZ Bell-Nonlocality in the Everett MultiverseResearch Paper

Motivation

Whether the many-worlds (Everett) interpretation of quantum mechanics is local in the sense of Bell is a recurring question in the foundations of physics. A number of authors have argued that Everett's theory escapes Bell-type nonlocality theorems because it drops the assumption that each measurement has a single outcome. A. Drezet's paper arXiv:2306.07794 (2023) argues against this claim by revisiting the Greenberger–Horne–Zeilinger (GHZ) nonlocality theorem, which, unlike Bell's inequality, uses only probability-one (perfect) correlations. Its central mathematical step, stated in Section II, is that no locally causal beable model can reproduce the quantum predictions for the GHZ state. The paper's argument is that this step makes no assumption about completeness or hidden variables, and so applies to Everett's theory as well.

Timeline:

1964–1976: J. S. Bell introduces Bell inequalities and, in "The theory of local beables" (1976), the notion of local causality phrased with beables $\lambda$ (collected in Speakable and Unspeakable in Quantum Mechanics, 2004).
1989: Greenberger, Horne and Zeilinger give a nonlocality proof for three spin-½ particles that uses no inequality ("Going beyond Bell's theorem").
2015: L. Vaidman discusses the GHZ argument in the many-worlds setting ("Bell inequality and Many-Worlds interpretation").
2023: Drezet's paper, the source of this mission.

Setting

Three spin-½ particles are sent to three distant observers, Alice, Bob and Charlie. Each one measures the spin of their particle along a direction $\hat n_j \in \{\hat x, \hat y\}$ and records an outcome $\alpha, \beta, \gamma \in \{+1, -1\}$ . The particles are prepared in the GHZ state

|\psi\rangle = \tfrac{1}{\sqrt 2}\big(|{+z}\rangle_1|{+z}\rangle_2|{+z}\rangle_3 - |{-z}\rangle_1|{-z}\rangle_2|{-z}\rangle_3\big),

and quantum mechanics predicts the joint outcome probabilities through the Born rule, $P(\alpha,\beta,\gamma\mid\hat n_1,\hat n_2,\hat n_3,\psi) = |\langle \alpha_{\hat n_1},\beta_{\hat n_2},\gamma_{\hat n_3}|\psi\rangle|^2$ . Here $|a_{\hat n}\rangle$ denotes the eigenvector of $\sigma_{\hat n}$ with eigenvalue $a$ . In Lean this is bornProb n₁ n₂ n₃ α β γ.

A locally causal (Bell-local) model consists of

a space $\Lambda$ of beables with a probability distribution $\rho(\lambda)$ that does not depend on the settings (Eq. (18), statistical independence), and
local response probabilities $P_j(\alpha\mid\lambda,\hat n_j)$ , where party $j$ 's outcome depends only on $\lambda$ and its own setting (Eq. (17)).

Such a model predicts

P(\alpha,\beta,\gamma\mid\hat n_1,\hat n_2,\hat n_3) = \int_\Lambda P_1(\alpha\mid\lambda,\hat n_1)\,P_2(\beta\mid\lambda,\hat n_2)\,P_3(\gamma\mid\lambda,\hat n_3)\,d\rho(\lambda).

In Lean the model is a LocalCausalModel Λ and its prediction is M.predict. The beables are arbitrary: $\lambda$ may be a hidden variable, or the quantum state itself as in the Beltrametti–Bugajski representation, Eq. (15).

Formalization targets

Goal (Section II, Eqs. (10)–(27))

No locally causal model reproduces the quantum predictions on the four GHZ settings $(\hat x,\hat x,\hat x)$ , $(\hat x,\hat y,\hat y)$ , $(\hat y,\hat x,\hat y)$ , $(\hat y,\hat y,\hat x)$ :

\neg\Big(\forall\,\text{GHZ settings } \hat n,\ \forall \alpha,\beta,\gamma:\ P^{\mathrm{model}}(\alpha,\beta,\gamma\mid\hat n) = P^{\mathrm{Born}}(\alpha,\beta,\gamma\mid\hat n,\psi)\Big).

Milestones

Eqs. (2)–(5). $\sigma_x^{(1)}\sigma_x^{(2)}\sigma_x^{(3)}|\psi\rangle = -|\psi\rangle$ , and the three $\sigma_x\sigma_y\sigma_y$ -type operators fix $|\psi\rangle$ .
Born probabilities (Section III, Eqs. (30)–(32)). For $(\hat x,\hat x,\hat x)$ each outcome triple has probability $1/4$ if $\alpha\beta\gamma=-1$ and $0$ otherwise. For the other three GHZ settings the same holds with $\alpha\beta\gamma=+1$ .
Eqs. (10)–(13). No assignment $A_j, B_j \in\{\pm1\}$ satisfies all four GHZ constraints.
Eqs. (19)–(27). If a product of three probability distributions on $\{\pm1\}$ vanishes off the set $\{\alpha\beta\gamma = s\}$ , then each factor is a point mass, and the three atoms multiply to $s$ .
Section II, summary (ii). A locally causal model that reproduces the GHZ predictions is, for $\rho$ -almost every $\lambda$ , deterministic, with values satisfying (10)–(13).
Section III (B). Local causality implies non-signalling.
Eq. (29). Quantum non-signalling for the GHZ state, with Alice's marginal $P_1(\pm1\mid\hat x,\psi)=\tfrac12$ .
Appendix 3, Eqs. (39)–(45). Keeping Eq. (17) but letting the beable density depend on the settings (a "superdeterministic" model) does reproduce the GHZ predictions.

Significance

The goal theorem is the mathematical core of the paper's conclusion that any beable account of the GHZ correlations, including one where $\lambda$ is just the quantum state, violates Bell's local causality. Milestones 6–8 formalize the paper's separation of notions of locality: non-signalling holds both in quantum mechanics and in every locally causal model, so it cannot tell them apart; and dropping statistical independence (Eq. (18)) is enough to reproduce the correlations. The GHZ theorem itself has been known since 1989. As far as the drafter is aware it has no machine-checked formalization on this platform, and this mission provides one, stated for general measurable beable spaces.

Difficulty

The combinatorial core (milestone 3) is a parity argument. The substance lies in the steps that connect it to probability: showing that perfect correlations force determinism almost surely when $\rho$ is an arbitrary probability measure (null sets, measurability, integrals of nonnegative functions), and computing the Born probabilities exactly in Lean from explicit matrices and eigenvectors.

Formalization scope

Outcomes are elements of ℤˣ (exactly $\{+1,-1\}$ ). Settings form a two-element type Setting with values x and y. Qubit index 0 is $|{+z}\rangle$ and index 1 is $|{-z}\rangle$ . Three-qubit operators are Kronecker products.
A LocalCausalModel Λ has a probability measure ρ on a measurable space Λ and measurable response functions P j λ n α with values in $[0,1]$ that sum to one over $\alpha$ . The fixed state $\psi$ is left implicit. Predictions are Bochner integrals, and all integrands are bounded and measurable.
The goal quantifies over all such models on all measurable spaces. Its hypothesis is the equality of all $4\times 8$ predicted and Born probabilities. Because it uses the actual Born probabilities rather than an arbitrary list of constraints, it cannot hold vacuously.
Needed infrastructure: finite-dimensional matrix computations over $\mathbb C$ with $\sqrt2$ , and basic measure theory (a.e. vanishing of nonnegative integrands).

Selected references

A. Drezet, An Elementary Proof That Everett's Quantum Multiverse Is Nonlocal: Bell-Locality and Branch-Symmetry in the Many-Worlds Interpretation, arXiv:2306.07794, 2023. https://arxiv.org/abs/2306.07794
D. M. Greenberger, M. A. Horne, A. Zeilinger, Going beyond Bell's theorem, in Bell's Theorem, Quantum Theory and Conceptions of the Universe, Kluwer, 1989, pp. 69–72. https://arxiv.org/abs/0712.0921
J. S. Bell, Speakable and Unspeakable in Quantum Mechanics, 2nd ed., Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511815676

11 thms3 active usersReviewed

Complexity Theory Probability Theoretical Computer Science·Captain: mikedeng1

Strengths and Weaknesses of Quantum Computing I: Relative to a Random Oracle, a Quantum Algorithm Needs Ω(2^{n/2}) Queries to Decide Whether 1ⁿ Has a PreimageResearch Paper

Motivation

Grover's algorithm (Grover 1996) finds a marked item among $N$ with $O(\sqrt N)$ queries, a quadratic speed-up over any classical algorithm. Whether quantum computers can do substantially better on search, and so solve NP-type problems by brute force in polynomial time, was settled in the negative by Bennett, Bernstein, Brassard and Vazirani (arXiv:quant-ph/9701001, SIAM J. Comput. 26(5), 1997): relative to a random oracle, a quantum algorithm needs $\Omega(2^{n/2})$ queries to decide whether a string has a preimage. The bound matches Grover's algorithm up to a constant factor, and its hybrid argument is one of the two standard lower-bound methods of the field, together with the polynomial method (Beals et al. 1998) and the adversary method (Ambainis 2000).

Timeline:

1996: Grover's algorithm searches $N$ items with $O(\sqrt N)$ queries.
1997: the paper proves $\mathbf{BQTime}(o(2^{n/2})) \not\supseteq \mathbf{NP}$ relative to a random oracle with probability 1 (Theorem 3.5), and the $\Omega(2^{n/3})$ bound for random permutations (Theorem 3.6).
1998: Boyer, Brassard, Høyer and Tapp give tight bounds for quantum searching.
1999: Zalka shows Grover's algorithm is exactly optimal.

Setting

A $T$ -query algorithm acts on vectors $\varphi \in \mathbb{C}^{(X \cup \{\bot\}) \times R \times W}$ , where $X$ is the set of query strings, $R$ the set of answers (an additive group) and $W$ a finite workspace. A basis configuration $(x, z, w)$ with $x \in X$ is querying $x$ ; $(\bot, z, w)$ is not querying. For an oracle $f : X \to R$ the oracle operator is

O_f\,|x, z, w\rangle = |x, z + f(x), w\rangle, \qquad O_f\,|\bot, z, w\rangle = |\bot, z, w\rangle .

The algorithm consists of a unit vector $\varphi_0$ , unitaries $U_0, \dots, U_{T-1}$ that do not depend on the oracle, and a set of accepting configurations. With oracle $A$ its states are $\varphi_{i+1} = U_i O_A \varphi_i$ ; the acceptance probability is the squared norm of the accepting part of $\varphi_T$ . The query magnitude of $y$ in $\varphi$ is $q_y(\varphi) = \sum_{z, w} |\varphi(y, z, w)|^2$ (Definition 3.2). The algorithm decides a property if it accepts with probability at least $2/3$ when the property holds and at most $1/3$ when it fails.

In the main theorem $X = R = \{0,1\}^n$ with bitwise addition, and the oracle is a uniformly random function $A : \{0,1\}^n \to \{0,1\}^n$ . The question is whether $1^n$ belongs to $\mathcal{L}_A = \{y : \exists x\ A(x) = y\}$ .

Formalization targets

Goal: Theorem 3.5 (finite form)

\exists\, c > 0\ \exists N\ \forall n \ge N\ \forall M \text{ with } T \le c\, 2^{n/2} \text{ queries}: \quad \Pr_A\bigl[M^A \text{ fails to decide } \exists x\ A(x) = 1^n\bigr] \ge \tfrac18 .

The constant is existential, matching the theorem's hypothesis $T(n) = o(2^{n/2})$ ; $c$ and $N$ do not depend on the workspace or the algorithm.

Milestones

Theorem 3.1: unit vectors at distance $\varepsilon$ have measurement distributions within total variation $4\varepsilon$ .
Theorem 3.3 (corrected): changing oracle answers on time–string pairs of total query magnitude $\le \varepsilon^2/T$ moves the final state by at most $2\varepsilon$ .
Corollary 3.4 (corrected): outside a set of at most $4T^2/\varepsilon^2$ strings, changing the oracle at one string moves the final state by at most $\varepsilon$ .
$\Pr[1^n \text{ has no preimage}] = ((2^n-1)/2^n)^{2^n} \ge 1/4$ .
$\Pr[1^n \text{ has a unique preimage}] = ((2^n-1)/2^n)^{2^n-1} \ge 1/e$ .
Final states within $1/13$ for $A$ and $A_y$ force failure on one of them.
The double counting: failing oracles with a unique preimage are at least half the successful oracles with none.

Significance

The theorem shows that the quadratic speed-up of Grover's algorithm cannot be improved for unstructured search, and that relative to a random oracle $\mathbf{NP} \not\subseteq \mathbf{BQP}$ ; any quantum algorithm for NP-complete problems must use the structure of the problem. Theorem 3.3 and Corollary 3.4 isolate the constraint unitary evolution places on "quantum parallelism" and are reused across quantum lower bounds, including the permutation bound of the companion mission (Theorem 3.6).

The results are proved on paper and, to our knowledge, have no machine-checked proof. The mission produces a formal query model with an XOR oracle, a formal hybrid argument, and the lower bound with its constants checked. Two printed bounds are wrong by constant factors (below); the formal statements carry the corrected constants, and a formal proof settles them. Grover's matching upper bound is on the platform as Grover.search_succeeds_bounded, for a phase oracle and one fixed algorithm.

Difficulty

The obvious argument — each query reveals one bit about where the preimage is, so $\Omega(2^n)$ queries are needed — fails for quantum algorithms, which query all strings in superposition at once. The difficulty is to bound how much a superposition of queries can learn, which requires controlling the accumulated effect of small changes across $T$ unitary steps, and then converting a bound on states into a statement about the probability of failure over random oracles, where the set of sensitive strings depends on the oracle.

Formalization scope

The paper's oracle quantum Turing machines are replaced by the query model above, the model its proofs use. Every oracle QTM running $T$ steps is a $T$ -query algorithm: oracle answers on lengths other than $n$ are fixed and absorbed into the unitaries, as the proof fixes them, and the input $1^n$ is absorbed into $\varphi_0$ . Queries return the full value $A(x) \in \{0,1\}^n$ ; one Boolean query is two full-value queries, so the goal implies the Boolean-oracle bound with $c$ halved. Strings are Fin n → ZMod 2; states are EuclideanSpace ℂ (Option X × R × W); probabilities over oracles are counting fractions over all $(2^n)^{2^n}$ functions; total variation distance is the paper's $\sum_x |\mathcal D(x) - \mathcal D'(x)|$ without the factor $1/2$ .

Corrections: Theorem 3.3 is printed with conclusion $\le \varepsilon$ , which fails (one query string, $T = 1$ , distance $2$ at $\varepsilon = 1$ ; machine-checked); the true bound is $2\varepsilon$ . Corollary 3.4 is printed with $|S| \le 2T^2/\varepsilon^2$ , which fails (16 strings, $T = 1$ , $\varepsilon = 0.45$ ); the true bound is $4T^2/\varepsilon^2$ . The printed constant $T(n) \le 2^{n/2}/20$ in the proof of Theorem 3.5 does not support the step $2^n - \mathrm{card}(S) \ge 2^{n-1}$ even with the paper's own count; the goal states an existential constant, and $c = 1/37$ works with the corrected Corollary 3.4. The closing probability- $1$ argument over countably many machines and the class statement about $\mathbf{BQTime}$ are not formalized.

A formalization in which algorithms query at every step on every branch (no $\bot$ sector), only one side of the bounded-error condition is tested, or the probability is taken over a set of oracles that excludes the hard instances, proves a weaker theorem and is ruled out by these definitions.

Needed infrastructure: norms of finite-dimensional complex vectors, unitaries as linear isometry equivalences, finite counting of functions. The query model and the hybrid argument are reusable for any quantum query lower bound.

Selected references

C. H. Bennett, E. Bernstein, G. Brassard, U. Vazirani, Strengths and weaknesses of quantum computing, SIAM J. Comput. 26(5):1510–1523, 1997. arXiv:quant-ph/9701001
L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. arXiv:quant-ph/9605043
M. Boyer, G. Brassard, P. Høyer, A. Tapp, Tight bounds on quantum searching, Fortschr. Phys. 46, 1998. arXiv:quant-ph/9605034
C. Zalka, Grover's quantum searching algorithm is optimal, Phys. Rev. A 60, 1999. arXiv:quant-ph/9711070
R. Beals, H. Buhrman, R. Cleve, M. Mosca, R. de Wolf, Quantum lower bounds by polynomials, J. ACM 48, 2001. arXiv:quant-ph/9802049
A. Ambainis, Quantum lower bounds by quantum arguments, J. Comput. Syst. Sci. 64, 2002. arXiv:quant-ph/0002066

9 thms3 active usersReviewed

Information Theory Theoretical Computer Science·Captain: mikedeng1

Shadow Tomography of Quantum States 3: Shadow Tomography Needs Ω(min{D², log M}/ε²) CopiesResearch Paper

Why count copies of a quantum state

A mixed state of a $D$ -dimensional quantum system is a $D\times D$ positive semidefinite matrix $\rho$ of trace $1$ . Writing $\rho$ down takes about $D^2$ real numbers, and $D$ is exponential in the number of qubits, so learning $\rho$ in full is expensive. Holevo's theorem and the random access code bounds of Ambainis, Nayak, Ta-Shma and Vazirani say that an $n$ -qubit state carries far fewer usable classical bits than its $2^n$ amplitudes suggest. Shadow tomography, introduced by S. Aaronson (arXiv:1711.01053), makes this quantitative: given $M$ known two-outcome measurements $E_1,\dots,E_M$ , how many copies of an unknown $\rho$ are needed to estimate every acceptance probability $\operatorname{Tr}(E_i\rho)$ to within $\varepsilon$ ?

Aaronson shows that $\widetilde O(\log^4 M\cdot\log D/\varepsilon^4)$ copies suffice, polylogarithmic in $M$ and $D$ . The question this mission addresses is the converse: how many copies are necessary. Section 6 of the paper proves two lower bounds. Theorem 16 gives $\Omega(\min\{D,\log M\}/\varepsilon^2)$ even when $\rho$ and the $E_i$ are diagonal (a classical distribution). Theorem 19, the goal here, strengthens the dimension term to $D^2$ for genuinely quantum states.

Timeline:

2016: full tomography of a $D$ -dimensional state to trace-distance accuracy $\varepsilon$ needs $\Theta(D^2/\varepsilon^2)$ copies up to logarithmic factors, with upper and lower bounds by O'Donnell and Wright (arXiv:1508.01907) and Haah, Harrow, Ji, Wu and Yu (arXiv:1508.01797).
2017–2018: Aaronson poses shadow tomography (Problem 1), proves the polylogarithmic upper bound (Theorem 2), and proves the lower bounds of Theorems 16 and 19.
2020 onward: classical shadows (Huang, Kueng and Preskill, arXiv:2002.08953) and later shadow-tomography algorithms study the same estimation task with other measurement models and improved upper bounds.

Setting

Fix a dimension $D$ . A two-outcome measurement is a $D\times D$ Hermitian matrix $E$ with $0\preceq E\preceq I$ ; it accepts $\rho$ with probability $\operatorname{Tr}(E\rho)$ . The tensor power $\rho^{\otimes k}$ is the $D^k\times D^k$ matrix of $k$ independent copies. A strategy using $k$ copies is a measurement of $\rho^{\otimes k}$ with finitely many outcomes $\omega\in\Omega$ , given by positive semidefinite matrices $\Pi_\omega$ with $\sum_\omega\Pi_\omega = I$ , together with outputs $b(\omega)=(b_1(\omega),\dots,b_M(\omega))$ . It succeeds on $\rho$ when, with probability at least $2/3$ over $\omega$ , $|b_i(\omega)-\operatorname{Tr}(E_i\rho)|\le\varepsilon$ for every $i\in[M]$ .

The proof works with these further objects, all defined in the mission:

an orthogonal projection $\mathbb P$ onto an $N/2$ -dimensional subspace of $\mathbb C^N$ (Hermitian, idempotent, trace $N/2$ );
$\rho_{\mathbb P} := \tfrac2N\mathbb P$ , the maximally mixed state on that subspace;
$\sigma_{\mathbb P,\varepsilon} := (1-6\varepsilon)\,\mathbb I/N + 6\varepsilon\,\rho_{\mathbb P}$ ;
the von Neumann entropy in bits, $S(\rho) = -\sum_x\lambda_x\log_2\lambda_x$ over the eigenvalues of $\rho$ ;
for states $\sigma_1,\dots,\sigma_K$ and $\zeta := \tfrac1K\sum_i\sigma_i^{\otimes T}$ , the quantum mutual information with the classical index, $I(\zeta;i) := S(\zeta) - \tfrac1K\sum_i S(\sigma_i^{\otimes T})$ .

Formalization targets

Goal: Theorem 19 (p. 23)

There are a universal constant $c>0$ and a threshold $N_0$ such that for all $D\ge N_0$ , all $M$ with $\log_2 M\ge N_0^2$ and all $0<\varepsilon\le\tfrac16$ , some measurements $E_1,\dots,E_M$ on $\mathbb C^D$ force every strategy that succeeds on every mixed state to use

k \;\ge\; c\,\frac{\min\{D^2,\ \log_2 M\}}{\varepsilon^2}

copies. The goal fixes only the shape $\Omega(\min\{D^2,\log M\}/\varepsilon^2)$ , not a constant, so a sharper constant does not invalidate it.

Milestones (pp. 23–24)

The milestones follow the proof, which sets $N:=\lfloor\min\{D,\sqrt{\log_2 M}\}\rfloor$ and $K:=\lfloor c^{N^2}\rfloor$ :

Eq. (2): for some $c\in(1,2)$ and all large even $N$ there are $K$ projections $\mathbb P_i$ of rank $N/2$ with $|\operatorname{Tr}(\mathbb P_i\rho_j)-\tfrac12|\le\tfrac1{12}$ for all $i\ne j$ .
$\operatorname{Tr}(\mathbb P_i\sigma_i) = \tfrac12+3\varepsilon$ .
$|\operatorname{Tr}(\mathbb P_j\sigma_i)-\tfrac12| = 6\varepsilon|\operatorname{Tr}(\mathbb P_j\rho_i)-\tfrac12|\le\tfrac\varepsilon2$ for $i\neq j$ .
The exact entropy $S(\sigma_i) = \log_2 N - [1-h(\tfrac12+3\varepsilon)]$ , with $h$ the binary entropy, and the bound $S(\sigma_i)\ge\log_2 N - C\varepsilon^2$ .
$I(\zeta;i)\le T(\log_2 N - S(\sigma_i))$ when all $\sigma_i$ have equal entropy.

Significance

Theorem 19 shows that the $\log M$ dependence of shadow tomography cannot be removed, and that for $M\ge 2^{D^2}$ shadow tomography is as hard as full tomography: as $M$ grows the bound becomes the $\Omega(D^2/\varepsilon^2)$ tomography lower bound, which it therefore contains. Compared with the classical Theorem 16, it shows that quantum states need quadratically more copies in the dimension term. The $1/\varepsilon^2$ factor matches the upper bound of Proposition 20 for the decision version, so the $\varepsilon$ -dependence of the lower bound is tight in that setting.

The results are proved in the paper; none of them has a machine-checked proof that we know of. Formalizing the argument requires von Neumann entropy and its additivity on tensor products, the bound $S\le\log_2(\text{dimension})$ , a Holevo-plus-Fano step that turns successful estimation into mutual information, and the existence of many nearly orthogonal half-dimensional subspaces. Each is reusable well beyond this mission.

Difficulty

The obvious attempt adapts the classical argument of Theorem 16, which hides $K$ subsets of $[N]$ in a biased distribution. Quantum states allow $\exp(\Omega(N^2))$ hidden subspaces instead of $\exp(\Omega(N))$ subsets, which is where $D^2$ comes from, but two steps change character. First, the hiding family must be shown to exist: Eq. (2) is a concentration statement for random subspaces, and the lemma the paper cites for it (Lemma 18) is misstated, as explained below. Second, the information bound must be carried out for quantum states: the step "learning $i$ from $\zeta$ requires $I(\zeta;i)\ge\log_2 K$ " needs Holevo's bound and Fano's inequality, adjusted for success probability $2/3$ rather than certainty.

Formalization scope

Matrices are Matrix n n ℂ over a finite index type; the goal uses $n=\texttt{Fin } D$ . Conventions committed to:

A mixed state is the published WildeQIT.IsDensityOperator (positive semidefinite, trace $1$ ), reused as a reference item.
A strategy is a finite-outcome POVM on $\rho^{\otimes k}$ , indexed by Fin k → Fin D, with deterministic outputs $b(\omega)\in\mathbb R^M$ ; classical randomness can be absorbed into the outcome set.
Probabilities and traces are real parts of complex traces. Entropies use $\log_2$ ; Lean's $\log_2 0 = 0$ gives $0\log 0=0$ , and vnEntropy returns $0$ on non-Hermitian matrices, which no statement uses.
Added to the goal: the threshold $N_0$ on $D$ and $\sqrt{\log_2 M}$ (for $D=1$ , $k=0$ succeeds) and $\varepsilon\le\tfrac16$ (for $\varepsilon\ge\tfrac12$ , the output $b_i=\tfrac12$ succeeds with $k=0$ ). Problem 1's $b_i\in[0,1]$ is dropped, an equivalent statement under clipping.
The measurements are chosen before the strategy (for every strategy, the same $E$ ), which is the meaning of a lower bound.

A trivializing formalization is ruled out: the goal does not mention $N$ , $K$ , $\mathbb P_i$ , $\sigma_i$ or $\zeta$ , the success condition quantifies over all mixed states rather than a vacuous class, and the measurements are fixed before the strategy.

Not drafted:

Lemma 18 (pp. 22–23) is false as printed. Since $\mathbb E_S[\rho_S] = \mathbb I/N$ , $\operatorname{Tr}(\mathbb P_T\rho_S)$ concentrates at $1/2$ , not $1/4$ . The proof needs only Eq. (2), which is centred correctly and is a milestone.
Eq. (2) is stated as existence, not as "probability $1-o(1)$ over Haar-random subspaces", because Mathlib has no Haar measure on the unitary group or the Grassmannian; existence is what the proof uses.
" $I(\zeta;i)$ must be at least $\log_2 K$ " is not drafted: as stated it is imprecise for success probability $2/3$ , and the correct Holevo–Fano form is left to the solver.
The final combination $I(\zeta;i)=O(T\varepsilon^2)$ , $T=\Omega(N^2/\varepsilon^2)$ is the goal's last step.

Contributions welcome: proofs of the milestones; a Haar-measure version of Eq. (2); von Neumann entropy infrastructure (additivity, the dimension bound, concavity); Holevo's bound and Fano's inequality for finite-dimensional states.

Selected references

S. Aaronson, Shadow Tomography of Quantum States, arXiv:1711.01053v2, 2018; STOC 2018. https://arxiv.org/abs/1711.01053
P. Hayden, D. Leung, A. Winter, Aspects of generic entanglement, Comm. Math. Phys. 265, 2006. https://arxiv.org/abs/quant-ph/0407049
R. O'Donnell, J. Wright, Efficient quantum tomography, STOC 2016. https://arxiv.org/abs/1508.01907
J. Haah, A. W. Harrow, Z. Ji, X. Wu, N. Yu, Sample-optimal tomography of quantum states, IEEE Trans. Inf. Theory 63, 2017. https://arxiv.org/abs/1508.01797
A. Ambainis, A. Nayak, A. Ta-Shma, U. Vazirani, Dense quantum coding and quantum finite automata, J. ACM 49, 2002. https://arxiv.org/abs/quant-ph/9804043
H.-Y. Huang, R. Kueng, J. Preskill, Predicting many properties of a quantum system from very few measurements, Nature Physics 16, 2020. https://arxiv.org/abs/2002.08953

16 thms3 active usersReviewed

Completed

Information Theory Statistics·Captain: mikedeng1

Shadow Tomography of Quantum States 2: Even the Classical Special Case Needs Ω(min{D, log M}/ε²) CopiesResearch Paper

Why the copy count matters

Shadow tomography asks for predictions of many specified measurements of an unknown quantum state, while using as few prepared copies of that state as possible. The requested output is a list of acceptance probabilities, not a full description of the state. A procedure might exploit the fact that these are only $M$ numbers, even when the state has dimension $D$ . The natural question is how far this saving can go. Aaronson's paper gives upper bounds and separates two sources of difficulty: one already present for ordinary probability distributions, and one arising from noncommuting quantum measurements.

This mission concerns the first source. It formalizes Theorem 16, which says that even when the state and every requested measurement are diagonal in the same basis, the number of copies must grow with $\min\{D,\log M\}/\varepsilon^2$ in the relevant asymptotic regime. In that special case, the unknown state is an ordinary distribution on $D$ outcomes. The theorem therefore puts a limit on any proposed improvement to shadow tomography that would promise fewer copies in all instances.

States, measurements, and estimates

A mixed state $\rho$ on a $D$ -dimensional system is a positive semidefinite $D\times D$ complex matrix with trace one. A two-outcome measurement is represented by an effect $E$ satisfying $0\preceq E\preceq I$ ; it accepts $\rho$ with probability $\operatorname{Tr}(E\rho)$ . When $\rho$ is diagonal, its diagonal entries are the probabilities of the $D$ basis outcomes. When $E$ is diagonal too, it specifies a randomized yes-or-no test on those outcomes. These conventions are stated in Section 3 of the paper.

Given effects $E_1,\ldots,E_M$ , a shadow-tomography strategy measures $k$ independent copies $\rho^{\otimes k}$ and outputs estimates $b_1,\ldots,b_M$ . It succeeds on $\rho$ when every estimate differs from $\operatorname{Tr}(E_i\rho)$ by at most $\varepsilon$ . The lower bound requires success probability at least $2/3$ for every diagonal mixed state. The strategy may make a joint quantum measurement on all copies and may choose its estimates from its observed outcome. This is the same measurement model used in Problem 1.

Formalization targets

Classical special-case lower bound

The goal is the classical clause of Theorem 16. There are absolute constants $c>0$ and $N_0$ such that, for $D\ge N_0$ , $\log_2 M\ge N_0$ , and $0<\varepsilon\le1/6$ , there are $M$ diagonal effects with 0/1 entries, corresponding to the known Boolean functions in Section 6.1, for which every strategy successful on all diagonal states must use

k\ge c\,\frac{\min\{D,\log_2 M\}}{\varepsilon^2}.

The hard measurements are chosen before the strategy is quantified. The statement therefore also rules out a strategy with a smaller copy count that works uniformly for all quantum states and measurements. Its constants and threshold express the $\Omega$ notation in Theorem 16, rather than specifying a numerical optimum.

Supporting targets

Four milestones come from the proof on pages 20–21: the high-probability overlap bound for independently chosen half-size subsets (Eq. (1)); the acceptance probability of a subset under its associated biased distribution; an upper bound on the mutual information between the hidden subset index and the observed samples; and the exact entropy formula with a quadratic entropy deficit. These statements expose the combinatorial and information-theoretic parts of the lower bound while leaving the goal as the paper's copy-complexity result.

What the result supplies

Theorem 16 sets a floor for shadow tomography that survives even when all operators commute. Any uniform copy bound for the full quantum task must respect this floor. The result also distinguishes the difficulty of predicting many properties of a distribution from the extra difficulty possible for noncommuting states and measurements, which the paper treats in a separate lower bound. Section 6 presents both bounds.

A complete formalization would give machine-checked statements and proofs for the finite subset construction, the entropy calculation, the information inequality, and the reduction from a successful quantum measurement procedure on diagonal states to a lower bound on $k$ . The theorem is proved on paper; these draft statements are open Lean goals and do not claim that its proof has been machine checked. The finite-distribution and information-theory infrastructure is reusable for other lower bounds based on hidden-index families.

Where the argument is delicate

Counting how many possible measurements there are does not by itself show that samples reveal enough about which distribution generated them. The lower bound needs a quantitative relation between estimation accuracy and information about a hidden index, while each individual sample carries limited information. The paper's printed overlap condition (1) is too weak for the next displayed $\varepsilon/2$ estimate: at its boundary it gives $\varepsilon$ . The milestone preserves Eq. (1) as printed; closing the goal requires the correspondingly sharper overlap fact with $N/24$ , which follows from the same type of concentration statement after adjusting its constant. The printed assertion that learning the index requires mutual information at least $\log_2 K$ is also imprecise at success probability $2/3$ ; a quantitative decoding inequality is needed. Neither incorrect display is a draft milestone.

Formalization scope

Matrices are indexed by Fin D. WildeQIT.IsDensityOperator supplies the mixed-state predicate $\rho\succeq0$ and $\operatorname{Tr}(\rho)=1$ . Diagonal states and effects use the standard matrix diagonal predicate. An effect is positive semidefinite together with its complement. The tensor power uses functions Fin k → Fin D as basis indices; at $k=0$ it is a one-by-one identity matrix. A strategy is a finite-outcome POVM on that tensor power, followed by a real estimate vector for each outcome. The output values are not restricted to $[0,1]$ : clipping them to this interval cannot worsen an estimate of a probability. No restriction to classical estimators is placed in the goal; that would change the allowed strategies before the theorem has been proved.

The asymptotic threshold excludes the one-dimensional and single-measurement corners where the claimed rate does not describe the problem. The bound $\varepsilon\le1/6$ keeps the biased distributions used on page 20 nonnegative; $\varepsilon\ge1/2$ would permit a zero-copy constant estimate. Subset milestones require even $N$ or explicitly require a half-size subset, so $N/2$ has its intended meaning. The natural logarithm appears nowhere in the lower-bound rate; entropy, mutual information, and $\log_2 M$ use base two. At zero probability the entropy convention is $0\log 0=0$ .

The finite distributions, entropy, conditional entropy, and mutual information reuse the published WildeQIT definitions. Contributions that prove the four source milestones, establish the sharper overlap fact, or supply the quantitative decoding step are welcome. The goal must retain its order of quantifiers: one hard measurement family, then every strategy, with success demanded on every diagonal state.

Selected references

Scott Aaronson, Shadow Tomography of Quantum States, arXiv preprint arXiv:1711.01053v2, 2018. Preprint.

14 thms3 active usersReviewed

Completed

Number Theory Probability Theoretical Computer Science·Captain: mikedeng1

Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer 3: The Success Probability of Quantum Order FindingResearch Paper

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

prepares $\frac{1}{q^{1/2}}\sum_{a=0}^{q-1}|a\rangle|x^a \bmod n\rangle$ (eq. (5.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)),
measures, obtaining some $|c, y\rangle$ ,
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,

\Pr\bigl[\text{the observed } c \text{ gives us } r\bigr] \;=\; \sum_{c\ \text{gives}\ r}\ \sum_{y \in \mathbb{Z}/n} |\Psi(c, y)|^2 \;\ge\; \frac{\varphi(r)}{3r},

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

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$ .
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$ .
Eq. (5.13). If $n^2 \le q$ , at most one fraction with denominator below $n$ lies within $1/2q$ of $c/q$ .
p. 1500. Such a fraction is a convergent of the continued fraction of $c/q$ .
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

12 thms3 active usersReviewed

Completed

Mathematical Physics Theoretical Computer Science·Captain: Lucas

Undecidability of the Spectral GapResearch Paper

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

H^{\Lambda(L)} \;=\; \sum_{\text{horizontal edges}} h_{\mathrm{row}}^{(i,j)} \;+\; \sum_{\text{vertical edges}} h_{\mathrm{col}}^{(i,j)} \;+\; \sum_{k\in\Lambda(L)} h_1^{(k)},

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$ ,

h_1(n)=\alpha(n)\Pi,\qquad h_{\mathrm{col}}(n)=D+\beta D',

h_{\mathrm{row}}(n)=A+\beta\Bigl(A'+e^{i\pi\varphi}B+e^{-i\pi\varphi}B^{\dagger}+e^{i\pi 2^{-|\varphi|}}C+e^{-i\pi 2^{-|\varphi|}}C^{\dagger}\Bigr),

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.

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).
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.
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.
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.
Operator norms are $\ell_2$ operator norms; the local interaction strength is the maximum of the three.
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

20 thms3 active usersReviewed

Completed

Captain: Henry Yuen

Parallel repetition for quantum gamesResearch Paper

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

\{A_a^x\}_{a\in A} \qquad\text{and}\qquad \{B_b^y\}_{b\in B}

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

\operatorname{Re}\operatorname{Tr}\!\left(\rho\,(A_a^x\otimes B_b^y)\right).

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

V(x_i,y_i,a_i,b_i)=1

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

\omega^*(G^n)\le e^{-c_G n}

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:

\omega^*(G)<1 \quad\Longrightarrow\quad \lim_{n\to\infty}\omega^*(G^n)=0.

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

\omega^*(G^n)\le Cn^{-\alpha}.

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

\omega^*(G^n)\le C e^{-cn}.

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.

10 thms3 active usersReviewed

Graph Theory Quantum Error Correction·Captain: mikedeng1

Quantum Tanner Codes 1: On a Ramanujan Left-Right Cayley Complex with Robust Dual Tensor Codes, the Quantum Tanner Code Has Rate at Least (1−2ρ)² and Distance at Least δn/(4Δ^{3/2+ε})Research Paper

Why quantum Tanner codes matter

An error-correcting code protects information by adding redundancy. A quantum code must also account for two kinds of errors, commonly called $X$ and $Z$ errors. Quantum low-density parity-check codes use checks that each touch only a bounded number of qubits, while each qubit participates in only a bounded number of checks. Such locality matters when the number of qubits grows. For years it was difficult to make both the number of encoded qubits and the minimum distance proportional to the block length while retaining bounded-weight checks. Leverrier and Zémor's quantum Tanner construction gives a route through local codes placed on an expanding square complex; its main distance theorem is the target of this mission Leverrier and Zémor, 2022.

The construction combines two earlier ingredients. Left-right Cayley complexes provide the squares and expansion properties used by the code Dinur, Evra, Livne, Lubotzky, and Mozes, 2021. Robustness of a dual tensor code, including after puncturing coordinates, controls local words Panteleev and Kalachev, 2021. The paper states the local reduction property as Theorem 1 and derives the rate and distance bounds as Theorem 17. This mission formalizes that implication under the paper's stated component-code and expansion conditions; the separate random-code result that supplies robust examples belongs to the second mission of this series.

The square complex and its codes

Let $G$ be a finite group and let $A,B\subseteq G$ be inverse-closed sets, each of size $\Delta$ . The total no-conjugacy condition says $ag\ne gb$ for every $a\in A$ , $b\in B$ , and $g\in G$ . Vertices are two copies of the group, $V=G\times\{0,1\}$ . A square associated with $v=(g,i)$ and $(a,b)\in A\times B$ has vertices $v$ , $(ag,1-i)$ , $(gb,1-i)$ , and $(agb,i)$ . The set of squares is $Q$ , and a binary word on $Q$ has length $n=|Q|$ . At a vertex $v$ , the incident squares are indexed by $A\times B$ ; this indexing makes the local view $x_v$ of a word $x\in\mathbb F_2^Q$ an $A\times B$ matrix Leverrier and Zémor, §§3.2 and 4.1.

A binary linear code $C_A$ has coordinates indexed by $A$ , and $C_B$ has coordinates indexed by $B$ . Their tensor code $C_A\otimes C_B$ consists of matrices whose columns lie in $C_A$ and whose rows lie in $C_B$ . The dual tensor code $C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B$ is the sum of the column and row codes. In Definition 5, it is $w$ -robust when every member of weight at most $w$ is supported on a union of few rows and columns, with the bounds determined by the two component minimum distances. Definition 8 requires this property after deleting up to $p$ coordinates from each side. These are conditions on all relevant codewords and all permitted puncturings, including the unpunctured pair Leverrier and Zémor, pp. 15–16.

The two Tanner codes are $\mathcal C_0=T(\mathcal G^\square_0,(C_A\otimes C_B)^\perp)$ and $\mathcal C_1=T(\mathcal G^\square_1,(C_A^\perp\otimes C_B^\perp)^\perp)$ . Here $\mathcal G^\square_i$ is the square-adjacency graph on the vertices in copy $i$ . Together they define the quantum CSS code $\mathcal Q=(\mathcal C_0,\mathcal C_1)$ . Its dimension counts encoded qubits. Its distance is the smaller of the minimum weights in $\mathcal C_0\setminus\mathcal C_1^\perp$ and $\mathcal C_1\setminus\mathcal C_0^\perp$ Leverrier and Zémor, pp. 14, 18.

Formalization targets

The goal is Theorem 17. Fix $0<\rho<1/2$ , $0<\varepsilon<1/2$ , $1/2+\varepsilon<\gamma<1$ , and $\delta>0$ . For sufficiently large $\Delta$ , take a left-right Cayley complex satisfying total no-conjugacy and the paper's Ramanujan conditions. Require $0<\dim C_A\le\rho\Delta$ , $\dim C_B=\Delta-\dim C_A$ , minimum distance at least $\delta\Delta$ for $C_A,C_B$ and both duals, and $\Delta^{3/2-\varepsilon/2}$ robustness with $\Delta^\gamma$ resistance to puncturing for both relevant dual tensor codes. The target is

k\ge (1-2\rho)^2 n,\qquad d\ge \frac{\delta n}{4\Delta^{3/2+\varepsilon}}.

The milestones mirror the paper's route to this result. Lemma 4 bounds the nontrivial eigenvalues of the union and square graphs. Propositions 6 and 7 turn dual-tensor robustness into a decomposition and a $3/2$ closeness bound. Theorem 1 supplies a weight-reducing local codeword for every sufficiently light nonzero Tanner-code word. Display (5) supplies the dimension lower bound. Theorem 17 combines the two distance directions with that rate estimate Leverrier and Zémor, pp. 12, 15–16, 18–23.

What the result supplies

The lower bound on $k$ ensures a positive fraction of qubits can carry logical information when $\rho<1/2$ . The lower bound on $d$ rules out small undetectable logical errors. For a fixed allowable degree $\Delta$ , both bounds scale linearly with $n$ . The paper also shows that random component codes can satisfy the robustness assumptions; that probabilistic result is a separate formalization target Leverrier and Zémor, Theorems 9 and 17.

A checked development would make explicit how the square indexing, duals, punctured codes, and CSS quotient fit together. The source proves the mathematical result; the statements here remain open Lean theorems. Reusable contributions include the tensor-code interface, spectral bounds for the graph construction, and lemmas connecting local views to the global Tanner codes. A proof of the existence of infinite Ramanujan complex families is outside this mission's stated target.

Where the proof is difficult

A light global codeword need not have a local view that is itself close to a tensor-code word. Some square-graph vertices have unusually large local weight, and puncturing is needed to isolate coordinates shared with those exceptional vertices. The paper's small-set expansion estimates and robustness conditions control those interactions. Simply averaging local weights does not yield the weight-reducing local codeword asserted by Theorem 1 Leverrier and Zémor, §4.2.

Formalization scope

Words are functions into ZMod 2, codes are submodules, and a matrix is a function on $A\times B$ with $A$ indexing rows. The square coordinates are four-element vertex sets. The construction uses $V=G\times\operatorname{Fin}(2)$ and counts $n$ as the number of squares rather than building $n=\Delta^2|G|/2$ into a definition. The minimum distance of the zero code is infinity, and robustness uses inequalities involving that extended value. Powers of $\Delta$ and the parameters $w,p$ are real; the paper uses integer $w,p$ in Definition 8, while the theorem's power thresholds need real comparisons. The formal robustness predicate includes Definition 5's range $0\le w\le\Delta^2$ ; the theorem thresholds satisfy it for sufficiently large $\Delta$ . These conventions are recorded with each item.

The goal quantifies over every finite complex satisfying inverse closure, total no-conjugacy, and Ramanujan conditions, with a uniform threshold $\Delta_0$ chosen before the group and codes. This pins the complexes in the cited infinite family without formalizing their existence. In particular, the goal contains no auxiliary set or local reduction assumption that could make the distance bound immediate. The published CodingTheory and TillichZemor.HGP.Setting definitions supply dual codes and CSS dimension; the paper-specific setting supplies the square complex, local views, Tanner codes, and robustness. Contributions that keep these conventions and close any milestone theorem are welcome.

Selected references

A. Leverrier and G. Zémor, Quantum Tanner codes, arXiv preprint, 2022. arXiv:2202.13641v3.
I. Dinur, S. Evra, R. Livne, A. Lubotzky, and S. Mozes, Locally Testable Codes with constant rate, distance, and locality, arXiv preprint, 2021. arXiv:2111.04808.
P. Panteleev and G. Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, arXiv preprint, 2021. arXiv:2111.03654.

9 thms2 active usersReviewed

Completed

Mathematical Physics Probability·Captain: mikedeng1

Quantum Speedup of Monte Carlo Methods 2: Along a B-Chebyshev Cooling Schedule, Consecutive Gibbs Sample States Overlap with |⟨π_i|π_{i+1}⟩|² ≥ 1/BResearch Paper

Motivation

Approximating a partition function $Z(\beta)=\sum_{x\in\Omega}e^{-\beta H(x)}$ is a central task in statistical physics and in counting: it covers the Ising and Potts models, and, at $\beta=\infty$ , counting the zero-energy configurations of a Hamiltonian, for instance the proper $k$ -colourings of a graph. Computing $Z(\infty)$ exactly is #P-complete in many cases, so the goal is an estimate $\widetilde Z$ with $|\widetilde Z-Z(\infty)|\le\epsilon Z(\infty)$ with high probability.

The standard classical approach writes $Z(\infty)$ as a telescoping product of ratios $\alpha_i=Z(\beta_{i+1})/Z(\beta_i)$ along a sequence of inverse temperatures $0=\beta_0<\beta_1<\dots<\beta_\ell=\infty$ , and estimates each ratio by sampling from the Gibbs distribution $\pi_i$ at $\beta_i$ . Dyer and Frieze (1992, as cited on p. 14 of arXiv:1504.06987v3) showed how to bound the number of samples when each estimator has bounded relative second moment; Štefankovič, Vempala and Vigoda (J. ACM 2009) named the resulting condition a Chebyshev cooling schedule and showed that schedules of length $\widetilde O(\sqrt{\log|\Omega|})$ exist and can be found efficiently.

Montanaro (arXiv:1504.06987v3, 2017) gives a quantum algorithm for this problem that improves the dependence on $\epsilon$ and on the relaxation time $\tau$ of the underlying Markov chains quadratically. Its quantum sampling step rests on a theorem of Wocjan and Abeyesinghe (Phys. Rev. A 78, 042336, 2008): a sequence of coherent quantum sample states can be prepared efficiently if consecutive states overlap by at least a constant. This mission formalizes the paper's own link between the two: a Chebyshev cooling schedule produces exactly such overlaps.

Setting

Let $\Omega$ be a finite set of configurations and $H:\Omega\to\{0,1,\dots,n\}$ an integer-valued Hamiltonian. Inverse temperatures range over $[0,\infty]$ . The partition function is

Z(\beta)=\sum_{x\in\Omega}e^{-\beta H(x)},

with the convention $e^{-\infty\cdot h}=1$ if $h=0$ and $0$ otherwise, so that $Z(0)=|\Omega|$ and $Z(\infty)$ counts the configurations with $H(x)=0$ .

A cooling schedule is a sequence $0=\beta_0<\beta_1<\dots<\beta_\ell=\infty$ . Along it, the Gibbs distributions are $\pi_i(x)=e^{-\beta_iH(x)}/Z(\beta_i)$ , the ratios are $\alpha_i=Z(\beta_{i+1})/Z(\beta_i)$ , and the estimators are the random variables $Y_i(x)=e^{-(\beta_{i+1}-\beta_i)H(x)}$ , whose mean under $\pi_i$ is $\alpha_i$ .

Definition 1 (Chebyshev cooling schedule). The schedule is a $B$ -Chebyshev cooling schedule for $Z$ if for every $i=0,\dots,\ell-1$

\frac{Z(2\beta_{i+1}-\beta_i)\,Z(\beta_i)}{Z(\beta_{i+1})^2}\le B.

The chi-squared divergence of $\nu$ from $\pi$ is $\chi^2(\nu,\pi)=\sum_x\pi(x)\big(\nu(x)/\pi(x)-1\big)^2$ , and the quantum sample of a distribution $\pi$ is the unit vector $|\pi\rangle=\sum_{x\in\Omega}\sqrt{\pi(x)}\,|x\rangle$ of $\ell^2(\Omega;\mathbb C)$ . In Lean these are Z, gibbs, alpha, Y, IsCoolingSchedule, IsChebyshevSchedule, chiSq and qsample in the namespace QuantumMC.Cooling.

Formalization targets

Goal: overlap of consecutive quantum samples

For every $B$ -Chebyshev cooling schedule and every $i\in\{0,\dots,\ell-1\}$ ,

|\langle\pi_i|\pi_{i+1}\rangle|^2\ge\frac1B.

The statement fixes no value of $B$ and no length $\ell$ ; it is the shape in which the paper feeds the schedule into the quantum sampling theorem, with overlap parameter $p=1/B$ .

Milestones

The second form of the divergence: $\chi^2(\nu,\pi)=\sum_x\nu(x)^2/\pi(x)-1$ for probability vectors with $\pi>0$ .
Display (1): $\chi^2(\pi_{i+1},\pi_i)=Z(\beta_i)Z(2\beta_{i+1}-\beta_i)/Z(\beta_{i+1})^2-1$ , including the last step $\beta_{i+1}=\infty$ .
Along a $B$ -Chebyshev schedule, $\chi^2(\pi_{i+1},\pi_i)\le B-1$ for all $i$ .
For distributions $\nu$ and $\pi>0$ : $1/\sqrt{\chi^2(\nu,\pi)+1}\le\sum_x\nu(x)\sqrt{\pi(x)/\nu(x)}=\langle\nu|\pi\rangle$ .

Companion statements

The classical facts of §3–3.1 that motivate Definition 1: $\mathbb E_{\pi_i}[Y_i]=\alpha_i$ ; $\mathbb E[Y_i^2]/\mathbb E[Y_i]^2=Z(2\beta_{i+1}-\beta_i)Z(\beta_i)/Z(\beta_{i+1})^2$ ; the telescoping product $Z(\beta_\ell)=Z(\beta_0)\prod_i\alpha_i$ with $Z(\beta_0)=|\Omega|$ ; $\operatorname{Var}(Y_i)/\mathbb E[Y_i]^2\le B$ ; and the accuracy claim that ratio estimates within relative error $\epsilon/(2\ell)$ , each failing with probability at most $1/(4\ell)$ , give $|\widetilde Z-Z(\infty)|\le\epsilon Z(\infty)$ with probability at least $3/4$ for $\epsilon<1$ .

Significance

The result. The overlap bound is the hypothesis of the Wocjan–Abeyesinghe theorem (Theorem 9 of the paper) and is used in the proof of the paper's partition-function theorem (Theorem 11). It explains why a cooling schedule built for a classical estimator, with no reference to quantum states, is also good enough for quantum annealing-style state preparation. The paper remarks that, unlike the classical analysis of Štefankovič, Vempala and Vigoda, which needs the reverse divergence $\chi^2(\pi_i,\pi_{i+1})$ and a reversed schedule, the overlap is symmetric in $i$ and $i+1$ , so no reversal is needed.

Formalizing it. The result is proved on paper; nothing in it has been machine-checked. A formal development pins down the treatment of the endpoint $\beta_\ell=\infty$ , where $\pi_\ell$ is supported on the ground states and is no longer strictly positive, and records exactly which positivity conditions the divergence identities require. The definitions of Gibbs distributions, cooling schedules and $\chi^2$ on a finite space are reusable for other analyses of simulated annealing and of partition-function estimation.

Difficulty

The algebra at finite temperatures is a direct computation. The step that needs care is the last one, $i=\ell-1$ : there $\beta_{i+1}=\infty$ , the weights $e^{-\infty\cdot H(x)}$ are indicator values, $2\beta_{i+1}-\beta_i$ is again $\infty$ , and the divergence identity must hold with $\pi_{i+1}$ vanishing on every configuration of positive energy. A formalization that replaces $\infty$ by a large finite inverse temperature, or that requires both distributions to be strictly positive, does not cover this step. The second point is the passage from a bound on the divergence to a bound on an inner product of quantum states, which must handle the configurations where $\nu(x)=0$ .

Formalization scope

Inverse temperatures are elements of $[0,\infty]$ (ℝ≥0∞); the Boltzmann weight branches on $\beta=\infty$ . The differences $\beta_{i+1}-\beta_i$ and $2\beta_{i+1}-\beta_i$ are truncated subtractions in $[0,\infty]$ , exact on a cooling schedule. A schedule is a map $\mathbb N\to[0,\infty]$ of which only $\beta_0,\dots,\beta_\ell$ matter, and "for all $i$ " ranges over $i=0,\dots,\ell-1$ . $H$ takes values in $\mathbb N$ with $H\le n$ . Quantum samples are vectors of EuclideanSpace ℂ Ω with real amplitudes, and $|\langle\cdot|\cdot\rangle|^2$ is the squared norm of the complex inner product.

Added hypotheses, all disclosed in the statements: some configuration has $H(x)=0$ , so that $Z(\infty)>0$ (without it $\pi_\ell$ and the last ratio of Definition 1 are divisions by zero, which Lean evaluates to $0$ ); the general divergence statements assume $\pi(x)>0$ , which the paper's displays use implicitly by dividing by $\pi(x)$ . No hypothesis is placed on $B$ . In the accuracy companion, the per-ratio guarantee is stated as a bound on the failure probability; neither measurability nor independence is assumed.

A goal that assumes $\chi^2(\pi_{i+1},\pi_i)\le B-1$ , assumes $B>0$ in a way that excludes the endpoint, or drops the step $\beta_\ell=\infty$ would be a different, weaker statement; the goal's only hypothesis on the schedule is Definition 1.

Not formalized: the quantum walk algorithms, the Wocjan–Abeyesinghe theorems (Theorems 9 and 10), the sample and step counts of Theorems 8 and 11 (stated in $O(\cdot)$ notation), and the existence of short Chebyshev cooling schedules.

Contributions welcome: proofs of the milestones and of the companions, and lemmas on Gibbs distributions at $\beta=\infty$ that the companions share.

Selected references

A. Montanaro, Quantum speedup of Monte Carlo methods, Proc. R. Soc. A 471:20150301, 2015; cited here as the preprint arXiv:1504.06987v3, 2017. https://arxiv.org/abs/1504.06987
D. Štefankovič, S. Vempala, E. Vigoda, Adaptive simulated annealing: a new connection between sampling and counting, J. ACM 56(3):18, 2009. https://arxiv.org/abs/cs/0612058
P. Wocjan, A. Abeyesinghe, Speedup via quantum sampling, Phys. Rev. A 78:042336, 2008. https://arxiv.org/abs/0804.4259
P. Wocjan, C.-F. Chang, D. Nagaj, A. Abeyesinghe, Quantum algorithm for approximating partition functions, Phys. Rev. A 80:022340, 2009. https://arxiv.org/abs/0811.0596
M. Szegedy, Quantum speed-up of Markov chain based algorithms, FOCS 2004, 32–41. https://arxiv.org/abs/quant-ph/0401053

6 thms2 active usersReviewed

Linear algebra Optimization Theoretical Computer Science·Captain: mikedeng1

Optimization by Decoded Quantum Interferometry 2: With an Imperfect Decoder and Uniform v, 𝔼_v⟨f⟩ ≥ wᵀ[A − 2ε(m+1)]w / Σ_k w_k²(1 − ε_k) for max-XORSATResearch Paper

Motivation

A max-XORSAT instance asks for a binary assignment that satisfies as many parity constraints as possible. A matrix specifies the parity check in each constraint, while a second binary vector specifies the desired parity. The objective can be written as the number of satisfied constraints minus the number violated, so an assignment with a high objective value is also a good approximate solution. Jordan and coauthors study decoded quantum interferometry (DQI), a way to sample candidate assignments by encoding a weighted superposition of error patterns and then decoding their syndromes. Their ideal-state analysis assumes that low-weight errors have distinct syndromes. Real decoders can succeed on many errors even when this uniqueness condition fails, which makes the theorem in this mission relevant to the algorithmic regime beyond the guaranteed decoding radius. Jordan et al., §§8.1 and 10.

The paper's 2024 preprint introduced DQI for linear constraint satisfaction and related optimization problems. Its revised 2025 version studies the effect of decoder failures on the measured objective in Theorem 10.1. This mission uses that revision, arXiv:2408.08292v5, and isolates the first inequality of equation (172). The same section supplies explicit identities for the norm of the postselected state and for its objective matrix, making the theorem a bounded campaign of finite combinatorics and linear algebra. Jordan et al., §10, pp. 35–43.

Setting

Fix integers $m,n\ge0$ and a binary matrix $B\in\mathbb F_2^{m\times n}$ . Its $i$ th row defines a parity $b_i\cdot x$ of an assignment $x\in\mathbb F_2^n$ . For a binary vector $v\in\mathbb F_2^m$ , the objective is

f_v(x)=\sum_{i=1}^{m}(-1)^{b_i\cdot x+v_i}.

An error pattern $y\in\mathbb F_2^m$ has syndrome $B^\top y$ and Hamming weight $|y|$ . The weight- $k$ shell $E_k$ contains all errors with $|y|=k$ . Choose $0\le\ell\le m$ and real weights $w_0,\ldots,w_\ell$ . The ideal syndrome-space state in equation (140) sums $(-1)^{v\cdot y}|B^\top y\rangle$ over each $E_k$ , multiplied by $w_k/\sqrt{\binom m k}$ . Jordan et al., equations (140) and (171).

A deterministic decoder $\mathrm{dec}:\mathbb F_2^n\to\mathbb F_2^m$ guesses an error from its syndrome. It correctly identifies $y$ when $\mathrm{dec}(B^\top y)=y$ . Write $D_k\subseteq E_k$ for the correctly identified errors and $F_k=E_k\setminus D_k$ for the failures. The shell failure rate is $\varepsilon_k=|F_k|/\binom m k$ , and $\varepsilon=\max_{0\le k\le\ell}\varepsilon_k$ . Postselecting successful decoding leaves the unnormalized state $\widetilde P_D(f)$ formed by replacing each $E_k$ in the ideal state with $D_k$ . Apply the binary Hadamard transform, divide by the resulting norm, measure $x$ , and evaluate $f_v(x)$ . Denote this measured expectation by $\langle f_v\rangle$ . Jordan et al., §10.3, pp. 39–40.

Formalization targets

Theorem 10.1: the averaged objective

Let $N=\sum_{k=0}^{\ell}w_k^2(1-\varepsilon_k)$ be the squared norm of the postselected state. The goal, for $N>0$ and uniform $v\in\mathbb F_2^m$ , is

\mathbb E_v\langle f_v\rangle\ge \frac{w^\top A^{(m,\ell,0)}w-2\varepsilon(m+1)w^\top w}{N}.

The matrix $A^{(m,\ell,0)}$ is the symmetric tridiagonal matrix in equation (70): its diagonal is zero and its entries adjacent to the diagonal are $a_k=\sqrt{k(m-k+1)}$ . This is the first inequality of (172), with the decoder's actual failure fractions in $N$ and the worst shell failure rate in the correction. It has no minimum-distance hypothesis. Jordan et al., Theorem 10.1, pp. 39–40.

Supporting targets

The milestone list includes the norm identity of Lemma 10.4, the ideal and postselected objective matrices of Lemmas 10.2 and 10.5, the normalized expectation identity in (179), the averaged matrix identities of Lemmas 10.3 and 10.6, and the error-matrix bound of Lemma 10.7. A separate companion item records the second comparison printed in (172) under an explicit sign condition; without that condition, the printed comparison can fail. Jordan et al., §10, pp. 36–43.

Significance

The result assigns a quantitative cost to decoding errors. It says how the measured max-XORSAT objective changes when some error patterns are lost during postselection, while permitting a code whose low-weight errors share syndromes. Consequently the theorem addresses the setting in which practical decoding succeeds often but exact distance-based uniqueness is unavailable. The denominator also records the survival probability of the weighted state, so the bound keeps the actual normalization visible. Jordan et al., §10, pp. 35 and 39–43.

A complete formalization would provide reusable definitions for binary syndrome decoding, shellwise failure rates, real-amplitude states, normalized measurement expectations, and finite objective matrices. The paper proves the result on paper; this mission asks for machine-checked proofs of the stated goal and its milestones. The formal development would also document exactly which part of equation (172) requires an additional sign assumption. No proof is claimed by the draft statements themselves.

Difficulty

When two errors have the same syndrome, the ideal syndrome state can combine their amplitudes, so its norm need not equal $w^\top w$ . Postselection changes which errors remain, and the measured objective depends on the normalized state for each $v$ . Replacing that normalized expectation with the objective of an average state would change the claim. The proof must keep the decoder fixed while $v$ varies and must control the error matrix uniformly over every real weight vector. The printed second inequality of (172) adds a separate sign issue: a smaller positive denominator reverses the expected comparison when the numerator is negative. Jordan et al., equations (161), (171)–(172), (179)–(182).

Formalization scope

Lean uses ZMod 2 for bits, Fin m and Fin n for zero-based coordinates, functions for binary vectors, and Matrix for $B$ . The decoder is one function of the syndrome, independent of $v$ . Hamming shells, correct and failed decoding sets, and $\varepsilon_k$ are computed from that function. Weights and amplitudes are real. The postselected state uses the factor $1/\sqrt{\binom m k}$ ; the Hadamard transform uses $1/\sqrt{2^n}$ . The average over $v$ is the sum over all $2^m$ vectors divided by $2^m$ . The tridiagonal entries compute $m-k$ in the reals, preserving the square-root formula at the boundary.

Two domain conditions are made explicit. The bound $\ell\le m$ rules out absent weight shells, for which Lean would otherwise assign zero to division by $\binom m k=0$ . The condition $N>0$ rules out a zero postselected state, whose normalized expectation would likewise be assigned a meaningless zero by total real division. The goal ranges over every binary matrix, every fixed deterministic decoder, and every real weight vector satisfying those conditions. It states the expectation of the explicit postselected state after a Hadamard transform, rather than an unconstrained expectation variable.

The supporting development needs finite character sums, Hamming-shell cardinalities, matrix quadratic forms, and an operator bound for a symmetric real matrix. These components can serve other finite decoding and quantum-state calculations. Contributions proving the seven cited milestones or the goal are within scope. The circuit's resource accounting, asymptotic equation (173), and numerical decoder studies are outside this mission.

Selected references

S. P. Jordan, N. Shutty, M. Wootters, A. Zalcman, A. Schmidhuber, R. King, S. V. Isakov, T. Khattar, and R. Babbush, Optimization by Decoded Quantum Interferometry, arXiv:2408.08292v5, 2025 revision of the 2024 preprint. arXiv

10 thms2 active usersReviewed

Optimization Theoretical Computer Science·Captain: mikedeng1

A Quantum Approximate Optimization Algorithm Applied to a Bounded Occurrence Constraint Problem II: For Random Signs the QAOA Expectation Concentrates Above (1/2 + sin γ cos^(3D) γ/2)mResearch Paper

Motivation

The Quantum Approximate Optimization Algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028) prepares a parametrized quantum state whose measurement yields a candidate solution of a combinatorial optimization problem. Its level-one version alternates a single phase operator and a single mixing operator and is simple enough to analyse by hand. In arXiv:1412.6062 the same authors applied it to Max E3LIN2 with bounded occurrence: given linear equations mod 2, each on exactly three bits, with every bit in at most $D+1$ equations, satisfy as many equations as possible. A uniformly random string satisfies half of them in expectation; the question is by how much an algorithm can beat $\tfrac12$ .

Without the occurrence bound no efficient algorithm achieves $\tfrac12+\epsilon$ unless P = NP (Håstad, J. ACM 2001). With every bit in at most $D+1$ equations the history, as recounted on pp. 2–3 of the paper, is:

2000: Håstad gave a classical algorithm with approximation ratio $\tfrac12+\Omega(1/D)$ (Inf. Process. Lett. 74).
2001: Trevisan showed that an efficient algorithm achieving $\tfrac12+c/D^{1/2}$ for a sufficiently large constant $c$ would imply P = NP (STOC).
2014: the first version of this paper showed that the level-one QAOA satisfies at least $\big(\tfrac12+\tfrac1{22D^{3/4}}\big)m$ equations.
2015: Barak et al. gave an efficient classical algorithm reaching $\big(\tfrac12+\Omega(D^{-1/2})\big)m$ on every instance (arXiv:1505.03424); the second version of this paper improved the QAOA worst-case bound to $\big(\tfrac12+\tfrac1{101D^{1/2}\ln D}\big)m$ (Section II).

Section III, formalized here, studies the typical case: it fixes the triples and draws the right-hand sides at random, and shows that the QAOA then reaches an advantage of order $D^{-1/2}$ , the order of the classical algorithm, on all but a vanishing fraction of the instances.

Setting

An instance on $n$ bits with $m$ equations is a list of triples $(a_i,b_i,c_i)$ with $a_i<b_i<c_i$ , no triple repeated, together with right-hand sides $r_i\in\{0,1\}$ ; equation $i$ is $x_{a_i}+x_{b_i}+x_{c_i}\equiv r_i\pmod 2$ . The instance has occurrence at most $D+1$ if every bit lies in at most $D+1$ triples. Write $z_v=(-1)^{x_v}$ and $d_i=(-1)^{r_i}$ ; equation $i$ is satisfied by $x$ exactly when $z_{a_i}z_{b_i}z_{c_i}=d_i$ .

Let $C(x)$ be the number of equations satisfied by $x$ , viewed as a diagonal operator on the $2^n$ -dimensional space spanned by $|x\rangle$ , let $B=\sum_v X_v$ , and let $|s\rangle$ be the uniform superposition. For angles $\gamma,\beta$ the level-one QAOA state is

|\gamma,\beta\rangle=e^{-i\beta B}e^{-i\gamma C}|s\rangle .

Measuring it in the computational basis gives a string; $N(\gamma,\beta)=\sum_x|\langle x|\gamma,\beta\rangle|^2C(x)$ is the expected number of satisfied equations.

In Section III the triples are fixed and the instance is drawn uniformly from the $2^m$ choices of right-hand sides; $\mathbb E_d$ and $\mathrm{Var}_d$ denote the mean and variance over this choice. The mixing angle is $\beta=\pi/4$ and the state analysed is $|-\gamma,\pi/4\rangle$ , following the paper's sign convention.

For an equation with bits $1,2,3$ , the polynomial $c_\rho(z)=\sum d_{\rho ab}z_az_b$ collects the equations that share exactly the bit $\rho$ with it, and $D_\rho$ is its number of terms.

Formalization targets

Goal: concentration above the mean bound

For every E3LIN2 family of $m$ triples with occurrence at most $D+1$ , every $\gamma\in[0,\pi/2]$ and every $t>0$ ,

\Pr_d\Big[N(-\gamma,\pi/4)\le\frac m2+\frac m2\sin\gamma\cos^{3D}\gamma-t\Big]\le\frac{m(6D+3)(D+1)}{4t^2}.

With $t=c\sqrt m$ and $D$ fixed, all but a fraction $(6D+3)(D+1)/(4c^2)$ of the instances reach $\big(\tfrac12+\tfrac12\sin\gamma\cos^{3D}\gamma\big)m-c\sqrt m$ . This is the paper's closing sentence of Section III with an explicit failure probability.

Milestones

(55): $N(-\gamma,\pi/4)=\tfrac m2+\sum_i\tfrac12d_i\langle Z_{a_i}Z_{b_i}Z_{c_i}\rangle$ .
(25): the single-clause term equals $\tfrac18d\,\mathbb E_z\big[\sum_{\pm}\sin(\gamma(d\pm c_1\pm c_2\pm c_3))\big]$ over four sign patterns.
(47): averaging over the clause's own sign gives $\tfrac12\sin\gamma\,\mathbb E_z[\cos\gamma c_1\cos\gamma c_2\cos\gamma c_3]$ .
(48): $\mathbb E_d[\cos\gamma c_\rho(z)]=(\cos\gamma)^{D_\rho}$ for every $z$ .
(49): $\mathbb E_d$ of the clause term is $\tfrac12\sin\gamma(\cos\gamma)^{D_1+D_2+D_3}$ , with $D_1+D_2+D_3\le3D$ .
(50): for $\gamma\in[0,\pi/2]$ , $\tfrac m2\sin\gamma\cos^{3D}\gamma\le\mathbb E_d[N-\tfrac m2]\le\tfrac m2\sin\gamma$ .
(57): clause terms whose (25) expressions share no sign are uncorrelated.
Linked count: each equation is linked to at most $(6D+3)(D+1)$ equations.
Variance: $\mathrm{Var}_d\,N(-\gamma,\pi/4)\le\tfrac14m(6D+3)(D+1)$ .
(51)–(53): $D^{1/2}\sin\gamma_D\cos^{3D}\gamma_D\to1/\sqrt{3e}$ at $\gamma_D=1/\sqrt{3D}$ .

Significance

The result shows that on random-sign instances with any fixed bounded-occurrence structure, a single layer of QAOA beats a random assignment by $\Theta(D^{-1/2})m$ , the same order as the best known classical guarantee and better than the paper's own worst-case bound by a logarithmic factor. It was one of the first concrete performance statements for the QAOA on a problem where its advantage over random guessing could be compared with the best classical guarantee. The average-case technique, an exact single-clause formula followed by an average over independent signs and a dependency count, applies to other local constraint problems.

The statements are proved in the paper by hand; none of them, and no QAOA performance bound, has a machine-checked proof on the platform. The mission produces a verified link from the quantum state to a classical average (25), a finite second-moment method over sign vectors, and an explicit Chebyshev form of the concentration claim.

Difficulty

The central step is (25): turning the expectation of $Z_aZ_bZ_c$ in the state $e^{-i\beta B}e^{-i\gamma C}|s\rangle$ into a classical average over bits. It requires conjugating three Pauli operators through the mixer at $\beta=\pi/4$ , expanding the phase operator around the three bits, and showing that equations sharing two bits with the clause cancel. A direct computation in the $2^n$ -dimensional space does not scale with $n$ and does not give a closed form.

For the variance, the naive bound by $m^2$ pairs gives nothing. The argument needs exact independence of clause terms whose sign dependencies are disjoint, which rests on (25) showing that each term depends only on its own sign and on the signs of the equations sharing exactly one bit with it, and then a combinatorial count of linked pairs.

Formalization scope

Bit strings are Fin n → Bool with true the bit $1$ ; the quantum layer reuses the published QAlgorithms definitions (Qubits, act, prob, uniformState, problemHamiltonian, qaoaMixer, qaoaUnitary). The phase operator is the full count of satisfied equations, which differs from the paper's $C$ of (6) by the constant $m/2$ ; the resulting states differ by a global phase and all probabilities agree. Triples are strictly increasing and pairwise distinct, which encodes "exactly three variables" and $d_{abc}\in\{0,\pm1\}$ . $D$ is a natural number. $\mathbb E_d$ is the uniform average over all $2^m$ right-hand-side vectors, $\mathbb E_z$ over all $2^n$ strings.

Two pins are disclosed. The angle range $0\le\gamma\le\pi/2$ is added to (50) and the goal, since the lower bound needs $\sin\gamma,\cos\gamma\ge0$ . The goal's threshold is (50)'s exact lower bound, not the paper's (54): $\big(\tfrac12+\tfrac1{2\sqrt{3e}D^{1/2}}\big)m$ is the large- $D$ limit and is false at every finite $D$ , so (51)–(53) are stated as a limit instead. The goal is about the expected satisfied count of the measured state; the sampling procedure, circuit size and the search over $\gamma$ are out of scope.

A trivializing reading is excluded: the probability is over the $2^m$ instances on the fixed triples, not over a single instance, and the bound is about the quantum expectation at $|-\gamma,\pi/4\rangle$ (at $+\gamma$ the mean has the opposite sign and the statement would be false).

A complete development needs finite averages over $\{0,1\}^m$ with independence of coordinates, the single-clause formula (25) in the $2^n$ -dimensional Hilbert space, and Chebyshev's inequality on a finite uniform space. The (25) computation and the second-moment count are reusable for other QAOA analyses. Contributions to any milestone are welcome, in any order.

Selected references

E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm Applied to a Bounded Occurrence Constraint Problem, arXiv:1412.6062v2, 2015. https://arxiv.org/abs/1412.6062
E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm, arXiv:1411.4028, 2014. https://arxiv.org/abs/1411.4028
B. Barak, A. Moitra, R. O'Donnell, P. Raghavendra, O. Regev, D. Steurer, L. Trevisan, A. Vijayaraghavan, D. Witmer, J. Wright, Beating the random assignment on constraint satisfaction problems of bounded degree, APPROX/RANDOM 2015. https://arxiv.org/abs/1505.03424
J. Håstad, On bounded occurrence constraint satisfaction, Information Processing Letters 74(1), 2000. (cited as [3] in arXiv:1412.6062v2)
L. Trevisan, Non-approximability results for optimization problems on bounded degree instances, Proc. STOC 2001 (cited as [4] in arXiv:1412.6062v2)

17 thms2 active usersReviewed

Optimization Theoretical Computer Science·Captain: mikedeng1

A Quantum Approximate Optimization Algorithm Applied to a Bounded Occurrence Constraint Problem I: Level-One QAOA Satisfies (1/2 + 1/(101 D^(1/2) ln D))m Equations of Max E3LIN2 for Large DResearch Paper

Motivation

The Quantum Approximate Optimization Algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028) is a family of shallow quantum circuits for combinatorial optimization. At its lowest level, $p = 1$ , the circuit has two real parameters, and its output is a random bit string. The question is how many constraints that string satisfies, compared with the best classical algorithms.

Max E3LIN2 is a natural test problem. Each constraint is a linear equation modulo $2$ on exactly three bits, and the task is to satisfy as many of the $m$ equations as possible. A uniformly random string satisfies $m/2$ in expectation, and for general instances no efficient algorithm does better than $(1/2 + \varepsilon)m$ unless P = NP (Håstad 2001). The interesting regime is bounded occurrence: every bit lies in at most $D + 1$ equations.

Timeline, as recorded on p. 3 of the paper:

2000: Håstad gives a classical algorithm with approximation ratio $1/2 + \mathrm{const}/D$ (doi:10.1016/S0020-0190(00)00032-6).
2001: Trevisan shows that an efficient algorithm with ratio $1/2 + \mathrm{const}/D^{1/2}$ , for a sufficiently large constant, would imply P = NP (doi:10.1145/380752.380839).
December 2014: the first version of this paper shows that the $p = 1$ QAOA yields a string satisfying $(1/2 + 1/(22D^{3/4}))m$ equations. That beat every classical algorithm known at the time.
2015: Barak et al. (arXiv:1505.03424) and Håstad give efficient classical algorithms reaching $(1/2 + \mathrm{const}/D^{1/2})m$ .
June 2015: version 2 of this paper (arXiv:1412.6062v2) improves the QAOA bound to $(1/2 + 1/(101D^{1/2}\ln D))m$ . This mission formalizes that bound.

Setting

An instance on $n$ bits consists of $m$ equations. Equation $i$ is

x_a + x_b + x_c \equiv r_i \pmod 2,

on a triple of distinct bits $a < b < c$ , with right-hand side $r_i \in \{0, 1\}$ , and no triple carries two equations. The instance has occurrence bound $D$ if every bit appears in at most $D + 1$ equations.

Let $C(z)$ be the number of equations satisfied by the string $z$ , viewed as a diagonal operator on the $2^n$ -dimensional space spanned by the basis states $|z\rangle$ . Let $B = X_1 + \dots + X_n$ be the sum of the Pauli $X$ operators, and $|s\rangle$ the uniform superposition of all basis states. For real angles $\gamma, \beta$ the level-one QAOA state is

|\gamma, \beta\rangle = e^{-i\beta B} e^{-i\gamma C} |s\rangle .

Measuring it in the computational basis returns $z$ with probability $|\langle z|\gamma,\beta\rangle|^2$ . The expected satisfied count is

F(\gamma, \beta) = \sum_z |\langle z|\gamma,\beta\rangle|^2\, C(z).

The paper writes the objective as $m/2 + \tfrac12\sum d_{abc} Z_a Z_b Z_c$ , with $d_{abc} = (-1)^{r}$ for the equation on $a, b, c$ . The analysis is phrased through the shifted quantity $\langle\gamma,\beta|\tfrac12\sum d_{abc}Z_aZ_bZ_c|\gamma,\beta\rangle = F(\gamma,\beta) - m/2$ .

The angles used are $\beta = \pi/4$ and, for an odd integer $k$ ,

\gamma_r = \frac{1}{10 D^{1/2}} \cos\frac{\pi r}{k}, \qquad r = 0, 1, \dots, k .

Formalization targets

Goal: (44)–(45), pp. 8–9

There is a threshold $D_0$ such that for every $D \ge D_0$ there is an odd $k$ with $5\ln D \le k \le 5\ln D + 2$ , such that on every instance with occurrence bound $D$ some grid angle satisfies

F(\gamma_r, \pi/4) \ \ge\ \Big(\frac12 + \frac{1}{101\, D^{1/2} \ln D}\Big)\, m .

$D_0$ and $k$ depend on $D$ only, never on the instance. Equivalently, in the paper's form (44), $\max_r \langle\gamma_r,\pi/4|\tfrac12\sum d_{abc}Z_aZ_bZ_c|\gamma_r,\pi/4\rangle \ge m/(101D^{1/2}\ln D)$ .

Milestones

The milestones are the displayed claims of Section II, in the order the argument uses them:

the sum form of $F$ and its oddness in $\gamma$ (p. 4);
the exact single-clause formula (25);
the Taylor remainder bound (28);
hypercontractivity for degree-2 polynomials (29);
the second-moment bounds (31) and (32);
the uniform remainder bound (34) and the triangle-inequality step (37);
the Chebyshev-node inequality (39), and its consequence (41) on the grid;
the numerical threshold (43).

Significance

The theorem shows that a single layer of the QAOA, with fixed $\beta$ and $O(\ln D)$ predetermined angles, beats random guessing by $\Omega(m/(D^{1/2}\ln D))$ on every bounded-occurrence instance. Up to the $\ln D$ factor this matches the $1/2 + \Theta(D^{-1/2})$ threshold that Trevisan's hardness result places on efficient algorithms.

Two ingredients are reusable well beyond this paper. The hypercontractive inequality (29) bounds all moments of a degree-2 polynomial in uniform $\pm1$ variables, at every exponent $q = k + 2$ . The Chebyshev-node inequality (39) bounds from below the maximum of a polynomial with unit linear coefficient over the points $\cos(\pi r/k)$ . Neither is in Mathlib or on the platform in this generality.

The result is proved on paper, with explicit constants, but none of it has been machine-checked. A complete formalization would also pin down two places where the printed argument is loose (see Formalization scope).

Difficulty

The obvious approach is to expand the expected count as a power series in $\gamma$ and keep the linear term $m\gamma/2$ . That fails because the higher-order terms are not small: each clause interacts with up to $3D$ others, so the coefficient of $\gamma^j$ can grow like $D^{j/2}$ , and their signs are uncontrolled. Uniform small-angle estimates therefore lose the linear gain unless $|\gamma| \lesssim D^{-1/2}$ . Even there, the polynomial part of degree up to $k$ can cancel the linear term at any single angle. The step that needs a genuinely new input is showing that some angle of a short fixed grid avoids this cancellation for every instance at once. The remaining difficulty is bookkeeping: the threshold where the explicit constants start to work is enormous ( $\ln D$ of order several hundred), so it has to be existential.

Formalization scope

Representation. Strings are Qubits n = Fin n → Bool, with true the bit $1$ . An instance is tri : Fin m → Fin n × Fin n × Fin n (strictly increasing coordinates, injective) and rhs : Fin m → Bool. Bounded occurrence counts, for each bit, the equations whose triple contains it.
Reused quantum layer. The published QAlgorithms definitions supply act, prob, uniformState, problemHamiltonian, qaoaMixer and qaoaUnitary.
Phase operator. The state uses the full count $C$ as phase operator, not the paper's $C - m/2$ . This changes the state by a global phase only, so every probability is the same.
Averages. $E_z$ is the uniform average over all $2^n$ strings. The paper averages over the bits occurring in $c_1, c_2, c_3$ only, which gives the same number.
Pinned forms. "For large $D$ " is an existential threshold $D_0$ , uniform over instances. " $k = 5\ln D$ " is an odd $k$ with $5\ln D \le k \le 5\ln D + 2$ : the Chebyshev-node step requires $k$ odd, and $5\ln D$ is not an integer. The grid therefore has at most $5\ln D + 3$ angles rather than the printed "no more than $5\ln D$ ".
Added hypothesis. The remainder bound (34) and its consumers assume $D \ge 1$ . The printed last step $e(1+9D)^{1/2} \le 9D^{1/2}$ holds for $D \ge 1$ only, and the printed justification " $e < 3$ " does not by itself give it.
Scope. The goal is about the expected satisfied count of the measured $p = 1$ state, which is what the paper's analysis bounds. Out of scope: the repetition and sampling procedure after (45), running time, circuit size, and the search over angles.
No trivialization. The goal cannot be met by a degenerate encoding: $D_0$ and $k$ precede the instance, the grid angles are fixed by $D$ and $k$ , and the hypotheses on the instance (distinct bits, one equation per triple, occurrence at most $D + 1$ ) are satisfiable for every $D$ .
Infrastructure. A complete development needs moments of polynomials on the Boolean cube (hypercontractivity at general $q$ ), Taylor remainders for $\sin$ , an extremal inequality for polynomials on Chebyshev extreme points, and exponential-of-Pauli computations on $n$ qubits. Hypercontractivity and the Chebyshev-node inequality are stated independently of the QAOA and are the most reusable contributions. Proofs of any milestone are welcome. Platform statements of $L^4$ – $L^2$ Bonami inequalities for bilinear chaos exist, but they cover only $q = 4$ and do not imply (29).

Selected references

E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm Applied to a Bounded Occurrence Constraint Problem, arXiv preprint, v2, 2015. https://arxiv.org/abs/1412.6062v2
E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm, arXiv preprint, 2014. https://arxiv.org/abs/1411.4028
I. Dinur, E. Friedgut, G. Kindler, R. O'Donnell, On the Fourier tails of bounded functions over the discrete cube, Israel Journal of Mathematics 160 (2007), 389–412. https://doi.org/10.1007/s11856-007-0068-z
J. Håstad, Some optimal inapproximability results, Journal of the ACM 48 (2001), 798–859. https://doi.org/10.1145/502090.502098
J. Håstad, On bounded occurrence constraint satisfaction, Information Processing Letters 74 (2000), 1–6. https://doi.org/10.1016/S0020-0190(00)00032-6
L. Trevisan, Non-approximability results for optimization problems on bounded degree instances, Proc. 33rd ACM STOC (2001), 453–461. https://doi.org/10.1145/380752.380839
B. Barak et al., Beating the random assignment on constraint satisfaction problems of bounded degree, ECCC TR15-082 / arXiv preprint, 2015. https://arxiv.org/abs/1505.03424

18 thms2 active usersReviewed

Information Theory Linear algebra Quantum Error Correction·Captain: mikedeng1

Reversing quantum dynamics with near-optimal quantum and classical fidelity I: The Reversal Operation Attains at Least the Square of the Optimal Average Entanglement FidelityResearch Paper

Motivation

Quantum error correction and quantum communication both ask the same question: after a known noise process $\mathcal A$ has acted on a quantum system, how well can its effect be undone? For a given noise model the best recovery is the solution of a semidefinite program, which gives a number but no structure and no formula. Barnum and Knill showed in 2000 that a single, explicit recovery map, built from $\mathcal A$ and the input state alone, is always close to the best one: its fidelity is at least the square of the optimal fidelity (arXiv:quant-ph/0004088). The map they use is now usually called the Petz recovery map or transpose channel; Petz had introduced it in operator-algebraic work on sufficiency (Petz 1986; Petz 1988). Near-optimality results of this kind underlie approximate quantum error correction and the later theory of recoverability in quantum information.

Timeline.

1986–1988, D. Petz: the map $\rho^{1/2}\mathcal A^\dagger(\mathcal A(\rho)^{-1/2}\,\cdot\,\mathcal A(\rho)^{-1/2})\rho^{1/2}$ characterizes when a channel can be reversed exactly on a family of states.
2002, Barnum and Knill (J. Math. Phys. 43, 2097; doi:10.1063/1.1459754): in the published version, the reversal operation achieves at least the square of the optimal entanglement fidelity for a single input state.
arXiv v2 of the same paper (the source of this mission): the published Eq. (34) had dropped the ensemble weights; with that corrected, the bound holds for the average entanglement fidelity of any ensemble of commuting density matrices (Acknowledgments, p. 14).

Setting

A finite-dimensional quantum system is described by complex $n\times n$ matrices; $X^\dagger$ is the conjugate transpose, and a density matrix is a positive semidefinite matrix of trace one. A completely positive map $\mathcal A$ is given by a finite decomposition $\mathcal A\sim\{A_i\}_i$ of matrices and acts by

\mathcal A(X)=\sum_iA_iXA_i^\dagger .

It is trace-preserving if $\sum_iA_i^\dagger A_i=I$ and trace-nonincreasing if $\sum_iA_i^\dagger A_i\le I$ in the Loewner order. The composite $\mathcal R\mathcal A$ has decomposition $\{R_kA_i\}_{(k,i)}$ .

For a state $\rho$ the paper defines the reversal operation

\mathcal R_{\mathcal A,\rho}\sim\{\rho^{1/2}A_i^\dagger\,\mathcal A(\rho)^{-1/2}\}_i,

under the standing assumption that $\mathcal A(\rho)$ has full support. Here $X^{-1/2}$ is the generalized inverse square root: invert the square roots of the non-zero eigenvalues and keep the zero eigenvalues.

Fidelities are measured by the entanglement fidelity $F_e(\rho,\mathcal K)=\sum_k|\operatorname{tr}K_k\rho|^2$ of a map $\mathcal K\sim\{K_k\}_k$ and, for an ensemble $E=\{p_l,\rho_l\}_l$ (weights $p_l\ge0$ summing to one, density matrices $\rho_l$ ), by the average entanglement fidelity

\bar F_e(E,\mathcal K)=\sum_lp_lF_e(\rho_l,\mathcal K).

When $\rho=\sum_ip_i|i\rangle\langle i|$ in an orthonormal eigenbasis, the classical fidelity is $F_{\mathrm{cl}}(\rho,\mathcal K)=\sum_ip_i\langle i|\mathcal K(|i\rangle\langle i|)|i\rangle$ , the average entanglement fidelity of the ensemble of eigenstates.

Formalization targets

Goal: Theorem 3 (p. 7)

Let $\mathcal A$ be trace-preserving, $E=\{p_l,\rho_l\}_l$ an ensemble of pairwise commuting density matrices, $\rho=\sum_lp_l\rho_l$ , and assume $\mathcal A(\rho)$ has full support. Then for every trace-preserving completely positive $\mathcal R$ ,

\bar F_e(E,\mathcal R_{\mathcal A,\rho}\mathcal A)\;\ge\;\bar F_e(E,\mathcal R\mathcal A)^2 .

Milestones

The milestones follow the paper's proof:

Lemma 1 (p. 7): $\mathcal R_{\mathcal A,\rho}$ depends only on the map $\mathcal A$ , not on its decomposition.
(14)–(15) (p. 7): after replacing $R_k$ by $P_CR_k$ ( $P_C$ the support projector of $\rho$ ), which leaves $\bar F_e$ unchanged and makes $\mathcal R$ trace-nonincreasing, each $R_k=\rho^{1/2}B_k^\dagger\mathcal A(\rho)^{-1/2}$ , and $\mathcal B(\rho)\le\mathcal A(\rho)$ .
(28)–(32) (p. 9): $\sum_lp_l\sum_i|\operatorname{tr}\rho_lR^l_iB^l_i|^2\le\sum_lp_l\sum_{i,j}\operatorname{tr}R^l_iB^l_j\rho_lB_j^{l\dagger}R_i^{l\dagger}$ .
(33)–(34) (p. 9): that sum equals $\operatorname{tr}\mathcal R(\mathcal B(\rho))\le\operatorname{tr}\mathcal R(\mathcal A(\rho))\le1$ .

Two companions are also posed: Proposition 2, $\mathcal R_{\mathcal A,\rho}(\mathcal A(\rho))=\rho$ , and Corollary 4, $F_{\mathrm{cl}}(\rho,\mathcal R\mathcal A)\le\sqrt{F_{\mathrm{cl}}(\rho,\mathcal R_{\mathcal A,\rho}\mathcal A)}$ and $F_e(\rho,\mathcal R\mathcal A)\le\sqrt{F_e(\rho,\mathcal R_{\mathcal A,\rho}\mathcal A)}$ .

Significance

The result. Theorem 3 says that the error $1-\bar F_e$ of the reversal operation is at most twice the optimal error, since $(1-\eta)^2\ge1-2\eta$ . It gives a closed-form recovery whose performance is within a factor two in error of the semidefinite optimum, for every noise process and every commuting ensemble. Taking the ensemble of eigenstates of $\rho$ (Corollary 4) gives the same guarantee for classical information sent through a quantum channel; the companion mission (II of this series) applies the construction to state discrimination, where the reversal operation is the pretty good measurement.

Formalizing it. The result is proved on paper; none of it has a machine-checked proof that we know of. The mission asks for the full argument: the decomposition independence of the reversal map, the reduction to the support of $\rho$ , the singular-value change of decomposition (17)–(18), the chain (19)–(26) of Cauchy–Schwarz inequalities, and the normalization (27)–(34). It also fixes in Lean the arXiv v2 statement (commuting ensembles), which is stronger than the published one.

Difficulty

The obvious approach is to compare $\mathcal R_{\mathcal A,\rho}$ with an optimal $\mathcal R$ term by term. That fails: the fidelity of $\mathcal R\mathcal A$ is a sum of squared traces mixing the decompositions of $\mathcal R$ and $\mathcal A$ , and no termwise inequality relates it to the fidelity of $\mathcal R_{\mathcal A,\rho}\mathcal A$ . The paper first rewrites every recovery in the shape of the reversal map, then chooses, for each ensemble member separately, new decompositions of $\mathcal A$ and $\mathcal B$ that diagonalize a coefficient matrix; making that choice legitimate needs the unitary freedom of Kraus decompositions, which Mathlib does not have. The commutation $[\rho,\rho_l]=0$ is used to move fractional powers of $\rho$ and $\rho_l$ past each other inside traces; without commutation the authors do not know whether the theorem holds (p. 10).

Formalization scope

Matrices are Matrix n n ℂ over a finite type n with decidable equality; Loewner order, square roots and functional calculus come from Mathlib (open scoped MatrixOrder). The map $X\mapsto\sum_iA_iXA_i^\dagger$ is the published PeresTerno.krausUpdate, referenced, not redefined.
Maps are unbundled Kraus families over arbitrary finite index types. The recovery $\mathcal R$ in Theorem 3 ranges over every finite family with $\sum_kR_k^\dagger R_k=I$ .
$X^{-1/2}$ is cfc (fun x => (Real.sqrt x)⁻¹) X, the generalized inverse; Mathlib's junk matrix inverse is not used. The support projector is the functional calculus of the indicator of $x\ne0$ .
$F_e$ is defined by the formula (8), which the paper derives from its purification definition. $F_{\mathrm{cl}}$ takes an orthonormal eigenbasis and weights as data, with $\rho=\sum_ip_i|i\rangle\langle i|$ as a hypothesis.
Standing hypotheses, all from the paper: $\mathcal A$ trace-preserving (§II's noise model); $\mathcal A(\rho)$ positive definite (full support, p. 7); the ensemble is a probability vector of pairwise commuting density matrices with $\rho=\sum_lp_l\rho_l$ .
In (34) the page prints $\operatorname{tr}\mathcal R(\mathcal A(\rho))=1$ ; after the replacement $R_k\mapsto P_CR_k$ the map is only trace-nonincreasing, so the milestone states $\le1$ .
Trivializing encodings are ruled out: the reversal family is the literal formula (12) for the given $\mathcal A$ and the ensemble's own $\rho$ , and the fidelity of a composite map is (8) applied to the composite decomposition $\{R_kA_i\}$ , never the right-hand side of the proof's chain.
Infrastructure a complete development needs, reusable beyond this mission: the unitary freedom of Kraus decompositions, the singular value decomposition of a complex square matrix, the trace Cauchy–Schwarz inequality for Hilbert–Schmidt products, and functional-calculus identities such as $\rho^{1/2}\rho^{-1/2}=P_C$ . Contributions of any of these as separate theorems are welcome. The pure-state, measurement form $P_{\mathrm{opt}}^2\le P_{\mathrm{PGM}}\le P_{\mathrm{opt}}$ is already posed on the platform as QAlgorithms.Arunachalam.barnumKnill and is not repeated here.

Selected references

H. Barnum, E. Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, arXiv:quant-ph/0004088v2. https://arxiv.org/abs/quant-ph/0004088
H. Barnum, E. Knill, same title, J. Math. Phys. 43, 2097 (2002). https://doi.org/10.1063/1.1459754
D. Petz, Sufficient subalgebras and the relative entropy of states of a von Neumann algebra, Commun. Math. Phys. 105, 123–131 (1986). https://doi.org/10.1007/BF01212345
D. Petz, Sufficiency of channels over von Neumann algebras, Quart. J. Math. 39, 97–108 (1988). https://doi.org/10.1093/qmath/39.1.97
B. Schumacher, Sending entanglement through noisy quantum channels, Phys. Rev. A 54, 2614 (1996). https://doi.org/10.1103/PhysRevA.54.2614
R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press (1985), §7.3. https://doi.org/10.1017/CBO9780511810817

7 thms2 active usersReviewed

Probability Statistics·Captain: mikedeng1

Direct Fidelity Estimation from Few Pauli Measurements 2: A Unit Vector Nearly Orthogonal to 2^{cd} Given States With Every Non-Identity Pauli Expectation ≤ √(72π³)·√(log d)/√dResearch Paper

Motivation

Quantum state tomography reconstructs an unknown $d$ -dimensional quantum state from measurements on many copies of it. For $n$ qubits, $d = 2^n$ , so the number of copies a tomography procedure needs grows exponentially in $n$ , and lower bounds on that number decide how far experiments can scale. In many experiments the only measurements available are Pauli measurements: each qubit is measured in the eigenbasis of one of $\sigma_x, \sigma_y, \sigma_z$ .

Flammia and Liu, Direct fidelity estimation from few Pauli measurements (arXiv:1104.4695, Phys. Rev. Lett. 106, 230501, 2011), show that the fidelity of an experimental state with a target pure state can be estimated with far fewer copies than full tomography needs. To make the comparison meaningful they also prove that full tomography of a pure state with Pauli measurements requires $\Omega(d^2/\log d)$ copies. That lower bound has two steps. The first builds a large family of nearly orthogonal pure states whose Pauli expectation values are all small, so that Pauli measurements extract little information about which state is present. Its engine is Lemma 1 of the paper (p. 7), the subject of this mission. The second step, an information-theoretic argument over a noisy classical channel, is not in scope.

Setting

Fix $n \ge 1$ qubits and put $d = 2^n$ . States are unit vectors $\psi \in \mathbb C^d$ , $\|\psi\|_2 = 1$ ; the overlap $\langle\varphi|\psi\rangle = \sum_x \overline{\varphi_x}\psi_x$ is conjugate-linear in $\varphi$ .

The single-qubit Pauli matrices are $I$ , $\sigma_x$ , $\sigma_y$ , $\sigma_z$ . A Pauli label $k \in \{0,1,2,3\}^n$ determines the $n$ -qubit Pauli operator $W_k = \sigma_{k_1}\otimes\cdots\otimes\sigma_{k_n}$ (with $\sigma_0 = I$ ). There are $d^2$ labels; the all-zero label gives $W_k = I$ . Every $W_k$ is Hermitian and unitary, so the Pauli expectation $\langle\psi|W_k|\psi\rangle$ is a real number in $[-1, 1]$ .

A Haar-random state is a vector $\psi$ drawn from the uniform (rotation-invariant) probability measure on the unit sphere of $\mathbb C^d$ , a real sphere of dimension $2d - 1$ . The constants of the lemma are

\varepsilon = \sqrt{9\pi^3(\log 2)\,c},\qquad \tau = \sqrt{72\pi^3},\qquad C_1 = \frac{2}{9\pi^3},

with $\log$ the natural logarithm and $c > 0$ a parameter.

Formalization targets

Goal: Lemma 1

Let $\varphi_1, \dots, \varphi_s \in \mathbb C^d$ be states with $s \le 2^{cd}$ . Then there is a state $\psi \in \mathbb C^d$ with

|\langle\varphi_i|\psi\rangle| \le \varepsilon \quad (1 \le i \le s), \qquad |\langle\psi|W_k|\psi\rangle| \le \tau\sqrt{\log d}/\sqrt d \quad (W_k \ne I).

These are (31) and (32) of the paper. The goal is an existence statement with no measure in it.

Milestones (all p. 7)

(33): for a state $\varphi$ , $|\langle\varphi|\psi\rangle - \langle\varphi|\psi'\rangle| \le \|\psi - \psi'\|_2$ .
$\mathbb E\langle\varphi|\psi\rangle = 0$ for Haar-random $\psi$ .
(34): $\Pr[|\langle\varphi|\psi\rangle| \ge \varepsilon] \le 4\exp(-C_1 d\varepsilon^2/\eta^2)$ with $\eta = 1$ .
(35): $\Pr[(31)\text{ fails for some } i] \le 4\exp(cd\log 2 - C_1 d\varepsilon^2) = 4\cdot 2^{-cd}$ .
(36): on unit vectors, $|\langle\psi|W_k|\psi\rangle - \langle\psi'|W_k|\psi'\rangle| \le 2\|\psi - \psi'\|_2$ .
$\mathbb E\langle\psi|W_k|\psi\rangle = 0$ for $W_k \ne I$ .
(37): $\Pr[|\langle\psi|W_k|\psi\rangle| \ge \tau\sqrt{\log d}/\sqrt d] \le 4\exp(-C_1\tau^2(\log d)/\eta^2)$ with $\eta = 2$ .
(38): $\Pr[(32)\text{ fails for some } k] \le 4\exp(2\log d - C_1\tau^2(\log d)/4) = 4/d^2$ .

Every constant is the paper's; none is replaced by an unspecified absolute constant.

Significance

The result. Lemma 1 is a packing statement: applied repeatedly, it yields $2^{\Omega(d)}$ states that are pairwise almost orthogonal and whose non-identity Pauli expectations are all $O(\sqrt{\log d/d})$ . Such states are hard to tell apart with Pauli measurements, since each measurement outcome is nearly unbiased. The paper converts this into the $\Omega(d^2/\log d)$ copy lower bound for full tomography with Pauli measurements (pp. 3, 7–8). Since direct fidelity estimation of an arbitrary pure state uses $O(d)$ copies (for fixed accuracy and failure probability), the lower bound is what shows that the scheme beats tomography followed by a fidelity computation by a factor of about $d$ .

Formalizing it. The lemma and its proof are published, but none of it is machine-checked: Mathlib has no Pauli operators, no concentration of measure on spheres with explicit constants, and no Levy lemma. A formal proof needs a concentration inequality on the complex unit sphere with the explicit constant $C_1 = 2/(9\pi^3)$ (or any sharper one), the vanishing of the means by symmetry, and the union bounds. Each milestone is a reusable fact about Haar-random states.

Difficulty

The two union bounds (35) and (38) and the Lipschitz estimates (33) and (36) are elementary. The central difficulty is the tail bounds (34) and (37). The paper obtains them from Levy's lemma, which it cites (P. Lévy, 1951) and does not prove; Levy's lemma rests on the isoperimetric inequality on the sphere, which Mathlib does not have, and (37) concerns a quadratic form of $\psi$ rather than a linear one. Both tail bounds also need a working theory of the uniform measure on the complex unit sphere (rotation invariance, the distribution of a coordinate), little of which exists in Lean today.

A second difficulty is that the printed proof does not cover every parameter. The union bound produces a good $\psi$ only when $4\cdot 2^{-cd} + 4/d^2 < 1$ . For small $d$ , or small $c$ with few given states, the goal is still true, but a complete proof must handle those cases separately; they are not in the paper.

Formalization scope

Representation. Basis labels are Q n = Fin n → Fin 2, Pauli labels P n = Fin n → Fin 4, states live in EuclideanSpace ℂ (Q n), and $W_k$ is the entrywise product of single-qubit Pauli matrices (the Kronecker product). $d$ is the real number $2^n$ ; $\log$ is Real.log; ⟨φ|ψ⟩ is Mathlib's inner ℂ φ ψ.
Measure. The uniform measure on the sphere is Mathlib's Measure.toSphere of an additive Haar measure on $\mathbb C^d$ (as a real vector space), normalised to total mass one. The paper's "Haar-random vector in $S^{d-1}$ " is read as this measure on the unit sphere of $\mathbb C^d$ .
Added hypotheses, all disclosed. The goal assumes $n \ge 1$ : at $n = 0$ ( $d = 1$ ) and small $c$ the lemma is false, since every unit vector of $\mathbb C^1$ has overlap $1$ with $\varphi_1$ . It assumes $c > 0$ , under which $\varepsilon$ is defined. "States" means unit vectors, for the given $\varphi_i$ and for the produced $\psi$ . The mean-zero statement for Pauli operators assumes $W_k \ne I$ (for $W_k = I$ the mean is $1$ ); the paper's "for each $k$ " refers to the non-identity labels of (32). " $W_k \ne I$ " is formalized as "the label $k$ is not all zeros".
Non-trivialization. The produced $\psi$ must be a unit vector, so $\psi = 0$ does not satisfy the goal; the given states are unit vectors, so (31) is not trivially false; and the mean-zero milestones assert integrability together with the value of the integral, so they cannot hold merely because a non-integrable integral is $0$ .
Infrastructure needed. Facts about $n$ -qubit Pauli operators (Hermitian, unitary, traceless for $W_k \ne I$ ); rotation invariance of the normalised sphere measure; a concentration inequality for Lipschitz functions on the complex unit sphere with an explicit constant. The concentration inequality and the sphere-measure facts are reusable well beyond this mission and are welcome as separate contributions.

Selected references

S. T. Flammia and Y.-K. Liu, Direct fidelity estimation from few Pauli measurements, Phys. Rev. Lett. 106, 230501 (2011); arXiv:1104.4695v3. https://arxiv.org/abs/1104.4695
P. Lévy, Problèmes concrets d'analyse fonctionnelle, Gauthier-Villars, Paris, 1951 (reference [10] of the paper; no stable online link).
M. Ledoux, The Concentration of Measure Phenomenon, Mathematical Surveys and Monographs 89, AMS, 2001. https://doi.org/10.1090/surv/089
P. Hayden, D. W. Leung and A. Winter, Aspects of generic entanglement, Comm. Math. Phys. 265, 95–117 (2006); arXiv:quant-ph/0407049. https://arxiv.org/abs/quant-ph/0407049

11 thms2 active usersReviewed

Graph Theory Optimization·Captain: mikedeng1

A Quantum Approximate Optimization Algorithm II: On v-Regular Graphs the Variance of the Cut Value in the QAOA State Is at Most 2((v−1)^(2p+2)−1)/(v−2) Times the Number of EdgesResearch Paper

Motivation

The Quantum Approximate Optimization Algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028, 2014) is a family of shallow quantum circuits for combinatorial optimization, indexed by a depth $p$ and $2p$ real angles. It has become one of the standard candidate algorithms for near-term quantum hardware, and its MaxCut instance is the usual benchmark on which it is analysed.

The algorithm is run by preparing a quantum state, measuring it in the computational basis to obtain a bit string $z$ , and evaluating the classical objective $C(z)$ . Its analysis in the paper bounds the mean $F_p$ of $C(z)$ . A mean alone does not say what a single run returns. Section III of the paper supplies the missing piece for MaxCut on bounded-degree graphs: the variance of $C(z)$ grows at most linearly in the number of edges, so the measured cut values are concentrated around $F_p$ and a modest number of repetitions reproduces the mean. This mission formalizes that variance bound, equation (30) of the paper, together with the locality and counting facts it rests on.

Setting

Let $G$ be a simple graph on vertices $\{0,\dots,n-1\}$ with edge set $\{\langle jk\rangle\}$ of size $m$ , each edge listed once. Vertices are qubits; a computational basis state is a bit string $z\in\{0,1\}^n$ .

The clause operator of an edge is $C_{\langle jk\rangle}=\tfrac12(-\sigma^z_j\sigma^z_k+1)$ . It is diagonal: $C_{\langle jk\rangle}(z)=1$ if $z_j\ne z_k$ and $0$ otherwise.
The MaxCut objective is $C=\sum_{\langle jk\rangle}C_{\langle jk\rangle}$ ; $C(z)$ is the number of edges cut by $z$ .
The mixer is $B=\sum_j\sigma^x_j$ , and $U(C,\gamma)=e^{-i\gamma C}$ , $U(B,\beta)=e^{-i\beta B}$ .
The initial state is $|s\rangle=2^{-n/2}\sum_z|z\rangle$ .
For $p\ge1$ and angles $\boldsymbol\gamma=(\gamma_1,\dots,\gamma_p)$ , $\boldsymbol\beta=(\beta_1,\dots,\beta_p)$ , the QAOA state is

|\boldsymbol\gamma,\boldsymbol\beta\rangle=U(B,\beta_p)\,U(C,\gamma_p)\cdots U(B,\beta_1)\,U(C,\gamma_1)\,|s\rangle .

Measuring it gives $z$ with probability $P(z)=|\langle z|\boldsymbol\gamma,\boldsymbol\beta\rangle|^2$ . The mean is $F_p(\boldsymbol\gamma,\boldsymbol\beta)=\langle\boldsymbol\gamma,\boldsymbol\beta|C|\boldsymbol\gamma,\boldsymbol\beta\rangle=\sum_zP(z)C(z)$ and the variance is

\langle\boldsymbol\gamma,\boldsymbol\beta|C^2|\boldsymbol\gamma,\boldsymbol\beta\rangle-\langle\boldsymbol\gamma,\boldsymbol\beta|C|\boldsymbol\gamma,\boldsymbol\beta\rangle^2 .

The light cone (the paper's subgraph $g(j,k)$ ) of an edge is the set of qubits at graph distance at most $p$ from $j$ or from $k$ .

In Lean these are edgeCut, cutValue, qaoaState, expectCut and edgeTerm in the shared FarhiQAOA.Cubic setting, and edgePairs, cutVariance, edgePairTerm, edgeCov and lightCone in FarhiQAOA.Concentration, all built on the published QAlgorithms definitions of qubit registers, measurement probabilities, the uniform superposition, the problem Hamiltonian and the QAOA unitary.

Formalization targets

Goal: the variance bound (30)

For a $v$ -regular graph with $v\ge3$ , every depth $p\ge1$ and all real angles,

\langle\boldsymbol\gamma,\boldsymbol\beta|C^2|\boldsymbol\gamma,\boldsymbol\beta\rangle-\langle\boldsymbol\gamma,\boldsymbol\beta|C|\boldsymbol\gamma,\boldsymbol\beta\rangle^2\le2\left[\frac{(v-1)^{2p+2}-1}{(v-1)-1}\right]\cdot m .

The constant is the paper's, as printed.

Milestones

(27)–(28). The variance is the double sum, over ordered pairs of edges, of the covariances $\langle C_{\langle jk\rangle}C_{\langle j'k'\rangle}\rangle-\langle C_{\langle jk\rangle}\rangle\langle C_{\langle j'k'\rangle}\rangle$ .
Disjoint light cones. If $g(j,k)$ and $g(j',k')$ share no qubit, the covariance of the two edges is $0$ .
(26). For maximum degree $v\ge3$ , $|g(j,k)|\le2\big[((v-1)^{p+1}-1)/((v-1)-1)\big]$ .
(29). For maximum degree $v\ge3$ , at most $2\big[((v-1)^{2p+2}-1)/((v-1)-1)\big]$ edges $\langle j'k'\rangle$ have $g(j',k')$ meeting $g(j,k)$ .
Summand bound. Each covariance is at most $1$ in absolute value.

Companions, printed in the paper for $v=2$ : $|g(j,k)|\le2p+2$ and at most $4p+4$ meeting edges.

Significance

The result. For fixed $v$ and $p$ the bound makes the standard deviation of the cut value $O(\sqrt m)$ , while the mean is of order $m$ . The algorithm's output is therefore concentrated: a single measurement already returns a cut close to $F_p$ in relative terms, and the paper uses this to argue that the sample mean of polynomially many runs estimates $F_p$ within $1$ . The same locality structure, that each edge term depends only on a bounded neighbourhood, is what makes $F_p$ classically computable for fixed $p$ and underlies later analyses of QAOA on bounded-degree and random regular graphs.

Formalizing it. The bound is proved in the paper in a few lines; none of it is machine-checked. A formal proof has to make the paper's operator locality argument precise (the conjugated clause operator is supported on the light cone, and the initial state is a product state), connect it to the computational-basis probabilities, and carry out the graph counting with explicit constants. The resulting locality lemma for QAOA circuits on graphs is reusable for any statement about QAOA at fixed depth.

Difficulty

The algebra of (28) and the bound by $1$ are routine. The substance is in two places.

The vanishing of a covariance requires showing that $U^\dagger C_{\langle jk\rangle}U$ , for the full depth- $p$ QAOA unitary $U$ , acts only on the qubits of $g(j,k)$ , and that for two operators acting on disjoint sets of qubits the expectation in the product state $|s\rangle$ factorizes. Both are statements about operators on $(\mathbb C^2)^{\otimes n}$ , whereas the objects in the statement are probabilities of computational basis states; the formal proof must pass between the two. Matrix exponentials of commuting sums have to be split into commuting factors, which in Lean means working with NormedSpace.exp on matrices indexed by bit strings.

The counting (26) and (29) is a ball-growth bound in a graph of bounded degree. The paper's count, via (26) with $p$ replaced by $2p+1$ , bounds vertices, while (29) counts edges; the passage between the two, and the extended graph distance on disconnected graphs, must be made exact with the printed constant.

Formalization scope

Qubits are indexed by Fin n, bit strings are Fin n → Bool with true the bit $1$ , and states live in EuclideanSpace ℂ (Fin n → Bool).
All expectations are sums $\sum_zP(z)\,f(z)$ over the computational basis. This equals the operator expectation in the paper because every operator involved is diagonal.
Each edge is counted once (pairs $j<k$ ), in $m$ , in $C$ , in the double sum of (28) and in the count (29).
Graph distance is the extended distance SimpleGraph.edist ( $+\infty$ between components).
The goal is stated for $v$ -regular graphs with $v\ge3$ , the domain of the printed formula. The milestones (26) and (29) assume only maximum degree $\le v$ , as printed there.
The angles range over all of $\mathbb R^p$ . The paper restricts them to $[0,2\pi]$ and $[0,\pi]$ by periodicity; the bound does not depend on that restriction.
The QAOA state is the state itself, not an arbitrary vector: normalisation of the measurement probabilities follows from unitarity and is part of what must be proved.

A variance defined with two different states, or a probability vector that is not normalised, would make the goal vacuous or false; the definitions use the single state $|\boldsymbol\gamma,\boldsymbol\beta\rangle$ throughout.

Out of scope: the $O(\sqrt m)$ standard-deviation reading and the sampling claim after (30), which carry no explicit constant; the measurement-and-repetition procedure, running time, circuit depth and the classical search for the angles.

Welcome contributions: a general light-cone lemma for conjugation by products of exponentials of local Hamiltonians on qubits; factorization of product-state expectations over disjoint qubit sets; ball-size bounds in graphs of bounded degree.

Selected references

E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm, arXiv preprint, 2014. https://arxiv.org/abs/1411.4028 (v1; Section III, pp. 6–7)
E. Farhi, J. Goldstone, S. Gutmann, M. Sipser, Quantum Computation by Adiabatic Evolution, arXiv preprint, 2000. https://arxiv.org/abs/quant-ph/0001106

14 thms2 active usersReviewed

Linear algebra·Captain: mikedeng1

Improvements in Quantum SDP-Solving with Applications 1: A Unitary Preparing a Purification of a Subnormalized Density Operator ϱ Gives an Exact (1, w+a+1, 0)-Block-Encoding of ϱResearch Paper

Motivation

Quantum algorithms for semidefinite programming need a way to use an input matrix inside a quantum circuit. In the quantum state input model, an oracle prepares a purification of a density operator. In the quantum operator input model, a unitary instead exposes that operator as a block of a larger unitary. The two kinds of access serve different subroutines. Lemma 12 of van Apeldoorn and Gilyén’s 2018 preprint connects them for a subnormalized density operator. The same paper uses this connection when comparing its input models for quantum SDP solving.

The result concerns a precise finite-dimensional construction. It matters even without the paper’s query-complexity estimates: it specifies which registers must be present, what happens to probability mass outside the accepted flag state, and which block of the resulting unitary equals the desired operator. These details are easy to lose when a statement is shortened to “purification gives a block-encoding.”

Setting

A w-qubit register has basis labels in $\{0,1\}^{w}$ . A subnormalized density operator $\varrho$ on that register is a positive semidefinite complex matrix with $\operatorname{Tr}\varrho\leq1$ . Its trace may be strictly below one. A purification is a unit vector $|\varphi\rangle$ on three registers: the w-qubit system, one flag qubit, and a c-qubit junk register. The operator $\varrho$ is the flag-zero block after tracing out the junk. In entries,

\varrho_{ij}=\sum_{t\in\{0,1\}^{c}}\varphi_{i,0,t}\,\overline{\varphi_{j,0,t}}.

Thus probability in the flag-one branch does not contribute to $\varrho$ . Let $a=c+1$ , so a unitary $G$ preparing $|\varphi\rangle$ acts on $w+a$ qubits and $|\varphi\rangle=G|0\rangle^{\otimes(w+a)}$ . The result adds an initial w-qubit system and one extra qubit. Its register swap $S$ exchanges the initial $(\text{system},\text{extra})$ register with the $(\text{prepared system},\text{flag})$ register and leaves the c junk qubits fixed. The construction is

V=(I_{2^{w+1}}\otimes G^{\dagger})S(I_{2^{w+1}}\otimes G).

A $(\alpha,k,\varepsilon)$ block-encoding of an operator $A$ is a unitary on the system and k ancilla qubits whose all-zero ancilla block differs from $A/\alpha$ in operator norm by at most $\varepsilon/\alpha$ . Here the scale is one and the error is zero. The block of $V$ is taken at the all-zero state of the extra qubit and the entire register of $G$ .

Formalization targets

The goal is Lemma 12 with the ancilla count given by its displayed construction:

\left\|\varrho-(I_{2^w}\otimes\langle0|^{\otimes(w+a+1)})V (I_{2^w}\otimes|0\rangle^{\otimes(w+a+1)})\right\|=0.

The target includes that $V$ is unitary, making it an exact $(1,w+a+1,0)$ block-encoding of $\varrho$ . The theorem identifies $V$ explicitly, so its use of one $G$ and one $G^{\dagger}$ is part of the construction. The source’s Lemma 12 prints $(1,w+a,0)$ , while its proof says $V$ has $2w+a+1$ qubits and takes the block at $1+w+a$ ancillas. This mission uses the proof’s consistent count and labels the correction. The four milestones follow the proof’s stated steps: unitarity of $V$ , identification of its zero block, elimination of the flag-one component, and equality of the remaining SWAP sandwich with $\varrho$ .

Significance

The exact identity shows that a state-preparation unitary can be used where the paper’s quantum operator model expects a block-encoding. It also covers genuinely subnormalized operators, for which a normalized-state argument is insufficient: a preparation may have nonzero amplitude in the flag-one branch even though only the flag-zero branch defines $\varrho$ . The explicit ancilla count prevents such lost probability mass from being silently included in the output block.

Formalizing this known result gives a reusable interface between a purification predicate and a block-encoding predicate. The mission statement is open on Prove2Me; the paper’s mathematical argument is known. A related open block-encoding statement in Nannicini’s treatment concerns a normalized density matrix and a circuit-level construction with a different ancilla arrangement. It does not state this paper’s subnormalized, flag-qubit identity. The finite-register definitions and SWAP identities can be reused by later matrix-level quantum algorithms, whether or not the paper’s larger complexity bounds are formalized.

Difficulty

The first apparent shortcut is to use the ordinary purification identity without the flag qubit. That recovers the trace over both flag outcomes, which can have trace one even when $\operatorname{Tr}\varrho<1$ . The required block must select flag zero. A second source of error is register order: the paper displays the system first, while the existing Lean block-encoding predicate places the ancilla register first. Equality of matrix blocks depends on the explicit reindexing. Complex conjugation also matters: swapping the vector and covector amplitudes would produce a transpose of $\varrho$ instead of $\varrho$ for complex states.

Formalization scope

The Lean system register is QAlgorithms.Qubits w; the flag and extra register are each Bool; and the junk is QAlgorithms.Qubits c. The identity $a=c+1$ makes the flag register present even at $c=0$ . The all-zero state is the all-false basis label. Matrices are over $\mathbb C$ , tensor products are matrix Kronecker products, and $S$ is a permutation matrix fixing the junk. The paper’s printed identity factor beside the swap has size $2^a$ ; the consistent factor is $2^{a-1}=2^c$ , since the swap already acts on two $w+1$ -qubit registers.

The referenced QAlgorithms.IsBlockEncoding definition includes unitarity and measures error with the operator norm. Lean reindexes $V$ to put its $(\text{extra},\text{prepared system},\text{flag},\text{junk})$ ancilla first. The theorem requires $G$ unitary, $\varrho$ subnormalized, and the exact purification relation between $G|0\rangle$ and $\varrho$ . The purification relation prevents a vacuous claim about an unrelated matrix. The optional quantum gate-count clause of the printed lemma is outside this matrix-level formalization; the register swap is explicitly the swap of $w+1$ qubit pairs. A circuit-level gate-count theorem would require an additional gate-list representation.

The needed reusable components are finite complex matrices, unitary permutation matrices, Kronecker products, partial traces, and the operator norm. Contributions can address the four milestone identities, the main theorem, or a circuit-level refinement of the gate count. None of the statements introduces the proof’s Schmidt decomposition as an assumption.

Selected references

J. van Apeldoorn and A. Gilyén, Improvements in Quantum SDP-Solving with Applications, arXiv preprint, 2018, arXiv:1804.05058v1, Definition 1 (p. 3), Definition 2 (p. 4), Lemma 12 and proof (pp. 15–16).
G. Nannicini, Quantum Algorithms for Optimizers, arXiv preprint, 2024, arXiv:2408.07086, Definition 7.11 and the normalized density-matrix construction.

8 thms2 active usersReviewed

Quantum Information

Missions

Existence of complete sets of mutually unbiased basesOpen Problem

Motivation

Setting

Significance

Difficulty

Suggested attack route

Formalization scope

Milestones

Timeline and literature status

Acceptance criteria

Formal verification policy

Selected references

Markov Entanglement: Value Decomposition Error in Multi-agent MDPsResearch Paper

Hardy 2001 I: Five Reasonable Axioms — Degrees of Freedom K = N^rResearch Paper

Motivation

Setting

Formalization targets

Goal: K(N)=NrK(N)=N^rK(N)=Nr

Milestones

Significance

Difficulty

Formalization scope

Selected references

Albers–Kiefer–Reginatto 2008: Measurement Analysis and Quantum GravityResearch Paper

Motivation

Setting

Formalization targets

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

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stabilizer Rank of Magic StatesOpen Problem

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

Reversing quantum dynamics with near-optimal quantum and classical fidelity II: The Pretty Good Measurement Errs at Most the Weighted Sum of Bures–Uhlmann FidelitiesResearch Paper

Motivation

Setting

Formalization targets

Recovery error

Significance

Difficulty

Formalization scope

Selected references

Quantum Amplitude Amplification and Estimation: Est_Amp(A, χ, M) Outputs ã with |ã − a| ≤ 2πk√(a(1−a))/M + k²π²/M² with Probability ≥ 8/π² for k = 1 and > 1 − 1/(2(k−1)) for k ≥ 2Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 12 (Amplitude Estimation)

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Quantum Algorithm for Systems of Linear Equations with Exponentially Improved Dependence on Precision I: A Truncated Odd Chebyshev Series Is 2ε-Close to 1/x on [−1, −1/κ] ∪ [1/κ, 1]Research Paper

Motivation

Setting

Formalization targets

Goal: Lemma 14 (p. 16)

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Oreshkov–Costa–Brukner 2012: Quantum Correlations with No Causal OrderResearch Paper

Motivation

Setting

Formalization targets

Goal: violation of the causal inequality

Milestones (in source order)

Significance

Difficulty

Goal: $K(N)=N^r$

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