Quantum Information

Motivation

Quantum information often describes a system through a state shared among many small registers. One would like to replace the state on a few registers by a product of their individual states, because product states are easier to estimate and optimize over. The usual finite quantum de Finetti theorems obtain such approximations from permutation symmetry. A physical preparation, however, need not be symmetric. Berta, Borderi, Fawzi and Scholz give a quantitative statement that instead selects the retained registers at random and conditions on measurements of other registers. Their Theorem 2.5 is the target here.

The authors place this result alongside their hierarchy for constrained bilinear optimization, but the theorem without symmetry is independent of the hierarchy. In §2.6 they compare its polynomial dependence on the local dimension and the number of retained registers with the earlier no-symmetry approximation discussed in their reference [12]. The result identifies exactly what random selection and measurement can supply when a global permutation-invariance hypothesis is unavailable.

Setting

Let $B$ be a quantum system of dimension $d_B$, and let $\rho$ be an arbitrary density operator on $n$ copies of $B$. Choose a uniformly random permutation of these copies. Its first $k$ positions form an ordered tuple $\vec i=(i_1,\ldots,i_k)$ of systems to retain; the remaining $r=n-k$ positions form an ordered tuple $\vec j=(j_1,\ldots,j_r)$ available for measurement. There is no symmetry condition on $\rho$.

A measurement on $B$ has finitely many outcomes $z$ and positive operators $M_z$ whose sum is the identity. Measure the first $m$ systems $j_1,\ldots,j_m$, where $0\le m\le r$, and condition the retained state on the observed outcomes. Write $\rho_{\vec i\mid z}$ for that conditional state and $\rho_{i_s\mid z}$ for its marginal on the $s$th retained system. The trace norm $\|X\|_1=\operatorname{Tr}\sqrt{X^\dagger X}$ measures the error between $\rho_{\vec i\mid z}$ and $\rho_{i_1\mid z}\otimes\cdots\otimes\rho_{i_k\mid z}$. The expectation is over the uniform permutation and the measurement outcomes, with their Born-rule probabilities.

The distortion with side information of a fixed measurement is the largest ratio between an input trace norm and the norm left after measuring only its $B$ factor. The input ranges over Hermitian operators on $A\otimes B$, over every finite-dimensional side system $A$, with zero partial trace on both $A$ and $B$. The paper's $f(B\mid\cdot)$ is the infimum of this distortion over all measurements on $B$ equation (10). A state two-design is a finite family of rank-one projectors whose average second tensor power is the projector onto the symmetric subspace with the normalization in Lemma D.1. The projectors give an explicit measurement with distortion at most $d_B^2(d_B+1)$.

Formalization targets

The principal target is the explicit form of Theorem 2.5. For $1\le k\le n$, put $r=n-k$. With the two-design measurement, some $m\in\{0,\ldots,r\}$ satisfies

$$\mathbb E_{\vec i,\vec j,z}\left\|\rho_{\vec i\mid z}-\bigotimes_{s=1}^k\rho_{i_s\mid z}\right\|_1 \le k d_B^2(d_B+1)\sqrt{\frac{(2\ln 2)(k-1)\log_2 d_B}{r+1}} \le \frac{3k^{3/2}d_B^3\log_2 d_B}{\sqrt{r+1}}.$$

Here the $z$ in the expectation is the outcome string for the first $m$ members of $\vec j$. The same $m$ is chosen before taking that expectation. This rate is stated with its constants and its two consecutive inequalities; an existence assertion without the error bound would lose the theorem's content.

The milestone path also states the telescoping trace-norm inequality of equation (12), the measurement estimate of Lemma D.1, and the final averaged inequality on p. 11. A companion milestone treats any fixed POVM with its own distortion. That formulation captures the proof's arbitrary-measurement step without treating the infimum $f(B\mid\cdot)$ as if every measurement attained it.

Significance

For an arbitrary multipartite state, random ordering and conditioning give one measured prefix length at which the selected registers have small expected distance from a product. The explicit rate is polynomial in $d_B$ and $k$ and decays as $1/\sqrt{n-k+1}$. It therefore gives a quantitative approximation guarantee under a selection rule that can be applied without first establishing exchangeability Berta et al., §2.6.

The theorem is proved in the paper; the work here is to express its state, measurement, conditional distribution, and norm bound in Lean and to connect the estimate to reusable finite-dimensional quantum-information definitions. The local statements are currently proof obligations, not machine-checked proofs. The published density-operator, trace-norm, and partial-trace definitions are reused. Once proved, the statements can serve as a precise interface for subsequent formal work on randomized subsystem selection and information-theoretic decoupling.

Difficulty

Randomly choosing systems does not turn the original state into a product state. A direct bound on the distance to a product can be large even when each one-system marginal is simple, because correlations among the retained systems remain. Equation (12) breaks the total error into successive correlation terms; the paper controls their average by measuring other systems and using information-theoretic estimates. A second difficulty is that a measurement can erase distinctions between different input operators. The two-design estimate supplies a dimension-dependent bound on that loss, uniformly over the size of a side system.

The printed theorem leaves the measurement $M_B$ unspecified while using the minimum distortion over all measurements. A trivial measurement cannot satisfy that reading. The proof explicitly permits the measurement built from a state two-design, with $d_B^2(d_B+1)$ replacing $f(B\mid\cdot)$; that is the measurement used in the goal proof of Theorem 2.5, p. 10.

Formalization scope

The $B$ system has basis Fin dB; $n$ copies have basis Fin n → Fin dB. The formalization writes $n=k+r$, assumes $k\ge1$, and ranges over $m\le r$. A state is a positive semidefinite complex matrix with trace one. Permutations act on the copy coordinates, and their finite uniform average models the paper's random ordered tuples. Measurement outcomes are finite words; the conditional state divides the unnormalized post-measurement state by its probability. A zero-probability outcome uses Lean's zero inverse and contributes zero to the weighted expectation. The existence of a state and of a nonempty two-design rules out zero-dimensional and empty-outcome instances in the goal.

The fixed-measurement distortion and $f(B\mid\cdot)$ take values in extended nonnegative reals, so a measurement that destroys a nonzero operator has infinite distortion. The logarithm is base two except for $\ln 2$. The definitions use the paper's unnormalized trace norm, with no factor $1/2$. No mutual-information estimate or Pinsker inequality is assumed in the goal: both belong to possible proofs. Contributions proving the stated milestones, the positivity and normalization of the conditional states, or reusable trace-norm facts for finite tensor products all advance the target.

Selected references

• M. Berta, F. Borderi, O. Fawzi and V. B. Scholz, Semidefinite programming hierarchies for constrained bilinear optimization, Mathematical Programming, 2021; arXiv:1810.12197v3.

Motivation

Many problems in quantum information theory ask for the maximum of a linear functional over pairs of quantum states, one on each of two systems, subject to linear constraints on each state. The best success probability of an approximate quantum error-correcting code of given size is of this form: the encoder and the decoder are quantum channels, their Choi matrices are states with fixed marginals, and the objective is bilinear in the two (Berta, Borderi, Fawzi & Scholz, arXiv:1810.12197, §4). Such constrained bilinear programs are nonconvex. Seesaw methods give lower bounds that often converge in practice, but they offer no guarantee of global optimality. What is needed is a hierarchy of efficiently computable outer bounds that converges to the optimum, with an explicit rate.

For the unconstrained problem, the optimisation over separable states, such a hierarchy is classical: the Doherty–Parrilo–Spedalieri hierarchy of $n$-extendible states, whose convergence follows from finite quantum de Finetti theorems (Christandl, König, Mitchison & Renner 2007; Brandão & Harrow 2013). The standard de Finetti approximant is, however, a mixture of product states that need not satisfy the linear constraints, so it says nothing about the constrained problem. The paper proves a de Finetti theorem with linear constraints (Theorem 2.3) and derives from it a semidefinite hierarchy for constrained bilinear programs with a convergence guarantee (Theorem 3.1).

Setting

