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

Motivation

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:

1. Probabilities. Relative frequencies converge to the same limit for every ensemble prepared by a given preparation.
2. 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.
3. Subspaces. A system whose state is constrained to an $M$-dimensional subspace behaves like a system of dimension $M$.
4. Composite systems. A composite of systems $A$ and $B$ has $N=N_AN_B$ and $K=K_AK_B$.
5. 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

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)):

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

Motivation

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

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

Timeline.

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

Setting

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

and after the detector has measured photon 1 it is

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

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

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

Formalization targets

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

The 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

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

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

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

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

1. 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}$.
2. Lemma 18 (p. 19). On $[-1,1]$, $f_b = S_{b,b}$ exactly:

3. Display (89) (p. 21). $c_{b,j} \le e^{-j^2/b}$.
4. 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

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

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

(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:

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

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)

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

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

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

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

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)$:

Milestones

1. 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$.
2. 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$.
3. Eqs. (10)–(13). No assignment $A_j, B_j \in\{\pm1\}$ satisfies all four GHZ constraints.
4. 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$.
5. 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).
6. Section III (B). Local causality implies non-signalling.
7. Eq. (29). Quantum non-signalling for the GHZ state, with Alice's marginal $P_1(\pm1\mid\hat x,\psi)=\tfrac12$.
8. 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

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

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.

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

Formalization targets

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

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

Formalization scope

Conventions the statements commit to:

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