A $d$-dimensional quantum system has operator space $\mathcal S=\mathbb C^{d\times d}$; a state is a positive semidefinite $W\in\mathcal S$ with $\mathrm{Tr}\,W=1$. Let $A$ and $B$ be systems of dimensions $d_A$ and $d_B$. The data are an objective $G_{AB}\in\mathcal S_A\otimes\mathcal S_B$, arbitrary linear maps $\Lambda_{A\to C_A}:\mathcal S_A\to\mathcal S_{C_A}$ and $\Gamma_{B\to C_B}:\mathcal S_B\to\mathcal S_{C_B}$, and matrices $X_{C_A}$, $Y_{C_B}$. The constrained bilinear program is

$$Q=\max\ \mathrm{Tr}[G_{AB}(W_A\otimes W_B)]\quad\text{s.t. } W_A,W_B\ \text{states},\quad \Lambda_{A\to C_A}(W_A)=X_{C_A},\quad \Gamma_{B\to C_B}(W_B)=Y_{C_B}.$$

For $n\ge1$ let $B_1,\dots,B_n$ be copies of $B$. A state $W_{AB_1^n}$ on $A\otimes B_1\cdots B_n$ is symmetric with respect to $A$ if it is invariant under every permutation $\mathcal U^\pi_{B_1^n}$ of the copies $B_1,\dots,B_n$, $\pi\in\mathfrak S_n$. Write $W_{B_1^n}=\mathrm{Tr}_A W_{AB_1^n}$, $W_{B_1^{n-1}}=\mathrm{Tr}_{B_n}W_{B_1^n}$ and $W_{AB_1}=\mathrm{Tr}_{B_2^n}W_{AB_1^n}$. The level-$n$ program is

$$\mathrm{SDP}_n=\max\ \mathrm{Tr}[G_{AB}W_{AB_1}]\quad\text{s.t. } W_{AB_1^n}\ \text{a state, symmetric with respect to } A,$$ $$(\Lambda_{A\to C_A}\otimes\mathcal I_{B_1^n})(W_{AB_1^n})=X_{C_A}\otimes W_{B_1^n},\qquad (\mathcal I_{B_1^{n-1}}\otimes\Gamma_{B_n\to C_B})(W_{B_1^n})=W_{B_1^{n-1}}\otimes Y_{C_B}.$$

It is a semidefinite program of size polynomial in $d_A$ and $d_B^n$.

The rate involves the trace norm $\|X\|_1=\mathrm{Tr}|X|$, the Schatten $\infty$-norm $\|G\|_\infty$ (largest singular value), and the minimal distortion with side information of $B$,

$$f(B|\cdot)=\inf_{\mathcal M_B}\ \sup_{\substack{\xi_{AB}^\dagger=\xi_{AB}\\ \xi_A=0,\ \xi_B=0}}\frac{\|\xi_{AB}\|_1}{\|(\mathcal I_A\otimes\mathcal M_B)(\xi_{AB})\|_1},$$

the infimum over measurements $\mathcal M_B$ on $B$ and the supremum over all finite-dimensional $A$; $f(A,B)$ is the analogue with product measurements $\mathcal M_A\otimes\mathcal M_B$. Throughout, $\log$ is base 2.

Formalization targets

Goal: Theorem 3.1 with its explicit rate

$$Q\ \le\ \mathrm{SDP}_n\ \le\ Q+\|G_{AB}\|_\infty\,d_B^2(d_B+1)\sqrt{\frac{(2\ln2)\log d_A}{n}}\quad(n\ge1),\qquad Q=\lim_{n\to\infty}\mathrm{SDP}_n.$$

The page states $0\le\mathrm{SDP}_n-Q\le\mathrm{poly}(d)/\sqrt n$ with $d=\max\{d_A,d_B\}$. The goal makes explicit the rate the proof gives.

Milestones, in attack order

1. Lemma 2.1 (p. 6): for a permutation-invariant classical-quantum state $\rho_{AZ_1^n}$ there is $0\le m<n$ with $\mathbf E_{z_1^m}\|\rho_{AZ_{m+1}|z_1^m}-\rho_{A|z_1^m}\otimes\rho_{Z_{m+1}|z_1^m}\|_1^2\le(2\ln2)\log d_A/n$.
2. Lemma D.1 (p. 29): for a state two-design $\{P_z\}$ and $\mathcal M_B$ with effects $\frac{d_B}{t}P_z$, $\|(\mathcal I_A\otimes\mathcal M_B)(\xi_{AB})\|_1\ge\|\xi_{AB}\|_1/(d_B^2(d_B+1))$ for every Hermitian $\xi_{AB}$.
3. Existence of state two-designs in every dimension (p. 29).
4. $f(B|\cdot)\le d_B^2(d_B+1)$ (p. 6).
5. Conditional constraints (p. 8): the states obtained by measuring $B_1,\dots,B_m$ and conditioning satisfy $\Lambda(\rho_{A|z_1^m})=X_{C_A}$ and $\Gamma(\rho_{B_{m+1}|z_1^m})=Y_{C_B}$.
6. Theorem 2.3 (p. 7): under the constraints of $\mathrm{SDP}_n$, $\|\rho_{AB}-\sum_ip_i\sigma^i_A\otimes\omega^i_B\|_1\le\min\{f(A,B),f(B|\cdot)\}\sqrt{(2\ln2)\log d_A/n}$ with states $\Lambda(\sigma^i_A)=X_{C_A}$, $\Gamma(\omega^i_B)=Y_{C_B}$.
7. Eq. (3) (p. 2): $Q$ equals the maximum over mixtures of feasible product states.
8. Hölder step (p. 11): $\mathrm{Tr}[GW]\le\mathrm{Tr}[GV]+\|G\|_\infty\|W-V\|_1$.
9. $0\le\mathrm{SDP}_n-Q$ (p. 11).

Significance

Theorem 3.1 turns a nonconvex problem into a sequence of semidefinite programs whose values decrease to the optimum at rate $O(1/\sqrt n)$, with a constant that depends polynomially on $d_B$ and logarithmically on $d_A$. Every level is a certified upper bound; together with any feasible point it brackets $Q$. The same argument applied to channel fidelities gives converging outer bounds on the success probability of approximate quantum error correction (§4 of the paper), and the constrained de Finetti theorem is the key step there as well. Theorem 2.3 is of independent interest: it is the first finite de Finetti theorem in which the approximating separable state inherits linear constraints of the extension.

The results are proved in the paper; none of them has been machine-checked. A complete formalization requires the quantum relative entropy and mutual information with their chain rule, the quantum Pinsker inequality, state two-designs and their existence, and a weighted Hölder inequality for Schatten norms; most of this is absent from Mathlib, and each piece is reusable beyond this mission.

Difficulty

The obvious route measures every copy $B_i$ with a fixed informationally complete measurement and uses the resulting classical de Finetti statement. This approximates $\rho_{AB}$ by a mixture of product states, but the states in the mixture need not satisfy $\Gamma(\omega^i)=Y$, and projecting them onto the constraint set destroys the error bound. The paper instead conditions on the outcomes of only $m$ copies and keeps $B_{m+1}$ quantum; the constraint on $B_n$ then transfers to the conditional state of $B_{m+1}$ by symmetry. Making this rigorous needs the chain rule of conditional mutual information with classical conditioning, and the distortion of the measurement must be bounded independently of the side system $A$, which is what Lemma D.1 provides. The Schatten-norm estimate there is elementary but requires a weighted Hölder inequality and a careful choice of weight.

Formalization scope

Systems are finite index types: $A\otimes B_1\cdots B_N$ is indexed by Fin dA × (Fin N → Fin dB), $\otimes$ is Mathlib's Kronecker product, and the permutation action permutes the word in Fin N → Fin dB. States, trace norm and partial traces are the published definitions WildeQIT_IsDensityOperator, WildeQIT_traceNorm and WildeQIT_partialTrace. The linear maps $\Lambda$, $\Gamma$ are arbitrary $\mathbb C$-linear maps (not assumed positive or trace preserving), applied blockwise to one tensor factor. The objective is the real part of $\mathrm{Tr}[G\,W]$, equal to $\mathrm{Tr}[G\,W]$ for Hermitian $G$. Each "max" is the supremum of the set of objective values over the feasible set, never over all matrices. Wherever the page has $n\ge1$ copies of $B$, the Lean has n + 1: SDPval … n is the page's $\mathrm{SDP}_{n+1}$, and the bounds have denominator $n+1$. The distortions $f(A,B)$ and $f(B|\cdot)$ take values in $[0,\infty]$; the standalone bound on $f(B|\cdot)$ assumes $d_B\ge1$.

No feasibility hypothesis is added to the goal. The feasible sets of $Q$ and of every level are empty or nonempty together, and the empty case reads $0\le0\le0+\dots$. The goal mentions only $Q$, $\mathrm{SDP}_n$, $G$, $d_A$, $d_B$ and $n$; a formalization in which $Q$ or $\mathrm{SDP}_n$ were free real numbers, or in which the de Finetti mixture was not required to satisfy the constraints, would be a different and much weaker statement.

Contributions are welcome at every milestone, and especially in the reusable infrastructure: quantum relative entropy and mutual information on matrices, the quantum Pinsker inequality, unitary and state designs, and Hölder inequalities for Schatten norms.

Selected references

• M. Berta, F. Borderi, O. Fawzi, V. B. Scholz, Semidefinite programming hierarchies for constrained bilinear optimization, Mathematical Programming, 2021; arXiv:1810.12197v3. https://arxiv.org/abs/1810.12197
• F. G. S. L. Brandão, A. W. Harrow, Quantum de Finetti theorems under local measurements with applications, STOC 2013. https://arxiv.org/abs/1210.6367
• M. Christandl, R. König, G. Mitchison, R. Renner, One-and-a-half quantum de Finetti theorems, Communications in Mathematical Physics 273, 2007. https://arxiv.org/abs/quant-ph/0602130
• A. C. Doherty, P. A. Parrilo, F. M. Spedalieri, Complete family of separability criteria, Physical Review A 69, 2004. https://arxiv.org/abs/quant-ph/0308032

Motivation

A quantum algorithm for a system of linear equations must turn operations it can implement into an approximation of the inverse of the system matrix. For a Hermitian matrix, time evolution $e^{-iAt}$ is such an operation. Childs, Kothari and Somma use a Fourier expansion of the scalar reciprocal $1/x$ to express an approximation to $A^{-1}$ as a finite linear combination of these evolutions. Their paper reports an exponential improvement in the dependence on the requested precision over earlier linear-systems methods. The scalar approximation in Lemma 11 is the mathematical input to their Fourier algorithm and to the query and gate analyses in Theorem 3. This mission isolates that approximation and the Gaussian estimates stated around it. Theorem 3's complexity claims themselves are outside the present formalization. Childs, Kothari and Somma, §3, pp. 10–14.

Setting

Fix a condition number $\kappa\ge1$. The scalar spectral domain is

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

It contains the real eigenvalues permitted after the paper's normalization and excludes zero, where the reciprocal is undefined. For an accuracy $\varepsilon>0$, two functions are $\varepsilon$-close on $D_\kappa$ when their difference has magnitude at most $\varepsilon$ at every point of that domain. A complex-valued approximant is compared with $1/x$ as a complex number. The paper gives this domain and closeness convention before the Fourier construction. Childs, Kothari and Somma, pp. 9–10.

The intermediate function $g_{y_J,z_K}(x)$ is a truncated Gaussian Fourier integral. It integrates $z e^{-z^2/2}e^{-ixyz}$ over $-z_K\le z\le z_K$ and then over $0\le y\le y_J$, multiplying by $i/\sqrt{2\pi}$. The finite approximant $h_{J,K,\Delta_y,\Delta_z}(x)$ is a Gaussian Fourier double sum with the same normalization and phase. Its samples are $y_j=j\Delta_y$ for $j=0,\ldots,J-1$ and $z_k=k\Delta_z$ for $k=-K,\ldots,K$; each term carries both mesh widths. Thus $J,K$ count the retained samples, while $\Delta_y,\Delta_z$ control their spacing. The sign in the phase and the factor $i$ are part of the definitions. Childs, Kothari and Somma, (18), p. 10, and (21), p. 11.

Formalization targets

Truncation

Lemma 12 says that for cutoffs of scale

$$y_J=\Theta\!\bigl(\kappa\sqrt{\log(\kappa/\varepsilon)}\bigr), \qquad z_K=\Theta\!\bigl(\sqrt{\log(\kappa/\varepsilon)}\bigr),$$

the function $g_{y_J,z_K}$ is $\varepsilon$-close to $1/x$ on $D_\kappa$. The proposal includes the paper's explicit error bound (27) and its Gaussian tail bound (28), as well as the Gaussian Poisson-summation identity of Lemma 13. These are separate reusable targets, not replacements for the approximation theorem. Childs, Kothari and Somma, Lemmas 12–13 and (27)–(28), pp. 11–12.

Finite Fourier sum

The goal is Lemma 11:

$$\left|h_{J,K,\Delta_y,\Delta_z}(x)-\frac1x\right|\le\varepsilon \quad\text{for every }x\in D_\kappa,$$

where

$$J=\Theta\!\left(\frac\kappa\varepsilon\log\frac\kappa\varepsilon\right),\quad K=\Theta\!\left(\kappa\log\frac\kappa\varepsilon\right),\quad \Delta_y=\Theta\!\left(\frac\varepsilon{\sqrt{\log(\kappa/\varepsilon)}}\right),\quad \Delta_z=\Theta\!\left(\frac1{\kappa\sqrt{\log(\kappa/\varepsilon)}}\right).$$

The $\Theta$ statements impose upper and lower bounds with absolute constants, uniformly across $\kappa$ and $\varepsilon$. The requested approximation error is exactly $\varepsilon$, matching the lemma's claim. The four scales specify both the size of the finite expansion and its mesh. Childs, Kothari and Somma, Lemma 11, p. 10.

Significance

The finite sum provides the paper's Fourier route from scalar reciprocal approximation to a linear combination of time-evolution operators. Its sample counts and spacings are the quantities that enter the algorithm's implementation costs. A result that only asserted approximation after arbitrarily many samples would not express the bound used there. The truncated integral and Poisson identity also remain useful for other Gaussian quadrature and Fourier-sampling arguments. Childs, Kothari and Somma, §§3.1–3.2, pp. 11–14.

The paper proves these claims on paper. This proposal asks for machine-checked Lean proofs of the scalar statements, including the complex normalization, the finite and infinite sum conventions, and the uniform scale bounds. It does not assert that the quantum algorithm, its Hamiltonian simulation subroutines, or its query and gate complexity theorems have been formalized.

Difficulty

The infinite Gaussian Fourier representation alone does not specify a finite implementable expansion. Restricting both integrals introduces two truncation errors, while replacing them by samples adds discretization and periodic-aliasing effects. These errors have to be controlled simultaneously with $J$, $K$, $\Delta_y$, and $\Delta_z$ at the scales stated in Lemma 11. Merely taking the mesh arbitrarily fine gives approximation without the theorem's finite-size bounds. The proof also uses a complex Fourier phase although its target is real, and its infinite sums must have their ordinary convergent meaning. Childs, Kothari and Somma, proof of Lemma 11, pp. 13–14.

Formalization scope

The Lean development uses $\mathbb R$ for $x,\kappa,\varepsilon$ and the cutoff and mesh parameters, $\mathbb C$ for $g$ and $h$, and the complex norm for closeness. Finite sums use exactly $0\le j<J$ and $-K\le k\le K$; the integral for $g$ is iterated and has nonnegative upper cutoffs. The optional identity (20) is also an iterated integral, with the $z$ integral evaluated before the $y$ integral. Infinite sums in Lemma 13 are over $\mathbb Z$. The Gaussian integrals and series in the statements are convergent, so Lean's totalized integral and sum conventions do not supply artificial zero values.

The paper's condition-number convention is recorded as $\kappa\ge1$ and Corollary 10's operating range as $0<\varepsilon<1/2$. Those conditions keep $D_\kappa$ nonempty and $\log(\kappa/\varepsilon)$ positive. The unnumbered reciprocal-exponential bound from p. 13 has $x\ne0$ explicitly, because the printed fractions have no value at zero. The $\Theta$ bounds quantify their constants before the problem parameters. In particular, choices with unbounded sample counts or vanishing mesh widths cannot satisfy the goal solely by brute-force approximation.

A complete development needs reusable Gaussian integration and tail estimates, complex exponential identities, summability of Gaussian integer series, and Poisson summation in Mathlib's analytic setting. Contributions that establish these general facts, the stated milestones, or Lemma 11 with its original bounds all fit this scope. This mission uses the reviewed shared definition of $D_\kappa$. Childs, Kothari and Somma, pp. 9–14.

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 Journal on Computing 46(6), 2017; arXiv:1511.02306v2.

Motivation

Many classical search algorithms are random walks: a Markov chain $P$ on a finite state space $X$ is run until it hits a marked state. Szegedy (2004) attached to every such chain a unitary quantum walk $W(P)$, and Magniez, Nayak, Roland and Santha (SIAM J. Comput. 2011, arXiv:quant-ph/0608026) used it to search quadratically faster than the classical walk for every reversible ergodic chain. The search runs Grover-style rotations, and each rotation needs the reflection $\mathrm{ref}(\pi)$ about the stationary state $|\pi\rangle$. Preparing $|\pi\rangle$ exactly can cost far more than one step of the walk, so the paper builds an approximate reflection $R(P)$ from the walk alone, by phase estimation. Theorem 6 of the paper is the guarantee for that circuit, and this mission formalizes it.

Timeline:

• Jordan, 1875. Two subspaces of a Euclidean space decompose it into one- and two-dimensional invariant pieces ("principal angles").
• Cleve, Ekert, Macchiavello and Mosca, 1998 (Proc. R. Soc. A). The phase-estimation circuit $C(U)$ and its output distribution (Theorem 5 of the paper).
• Szegedy, 2004. The walk $W(P)$, and its spectrum in terms of the singular values of the discriminant matrix (Theorem 4 of the paper).
• Magniez, Nayak, Roland and Santha, 2007/2011. The circuit $R(P)$ and Theorem 6, the search algorithm (Theorem 7), and the bound $\Delta(P)\ge2\sqrt{\delta(P)}$ relating the phase gap to the eigenvalue gap.

Setting

$X$ is a finite set of size $n$. A Markov chain is a row-stochastic matrix $P=(p_{xy})_{x,y\in X}$. It is ergodic if some power of $P$ has all entries positive. A stationary distribution $\pi$ satisfies $\pi_x>0$, $\sum_x\pi_x=1$ and $\sum_x\pi_xp_{xy}=\pi_y$. The time-reversed chain $P^*$ is defined by $\pi_xp_{xy}=\pi_yp^*_{yx}$, and $P$ is reversible if $P^*=P$.

The space is $\mathcal H=\mathbb C^{X\times X}$ with basis $|x\rangle|y\rangle$. Put $|p_x\rangle=\sum_y\sqrt{p_{xy}}\,|y\rangle$ and $|p^*_y\rangle=\sum_x\sqrt{p^*_{yx}}\,|x\rangle$, and

$$\mathcal A=\mathrm{Span}(|x\rangle|p_x\rangle:x\in X),\qquad \mathcal B=\mathrm{Span}(|p^*_y\rangle|y\rangle:y\in X).$$

For a subspace $\mathcal K$, $\mathrm{ref}(\mathcal K)=2\Pi_{\mathcal K}-\mathrm{Id}$, where $\Pi_{\mathcal K}$ is the orthogonal projector onto $\mathcal K$. The quantum walk is $W(P)=\mathrm{ref}(\mathcal B)\cdot\mathrm{ref}(\mathcal A)$, and the stationary state is $|\pi\rangle=\sum_x\sqrt{\pi_x}\,|x\rangle|p_x\rangle$.

The discriminant matrix is $D(P)=(\sqrt{p_{xy}p^*_{yx}})_{x,y}$. Its singular values lie in $[0,1]$. The phase gap $\Delta(P)$ is $2\theta$, where $\theta$ is the smallest angle in $(0,\pi/2)$ such that $\cos\theta$ is a singular value of $D(P)$.

The phase-estimation circuit $C(U)$ acts on $\mathbb C^\iota\otimes\mathbb C^{2^s}$. It is

$$C(U)=(\mathrm{Id}\otimes F^\dagger)\Big(\sum_{j<2^s}U^j\otimes|j\rangle\langle j|\Big)(\mathrm{Id}\otimes H^{\otimes s}),$$

where $H^{\otimes s}$ is the Walsh–Hadamard matrix and $F$ is the $2^s$-point Fourier transform.

The circuit $R(P)$ uses $s=\lceil\log_2(2\pi/\Delta(P))\rceil$ and acts on $\mathcal H\otimes(\mathbb C^{2^s})^{\otimes k}$. It is built in three steps:

1. $V$ applies $C(W(P))$ $k$ times, each time to the system register and a fresh ancilla register.
2. $F_{\neq0}$ multiplies by $-1$ every basis state with a non-zero estimate in some register.
3. Then $R(P)=V^\dagger F_{\neq0}V$.

Formalization targets

Goal: Theorem 6, properties 2 and 3

For $P$ ergodic and reversible on $n\ge2$ states, and every integer $k\ge0$:

$$R(P)\,|\pi\rangle|0^{ks}\rangle=|\pi\rangle|0^{ks}\rangle,\qquad \big\|(R(P)+\mathrm{Id})\,|\psi\rangle|0^{ks}\rangle\big\|\le2^{1-k}\|\psi\|\quad(\psi\in\mathcal A+\mathcal B,\ \psi\perp|\pi\rangle).$$

Milestones

The milestones follow the order in which the paper's proof uses them:

1. Theorem 4 (Szegedy). The spectrum of $W(P)$ on $\mathcal A+\mathcal B$. On that space $W(P)$ has the eigenvalues $1$ (on $\mathcal A\cap\mathcal B$), $-1$, and $e^{\pm2i\theta}$ for $\cos\theta$ a singular value of $D(P)$ in $(0,1)$, with matching multiplicities. The mission has two items for it: the full statement, and the direction the proof uses.
2. §3.2. For ergodic reversible $P$, $|\pi\rangle$ is the only $1$-eigenvector of $W(P)$ in $\mathcal A+\mathcal B$, up to scalars, and every other eigenvalue $\mu$ there satisfies $|1-\mu|\ge|1-e^{i\Delta(P)}|$.
3. Theorem 5, properties 2 and 3. $C(U)$ fixes $|\psi\rangle|0^s\rangle$ when $U\psi=\psi$. If $U\psi=e^{2i\theta}\psi$ with $\theta\in(0,\pi)$, it outputs $|\psi\rangle|\omega\rangle$ with $|\langle0^s|\omega\rangle|=|\sin(2^s\theta)|/(2^s\sin\theta)$.
4. Single-copy bound. For $\Delta/2\le\theta\le\pi-\Delta/2$ and the $s$ above, $|\sin(2^s\theta)|/(2^s\sin\theta)\le1/2$.
5. $k$-copy bound. For $\psi\in\mathcal A+\mathcal B$ with $\psi\perp|\pi\rangle$, the all-zero-estimate component $\psi_0$ of $V|\psi\rangle|0^{ks}\rangle$ has $\|\psi_0\|\le2^{-k}\|\psi\|$. For every $\psi$, $\|(R(P)+\mathrm{Id})|\psi\rangle|0^{ks}\rangle\|=2\|\psi_0\|$.

Significance

Theorem 6 replaces the reflection about $|\pi\rangle$ with a circuit that only calls the walk. Its cost scales as $1/\Delta(P)$ rather than as the cost of preparing $|\pi\rangle$. Combined with $\Delta(P)\ge2\sqrt{\delta(P)}$, where $\delta(P)$ is the eigenvalue gap, this gives the search cost $S+\frac1{\sqrt\varepsilon}\big(\frac1{\sqrt\delta}U+C\big)$ of Theorem 7, up to logarithmic factors. The same approximate-reflection device recurs in later quantum-walk and amplitude-amplification algorithms.

The results are proved in the paper, which takes Theorem 4 from Szegedy and Theorem 5 from Cleve et al. As far as the platform index shows, none of Theorems 4, 5 or 6 has a machine-checked proof. The mission produces three reusable components: a Lean definition of the Szegedy walk and of the phase-estimation circuit, a formal Jordan-type spectral theorem for products of two reflections, and the analysis of phase estimation on an eigenvector.

Difficulty

Most of the work is linear algebra. The proof of Theorem 6 has a short outline: expand $\psi$ in eigenvectors of $W(P)$, apply Theorem 5 to each, and bound each amplitude by $1/2$. Three steps carry the weight:

• Theorem 4. The eigen-decomposition of $W(P)$ on $\mathcal A+\mathcal B$ is Jordan's two-subspace decomposition, with the multiplicities read off the singular value decomposition of $D(P)$. The decomposition has to be built, and the cases at singular values $0$ and $1$ have to be handled separately.
• Uniqueness of $|\pi\rangle$. This step needs ergodicity, through Perron–Frobenius, and reversibility, because $D(P)$ is then symmetric and its singular values are the moduli of the eigenvalues of $P$. Without reversibility $D(P)$ can have the singular value $1$ twice, and property 3 then fails.
• Repetition. The $k$ phase estimations share one system register. Their product acts on an eigenvector as a tensor power on the ancillas. This needs the eigenvectors of the unitary $W(P)$ restricted to the invariant subspace $\mathcal A+\mathcal B$ to be orthogonal.

Formalization scope

• $\mathcal H$ is EuclideanSpace ℂ (X × X), with the first coordinate the first register.
• The ancilla register is indexed by Fin (2^s), and $k$ registers by Fin k → Fin (2^s); the all-zeros state is the zero index.
• $\mathrm{ref}(\mathcal K)$ is Mathlib's Submodule.reflection.
• The stationary distribution $\pi$ is passed as data with its defining hypotheses. "Ergodic" is Matrix.IsPrimitive.
• Singular values of the real matrix $D(P)$ are LinearMap.singularValues.
• When $D(P)$ has no singular value in $(0,1)$, the paper leaves $\Delta(P)$ undefined, and the formalization sets $\Delta(P)=\pi$.
• $\log_2$ is Real.logb 2 and the ceiling is Nat.ceil.

Deviations from the page.

• Reversibility, the standing assumption of §3.2, is a hypothesis of the goal.
• Property 3 is stated for vectors and is homogeneous in $\|\psi\|$.
• Theorem 5 is stated for any finite-dimensional unitary, not only $2^m\times2^m$, and with $|\sin(2^s\theta)|$, because the printed right-hand side can be negative.
• The single-copy bound also covers the eigenvalue $-1$.

Only exact statements are formalized. The cost halves (gate counts, calls to $c$-$W(P)$, "$s\in\log_2(1/\Delta)+O(1)$", the qubit count, uniformity) are out of scope.

The circuit $R(P)$ is the explicit composition above, built from $C(W(P))$. It is neither "some circuit with properties 2–3" nor anything defined through the projector onto $|\pi\rangle$, either of which would make the goal a tautology.

Contributions welcome: proofs of the milestones, Jordan's lemma for two subspaces as a standalone result, and the bound $\Delta(P)\ge2\sqrt{\delta(P)}$ of §3.3.

Selected references

• F. Magniez, A. Nayak, J. Roland, M. Santha, Search via Quantum Walk, SIAM J. Comput. 40(1), 2011. https://arxiv.org/abs/quant-ph/0608026 (v4), https://doi.org/10.1137/090745854
• M. Szegedy, Quantum speed-up of Markov chain based algorithms, FOCS 2004. https://doi.org/10.1109/FOCS.2004.53
• R. Cleve, A. Ekert, C. Macchiavello, M. Mosca, Quantum algorithms revisited, Proc. R. Soc. Lond. A 454, 1998. https://doi.org/10.1098/rspa.1998.0164
• C. Jordan, Essai sur la géométrie à n dimensions, Bull. Soc. Math. France 3, 1875. https://doi.org/10.24033/bsmf.90

Motivation

Grover's algorithm finds a marked element among $N$ with $O(\sqrt N)$ queries by alternating two reflections: one about the initial state and one that flips the sign of marked states. In quantum-walk search, the initial state $|\pi\rangle$ encodes the stationary distribution of a Markov chain, and the reflection about $|\pi\rangle$ is too expensive to implement exactly. Magniez, Nayak, Roland and Santha (arXiv:quant-ph/0608026, SIAM J. Comput. 2011) obtain the reflection approximately, by phase estimation on the quantum walk, and need a search procedure that tolerates the approximation error without paying extra cost to reduce it. Their Section 4 supplies one: a variant of the recursive amplitude amplification (RAA) of Høyer, Mosca and de Wolf (ICALP 2003) in which the reflection about $|\pi\rangle$ is replaced, at recursion level $i$, by an approximate circuit of precision $\beta_i=\frac{18}{4\pi^3}\gamma/i^2$. The two lemmas of that section, stated "in full generality for potential further applications" (p. 11), are the exact engine of the paper's headline Theorem 3 (search with cost $S+\frac1{\sqrt\varepsilon}(\frac1{\sqrt\delta}U+C)$).

Timeline: Grover (1996) gives quadratic speedup for unstructured search; Brassard, Høyer, Mosca and Tapp (2002) generalize it to amplitude amplification; Høyer, Mosca and de Wolf (2003) introduce RAA to tolerate a bounded-error marking reflection; Szegedy (2004) defines quantum walks for arbitrary reversible chains with detection guarantees; Magniez, Nayak, Roland and Santha (STOC 2007, SIAM 2011) adapt RAA to an approximate initial-state reflection and obtain search, not only detection, for every reversible ergodic chain.

Setting

Let $X$ be a finite set and $M\subseteq X$ a set of marked elements. The state space is $\mathcal H=\mathbb C^{X\times X}$. The initial state $|\pi\rangle\in\mathcal H$ is any unit vector (Lemmas 1 and 2 never use its quantum-walk form), and the marked weight is $p_M=\|\Pi_M|\pi\rangle\|^2$, where $\Pi_M$ projects onto the basis states $|x\rangle|y\rangle$ with $x\in M$.

For each level $i\ge1$ an extra register $K_i$ (a finite-dimensional space with a basis state $|0\rangle$) is given together with a unitary $R_i$ on $\mathcal H\otimes K_i$, playing the role of $R(\beta_i)$:

$$R_i|\pi\rangle|0\rangle=|\pi\rangle|0\rangle,\qquad \|(R_i+\mathrm{Id})|\psi\rangle|0\rangle\|\le\beta_i\|\psi\|\ \text{ whenever }\langle\pi|\psi\rangle=0 .$$

On $\mathcal H\otimes K_1\otimes\cdots\otimes K_T$ the marked subspace $\tilde{\mathcal M}$ consists of states whose first register is marked, and $\mathrm{ref}(\tilde{\mathcal M}^\perp)=\mathrm{Id}-2\Pi_{\tilde M}$.

Approximate RAA$(i,\gamma)$ is the unitary $A_i$ with $A_0=\mathrm{Id}$ and

$$A_i=A_{i-1}\cdot O_i\cdot A_{i-1}^\dagger\cdot\mathrm{ref}(\tilde{\mathcal M}^\perp)\cdot A_{i-1},$$

where $O_i$ multiplies by $-1$ every basis state in which some register $K_j$, $j<i$, is not $|0\rangle$, and otherwise applies $R_i$ to $\mathcal H\otimes K_i$. Write $|\varphi_i\rangle=A_i|\pi\rangle|0^S\rangle$ and $\sin\phi_i=\|\Pi_{\tilde M}|\varphi_i\rangle\|$.

Tolerant RAA$(t_{\max},\gamma)$ first samples $x$ (succeeding with probability $p_M$); otherwise, for $i=1,\dots,t_{\max}$, it applies $A_i$ to the state left over from the previous failed measurement, $|\psi_i\rangle=A_i|\nu^\perp_{i-1}\rangle$ with $|\nu^\perp_0\rangle=|\pi\rangle|0^S\rangle$, and measures $\{\Pi_{\tilde M},\mathrm{Id}-\Pi_{\tilde M}\}$; a failure collapses the state to $|\nu_i^\perp\rangle=\Pi_{\tilde M^\perp}|\psi_i\rangle/\|\Pi_{\tilde M^\perp}|\psi_i\rangle\|$.

Formalization targets

Goal: Lemma 2 (p. 15)

Let $0<\gamma\le1/40$, let $\varepsilon>0$ satisfy $p_M\ge\varepsilon$ whenever $p_M>0$, and let $t_{\max}$ be the smallest non-negative integer with $3^{t_{\max}}\sin^{-1}\sqrt\varepsilon\in[\pi/4,3\pi/4]$. The probability $P_{\rm succ}$ that Tolerant RAA$(t_{\max},\gamma)$ ends with a marked element satisfies

$$M=\emptyset\Rightarrow P_{\rm succ}=0,\qquad p_M>0\Rightarrow P_{\rm succ}\ge\frac1{12}-3\gamma .$$

Lemma 1 (p. 12)

With $t$ the smallest non-negative integer such that $3^t\sin^{-1}\sqrt{p_M}\in[\pi/4,3\pi/4]$, for every $\gamma>0$,

$$\|\Pi_{\tilde M}A_t|\pi\rangle|0^S\rangle\|\ge\frac1{\sqrt2}-\gamma .$$

Milestones

In the order of the proofs: Fact 1 (the error operator $E_i=A_{i-1}O_iA_{i-1}^\dagger-\mathrm{ref}(\varphi_{i-1})$ kills $|\varphi_{i-1}\rangle$ and has norm $\le\beta_i$ on states with clean registers $K_{\ge i}$); the one-level bound $|\sin\phi_{i+1}-\sin3\phi_i|\le\beta_{i+1}|\sin2\phi_i|$; the two trigonometric inequalities on $[0,\pi/4]$; the surrogate bound $\tilde e_i\le\gamma\bar\phi_i/\pi\le\gamma$; Lemma 1; the three terms of the drift recursion (5); and the accumulated drift $\delta_t=\||\psi_t\rangle-|\varphi_t\rangle\|\le\pi/8+9\gamma/8$.

Significance

Lemma 2 turns any family of approximate reflections whose error decays like $1/i^2$ into a search procedure that succeeds with constant probability, needs only a lower bound $\varepsilon$ on $p_M$, and costs $O(3^{t_{\max}})=O(1/\sqrt\varepsilon)$ calls. Combined with the phase-estimation reflection of the paper's Theorem 6 it yields Theorem 3, the general quantum-walk search theorem that has become the standard tool for walk-based algorithms (element distinctness, triangle finding, group commutativity). Nothing in the lemma refers to Markov chains, so it applies to any setting with an approximate reflection about the initial state.

The results are proved in the paper. None of them is machine-checked: the platform holds a formal Grover search with one marked basis state and exact reflections, but no amplitude amplification with approximate or recursive reflections. A formal proof would also settle the steps the paper passes over quickly, notably that the trigonometric inequalities, claimed for angles in $[0,\pi/4]$, are applied to the actual angles $\phi_i$, which may exceed $\pi/4$ by $O(\gamma)$ at the last level.

Difficulty

The ideal analysis (every reflection exact, angle tripled at each level) is a two-dimensional rotation argument. With approximate reflections the state leaves the plane spanned by $|\mu_0\rangle$ and $|\mu_0^\perp\rangle$, and each level both triples the error already present and injects a new one; the errors stay bounded only because $\sum_i\beta_i$ converges and the injection at level $i$ is weighted by $\sin2\phi_i$. Fact 1 is not a restatement of the hypothesis on $R(\beta)$: it holds only because step 4 flips the phase of states whose earlier registers are dirty, and because $A_{i-1}$ never touches $K_{\ge i}$. In Lemma 2 the attempts reuse the leftover state, not a fresh $|\pi\rangle|0^S\rangle$, so the state at the decisive attempt $t$ has drifted; bounding the drift needs the normalised unmarked parts $|\mu_k^\perp\rangle$ to move little from level to level, which again depends on the error bounds of Lemma 1.

Formalization scope

• $\mathcal H\otimes K_1\otimes\cdots\otimes K_T$ is EuclideanSpace ℂ (X × X × ((j : Fin T) → κ (j+1))); operators are complex matrices. Registers are 0-based in Lean (index $j$ is $K_{j+1}$).
• $R_i$ is required only at the precisions $\beta_i$ actually used, which is weaker than the paper's "for any $\beta>0$". Property 3 is stated in the homogeneous form $\le\beta_i\|\psi\|$.
• "Undo" is the conjugate transpose. $t$ and $t_{\max}$ are explicit naturals with "satisfies the condition and no smaller one does". $\sin^{-1}$ is Real.arcsin; the interval is closed.
• The success probability of Tolerant RAA is defined from the measurement rule, $p_M+(1-p_M)\big(1-\prod_{i=1}^{t_{\max}}(1-\|\Pi_{\tilde M}|\psi_i\rangle\|^2)\big)$, with post-measurement states computed from the actual $|\psi_i\rangle$; registers are not reset. The classical sample succeeds with probability $\|\Pi_M|\pi\rangle\|^2$, which is $\sum_{x\in M}\pi_x$ in the paper's walk setting.
• "$M$ non-empty" in Lemma 2 is read as $p_M>0$, as in the paper's proof. Edge-case hypotheses: $\|\pi\|=1$; $\phi_i\le\pi/3$ in the one-level bound (so $\sin3\phi_i\ge0$); $p_M<1$ in the last drift term; $1\le i<t$ and $T\ge t$ in the drift bounds.
• Cost is not formalized: property 1 of $R(\beta)$, the cost $c_2$ of $-\mathrm{ref}(M)$ and every "incurs a cost of order" clause are out of scope. The data-structure subscript $d$ is omitted, as in the paper's own error analysis.
• A formalization in which step 4 applies an exact reflection about $|\pi\rangle$ or $|\varphi_{i-1}\rangle$, or in which the success probability is computed from ideal angles instead of the actual states, would make the lemmas statements about exact RAA; the definitions apply the given $R_i$ and measure the actual states.

Contributions welcome: proofs of the trigonometric milestones and of $\tilde e_i\le\gamma\bar\phi_i/\pi$ (pure real analysis), Fact 1 (finite-dimensional linear algebra with a block structure on registers), and the vector inequality $\|u/\|u\|-v/\|v\|\|\le2\|u-v\|/\|v\|$ that the drift bounds share. The register and controlled-unitary infrastructure is reusable for other recursive quantum algorithms.

Selected references

• F. Magniez, A. Nayak, J. Roland, M. Santha, Search via Quantum Walk, SIAM J. Comput. 40(1), 2011; arXiv:quant-ph/0608026v4. https://arxiv.org/abs/quant-ph/0608026
• P. Høyer, M. Mosca, R. de Wolf, Quantum search on bounded-error inputs, ICALP 2003. https://arxiv.org/abs/quant-ph/0304052
• G. Brassard, P. Høyer, M. Mosca, A. Tapp, Quantum amplitude amplification and estimation, Contemp. Math. 305, 2002. https://arxiv.org/abs/quant-ph/0005055
• L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. https://arxiv.org/abs/quant-ph/9605043
• M. Szegedy, Quantum speed-up of Markov chain based algorithms, FOCS 2004. https://doi.org/10.1109/FOCS.2004.53

Motivation

Bounded-error factoring and exact factoring have different correctness requirements. Repetition until success and increasingly accurate rotations do not automatically give a fixed-gate, worst-case polynomial exact algorithm. The pinned manuscript supplies the research context.

Setting

Circuit instructions use NOT, CNOT, Toffoli, Hadamard and phase primitives, their inverses and singly controlled versions. A classical finite-stack machine generates each encoded circuit from unary input length.

Formalization target

The selected goal is OAI.ExactQuantumFactoring.exact_quantum_factoring. Its central assertion is

$$P(\mathrm{complete\ prime\ factorization\ of}\ N)=1.$$

The theorem states that the defined proposition MainTheorem holds, i.e. there is a family of quantum circuits indexed by input bit length ℓ with three properties. Circuits are lists of instructions on q qubits, each applying one of 20 named gates (the primitives NOT, CNOT, Toffoli, Hadamard and phase, each optionally inverted and optionally given one extra control) to distinct wires; the output state is obtained by applying the instructions in order to the basis state holding the binary digits of N, least significant bit first, on the first ℓ wires, with all other wires zero. First, the family is uniform: a single Turing machine (TM2) with finite stack alphabets computes in polynomial time the encoding of the ℓth circuit from the unary string of length ℓ, where the encoding writes the qubit count, instruction count and each instruction's gate code, inverse and control flags and wire indices in unary. Second, the numbers of qubits and of instructions of the ℓth circuit are both bounded by one fixed polynomial in ℓ with natural-number coefficients. Third, for every ℓ and every integer N ≥ 2 whose binary length is exactly ℓ, the circuit has at least ℓ + n² qubits, where n = max(128, ℓ), and the total squared amplitude on basis states whose output is correct equals exactly 1. A basis state is correct if reading n consecutive blocks of n bits after the input wires, each block as a binary number, gives the nondecreasing list of prime factors of N with multiplicity, padded with zeros to length n.

Significance and status

The output is a sorted list of prime factors with multiplicity in fixed binary blocks, padded with zeros. The target is an existence theorem for a uniform circuit family, not an uploaded executable factoring program. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Uniform generation, polynomial qubit and gate bounds, a fixed finite gate alphabet, and probability-one correctness must all hold together.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Exact quantum factoring over a fixed finite gate set, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Positive partial transpose imposes strong constraints on quantum maps, but composition may retain entanglement. Explicit finite-dimensional examples make that distinction a precise algebraic target. The pinned manuscript supplies the research context.

Setting

The selected maps act on complex 10 by 10 matrices. Complete positivity is quantified over matrix amplifications, while separability is expressed by finite sums of positive tensor factors.

Formalization target

The selected goal is OAI.DimensionTen.main_pair. Its central assertion is

$$\Phi_1=\mathrm{phiOne},\quad\Phi_2=\mathrm{phiTwo},\quad\neg\mathrm{EB}(\Phi_2\circ\Phi_1).$$

The theorem states that there exist maps Φ₁ and Φ₂ from 10×10 complex matrices to 10×10 complex matrices, equal to the defined maps phiOne and phiTwo, each of which is PPT, meaning complex-linear, completely positive, and such that composing with the transpose of the output is also completely positive (complete positivity means that applying the map to one factor of any positive semidefinite block matrix on ℂᵏ⊗ℂ¹⁰, for every k≥1, yields a positive semidefinite matrix). Here phiOne sends A to the 6×6 matrix obtained from the transpose of A by embedding it as a symmetric tensor in ℂ⁴⊗ℂ⁴, applying the tensor square of an explicit 4×4 pencil map built from four integer 6×4 blocks, and compressing to the antisymmetric subspace, then padding it to a 10×10 matrix in the first six coordinates. phiTwo is the Hilbert–Schmidt adjoint of an associated complementary map, which uses a Hodge-type complement matrix, applied to the compression of its input onto the first six coordinates. Moreover, letting Z be the Choi matrix of the composition Φ₂∘Φ₁, a 100×100 matrix with entries given by the images of the matrix units, Z is nonzero; no nonzero product vector u⊗v with u,v∈ℂ¹⁰ lies in the range of Z, that is, whenever Z applied to some w∈ℂ¹⁰ˣ¹⁰ equals u⊗v then u=0 or v=0; and Φ₂∘Φ₁ is not entanglement breaking, where entanglement breaking means completely positive and sending every positive semidefinite amplification to a separable matrix, a finite sum of Kronecker products of positive semidefinite matrices. This theorem is admitted in the source, not proved.

Significance and status

The selected target is the explicit pair of PPT maps in dimension ten, including its nonzero Choi matrix and product-vector obstruction. It does not state a secret-key distillation theorem. The separate 21-dimensional channel is retained as an additional reference. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

PPT properties and non-entanglement-breaking composition require different certificates. The range condition must exclude every nonzero product vector.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

• OAI.DimensionTen.exists_channel_fin21 (Open).

Selected references

• OpenAI, Entanglement with zero distillable secret key in local dimension ten, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Character sums express phase constraints on complex Hadamard matrices. In dimension six these constraints also bear on how many mutually unbiased bases can coexist. The pinned manuscript supplies the research context.

Setting

A complex Hadamard matrix has unit-modulus entries and conjugate-transpose product 6I. Equivalence permits row and column permutations and unit phases. Tao's cubic matrix supplies the exceptional class.

Formalization target

The selected goal is OAI.MUB6.fourier_and_family_bound. Its central assertion is

$$g_H(\pi(1,1,1,-1,-1,-1))=0,\qquad n_{\rm MUB}\leq5.$$

The theorem states a conjunction of two claims about 6x6 complex matrices and mutually unbiased bases in C^6. First, for every complex Hadamard matrix H of order 6 (all entries of modulus 1 and HH = 6I, where H is the conjugate transpose) that is not equivalent to the specific matrix tao, every permutation π of the six coordinates gives g(H, alpha∘π) = 0. Here the character of a column x at an integer exponent vector a is the product over i of x_i^{a_i}, g(H,a) is (1/6) times the sum over the six columns k of H of the character of column k at a, and alpha is the exponent vector (1,1,1,-1,-1,-1), so alpha∘π is alpha with its entries permuted. Equivalence of H and K means K_{ij} = u_i H_{r(i),c(j)} v_j for some row and column permutations r, c and unit-modulus complex phase vectors u and v. The matrix tao has entries ω^{e_{ij}}, where ω = exp(2πi/3) and e is a fixed 6x6 exponent matrix with zero first row and column and a five-cycle pattern of exponents 0, 1, 2 in the remaining 5x5 block. Second, for every natural number n, if there exist n orthonormal bases of C^6 that are pairwise mutually unbiased, meaning |<b_i, b'_j>|^2 = 1/6 for all vectors of two distinct bases, then n ≤ 5. This is stated as an admitted theorem, not a verified proof.

Significance and status

The goal is the conjunction of Fourier vanishing outside the specified equivalence class and the bound on attainable families. The cube-fiber statement is an additional published supporting target with its own hypotheses. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Orthogonality immediately kills certain degree-two characters, but the target concerns a balanced degree-six character and a separate global bound on families of bases.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

• OAI.HadamardSix.rowRatio_cubeFiber_sum_zero (Open).

Selected references

• OpenAI, Exact Fourier certificates for complex Hadamard matrices of order six, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Shannon's entropy power inequality bounds the entropy of a sum of independent random vectors below by the entropies of the summands; it is a basic tool for classical Gaussian channel capacities. In optical communication, addition is replaced by passive mixing of bosonic modes at a beam splitter. Guha, Erkmen and Shapiro conjectured the sharp bosonic analogue, the entropy photon-number inequality (EPnI), stated in terms of the photon number of the thermal state with the same entropy (ITA 2008). If true, it settles the minimum output entropy of thermal attenuators at fixed input entropy and the capacity regions of bosonic broadcast and wiretap channels, which had been reduced to this inequality (PRA 2007).

This mission asks for a formal proof of the EPnI for finite-energy inputs in any finite number of modes, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1948–1965 — Shannon introduces entropy power; Stam (1959) and Blachman (IEEE IT 1965) prove the entropy power inequality.
• 2004 — Capacity of the pure-loss bosonic channel (PRL 2004) and the minimum-output-entropy conjecture (PRA 2004).
• 2007–2008 — Guha, Shapiro and Erkmen relate broadcast capacity to a minimum-output-entropy conjecture; Guha, Erkmen and Shapiro state the EPnI.
• 2011 — Special cases (one-mode number-diagonal inputs) by Das, Sharma and Muthukrishnan (arXiv:1107.2365).
• 2014 — König and Smith prove a quantum entropy power inequality, including $S(\rho_C)\ge\eta S(\rho_A)+(1-\eta)S(\rho_B)$ (IEEE IT 2014); De Palma, Mari and Giovannetti prove the exponential form $e^{S(\rho_C)/n}\ge\eta e^{S(\rho_A)/n}+(1-\eta)e^{S(\rho_B)/n}$ (Nat. Photonics 2014).
• 2015 — Giovannetti, Holevo and García-Patrón solve the Gaussian optimizer conjecture for unconstrained minimum output entropy (CMP 2015).
• 2016–2018 — De Palma, Trevisan and Giovannetti settle one-mode constrained problems (IEEE IT 2017; PRL 2017); De Palma and Trevisan give a rigorous finite-energy conditional EPI (CMP 2018).
• September 2026 — The OpenAI preprint claims the two-input EPnI for all finite-energy inputs (Theorem 1.1, p. 2).

Setting

An $n$-mode bosonic system has Fock space $\ell^2(\mathbb N^n)$ with number basis $|k\rangle$, $k\in\mathbb N^n$. A state is a positive trace-one operator $\rho$; it has finite energy if $\operatorname{Tr}\rho\sum_ja_j^\dagger a_j=\sum_k(k_1+\dots+k_n)\langle k|\rho|k\rangle<\infty$. The von Neumann entropy is $S(\rho)=-\operatorname{Tr}\rho\log\rho$ (natural log). The thermal entropy per mode is

$$g(t)=(t+1)\log(t+1)-t\log t,\qquad t\ge0,$$

increasing from $0$ to $\infty$, and the entropy photon number of $\rho$ is $N(\rho)=g^{-1}(S(\rho)/n)$, the mean photon number per mode of the product thermal state with the same entropy. For independent inputs $\rho_A,\rho_B$ and transmissivity $0\le\eta\le1$, the beam-splitter output $\rho_C$ is the reduced state of the modes $c_j=\sqrt\eta\,a_j+\sqrt{1-\eta}\,b_j$ after passive mixing of $\rho_A\otimes\rho_B$. No independence among the modes within either input is assumed.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every finite $n\ge1$, every pair of finite-energy $n$-mode states $\rho_A,\rho_B$ and every $0\le\eta\le1$,

$$g^{-1}\!\Bigl(\frac{S(\rho_C)}n\Bigr)\ \ge\ \eta\,g^{-1}\!\Bigl(\frac{S(\rho_A)}n\Bigr)+(1-\eta)\,g^{-1}\!\Bigl(\frac{S(\rho_B)}n\Bigr).$$

Thermal inputs with a common mean photon number within each port give equality.

Significance

The result itself. The EPnI is sharper than the exponential quantum entropy power inequality when the two input entropies differ, which is exactly the regime needed for constrained minimum output entropy. The preprint derives the exact minimum output entropy at fixed input entropy for every tensor power of an identical thermal attenuator, with inputs entangled across modes (Corollary 1.2, p. 2), and the exact capacity region of the degraded two-receiver pure-loss broadcast channel (Corollary 7.1, p. 26), completing the converse of Guha, Shapiro and Erkmen.

Formalizing it. The statement involves infinite-dimensional Fock space, trace-class positive operators, continuous functional calculus for the entropy, and the partial trace after a passive unitary. The Lean development builds these concretely in the number basis. A formal proof would give machine-checked infrastructure for quantum entropy on infinite-dimensional spaces, which Mathlib currently lacks. No machine-checked version of any quantum entropy power inequality is known.

Difficulty

Heat-flow (quantum Fisher information) proofs give the linear and exponential bounds, but these are attained only for equal entropies and do not recover the thermal comparison at unequal entropy levels. The preprint instead minimizes a regularized functional over pairs of inputs and must show that minimizers are thermal. This requires an interpolation theorem for diagonal form comparisons (Theorem 3.1, p. 8), attainment and Gibbs regularity of minimizers in infinite dimensions (Lemma 4.1, Proposition 4.2, pp. 15–16), a component entropy-Hessian estimate, and a stationarity identity whose cancellation forces convergence to thermal inputs (Section 6). Compactness relies on the finite-energy hypothesis; without it entropies can be infinite.

Formalization scope

• Fock n is lp (fun _ : Fin n → ℕ => ℂ) 2. A State is a positive bounded operator whose diagonal in the number basis sums (HasSum) to $1$.
• FiniteEnergy ρ is summability of $\sum_k|k|\,\langle k|\rho|k\rangle$.
• entropy ρ is the sum of diagonal entries of $\mathrm{cfc}(-t\log t)(\rho)$; for finite-energy states it is finite, so the tsum is the true entropy.
• gInv s = sInf {t ≥ 0 | s ≤ g t}, the inverse of $g$ on $[0,\infty)$.
• IsBeamSplitterOutput η ρA ρB ρC requires every number-basis entry of $\rho_C$ to be the (convergent) partial-trace sum of the explicitly given beam-splitter coefficients applied to $\rho_A\otimes\rho_B$; the inputs are arbitrary density matrices, so internal entanglement is allowed.
• The hypotheses are satisfiable (e.g. vacuum or thermal inputs) and the conclusion is the inequality as stated.

Selected references

• OpenAI, The entropy photon-number inequality, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-entropy-photon-number-inequality-September-24-2026/paper.pdf
• S. Guha, B. I. Erkmen, J. H. Shapiro, The entropy photon-number inequality and its consequences, ITA Workshop 2008, 128–130. https://doi.org/10.1109/ITA.2008.4601037
• S. Guha, J. H. Shapiro, B. I. Erkmen, Classical capacity of bosonic broadcast communication and a minimum output entropy conjecture, Phys. Rev. A 76 (2007), 032303. https://doi.org/10.1103/PhysRevA.76.032303
• R. König, G. Smith, The entropy power inequality for quantum systems, IEEE Trans. Inf. Theory 60 (2014), 1536–1548. https://doi.org/10.1109/TIT.2014.2298436
• G. De Palma, A. Mari, V. Giovannetti, A generalization of the entropy power inequality to bosonic quantum systems, Nat. Photonics 8 (2014), 958–964. https://doi.org/10.1038/nphoton.2014.252
• G. De Palma, D. Trevisan, The conditional entropy power inequality for bosonic quantum systems, Comm. Math. Phys. 360 (2018), 639–662. https://doi.org/10.1007/s00220-017-3082-8
• V. Giovannetti, A. S. Holevo, R. García-Patrón, A solution of Gaussian optimizer conjecture for quantum channels, Comm. Math. Phys. 334 (2015), 1553–1571. https://doi.org/10.1007/s00220-014-2150-6
• V. Giovannetti, S. Guha, S. Lloyd, L. Maccone, J. H. Shapiro, H. P. Yuen, Classical capacity of the lossy bosonic channel: the exact solution, Phys. Rev. Lett. 92 (2004), 027902. https://doi.org/10.1103/PhysRevLett.92.027902
• C. E. Shannon, A mathematical theory of communication, Bell Syst. Tech. J. 27 (1948). https://doi.org/10.1002/j.1538-7305.1948.tb00917.x