Quantum Information

Motivation

Two observers, Alice and Bob, share a quantum system. Alice performs some intervention (a measurement, possibly followed by discarding part of her apparatus) and Bob, somewhere else, performs his own. If the statistics of Bob's outcomes could depend on what Alice chose to do, Alice could send Bob a message through the shared system alone, and if the two interventions are spacelike separated this would be a signal faster than light. Quantum mechanics and special relativity coexist peacefully only because this does not happen: the no-communication theorem guarantees that Bob's marginal statistics are independent of Alice's intervention whenever the two interventions are "local" to different parts of the system.

The review article of Peres and Terno, Quantum information and relativity theory (Rev. Mod. Phys. 76, 2004), develops the operational toolkit of quantum information (Kraus matrices, positive-operator-valued measures, completely positive maps) in Sec. II.D and then derives, in Sec. II.E, a sufficient algebraic condition for the absence of instantaneous information transfer: all of Alice's Kraus matrices commute with all of Bob's (their Eq. (9)). This mission formalizes that derivation together with the facts about Kraus matrices and complete positivity that the same pages state.

Setting

A quantum state on a finite-dimensional Hilbert space $\mathbb C^d$ is a density matrix $\rho$: a positive semidefinite $d\times d$ complex matrix with $\operatorname{tr}\rho = 1$.

An intervention with outcomes $\mu$ is described by Kraus matrices $A_{\mu m}$, where the label $m$ ranges over a finite set indexing the subsystems discarded at the end of the interaction. When outcome $\mu$ occurs, the state is updated (Eq. (6)) to the unnormalized matrix

$$\rho'_\mu = \sum_m A_{\mu m}\,\rho\,A_{\mu m}^\dagger ,$$

and the probability of outcome $\mu$ is $p_\mu = \operatorname{tr}\rho'_\mu$. The matrices

$$E_\mu = \sum_m A_{\mu m}^\dagger A_{\mu m}$$

(Eq. (8)) are the POVM elements; the intervention is complete when $\sum_\mu E_\mu = \mathbb 1$.

A map $T$ on matrices is positive if it sends positive semidefinite matrices to positive semidefinite matrices, and completely positive if $T\otimes\mathbb 1$, acting blockwise on matrices over $\mathbb C^d\otimes\mathbb C^n$, is positive for every ancilla dimension $n$.

For the no-communication theorem, Alice's Kraus matrices $A_{\mu m}$ and Bob's Kraus matrices $B_{\nu n}$ act on the same finite-dimensional space. The probability that Bob obtains $\nu$, irrespective of Alice's outcome, is (Eq. (10))

$$p_\nu = \sum_\mu \operatorname{tr}\Big(\sum_{m,n} B_{\nu n} A_{\mu m}\,\rho\,A_{\mu m}^\dagger B_{\nu n}^\dagger\Big).$$

Formalization targets

Goal: no-communication (Sec. II.E, Eqs. (9)-(11))

If $[A_{\mu m}, B_{\nu n}] = 0$ for all $\mu, m, \nu, n$, Alice's POVM is complete, and $\rho$ is a density matrix, then for every outcome $\nu$ of Bob

$$\sum_\mu \operatorname{tr}\Big(\sum_{m,n} B_{\nu n} A_{\mu m}\,\rho\,A_{\mu m}^\dagger B_{\nu n}^\dagger\Big) = \operatorname{tr}\Big(\sum_n B_{\nu n}\,\rho\,B_{\nu n}^\dagger\Big),$$

so all of Alice's operators disappear from Bob's statistics.

Milestones (Sec. II.D-II.E)

1. Eq. (7): $\sum_m \operatorname{tr}(A_{\mu m}\rho A_{\mu m}^\dagger) = \operatorname{tr}(\rho E_\mu)$.
2. Eq. (8): every $E_\mu$ is positive semidefinite.
3. Eqs. (7)-(8): for a density matrix and a complete POVM, the $p_\mu$ are nonnegative reals summing to $1$.
4. Eq. (6) defines a completely positive map.
5. Eq. (6) is the most general completely positive linear map: every completely positive linear map between matrix algebras has a finite Kraus representation.
6. Time reversal (transposition, i.e. complex conjugation of a Hermitian $\rho$) is a positive map,
7. but it is not completely positive.
8. The exchange step of Sec. II.E: under the commutation hypothesis, $\operatorname{tr}\sum_{m,n} B_{\nu n}A_{\mu m}\rho A_{\mu m}^\dagger B_{\nu n}^\dagger = \operatorname{tr}\big(E_\mu \sum_n B_{\nu n}\rho B_{\nu n}^\dagger\big)$.

Significance

The no-communication theorem is the consistency check between quantum measurement theory and relativistic causality, and it is the starting point of the relativistic measurement theory developed in Sec. III of the review. The commutation condition (9) is exactly what local quantum field theory provides for spacelike separated regions, so this algebraic form is the one later used for microcausality arguments. The Kraus representation (milestones 4-5) is a basic structural theorem of quantum information theory, and the failure of complete positivity for transposition (milestones 6-7) underlies the partial-transpose entanglement criterion.

The results are classical and their proofs are known; the mission produces machine-checked versions on top of Mathlib's matrix library. The finite Kraus representation theorem (milestone 5) requires Choi-matrix machinery that is not, to the knowledge of this proposal, available in Mathlib in this form; it is reusable well beyond this mission.

Difficulty

The goal and milestones 1-3 and 8 are finite-dimensional trace manipulations; the care needed is in keeping the order of products right, using the adjoint of the commutation relation, and summing over indices in the correct order. Milestone 7 needs an explicit entangled witness on $\mathbb C^2\otimes\mathbb C^n$. Milestone 5 is the substantial one: the obvious approach of writing $T(\rho)$ in a basis does not produce Kraus operators directly; a positivity argument (via the Choi matrix of $T$ and its spectral decomposition) is needed.

Formalization scope

All Hilbert spaces are finite dimensional: matrices are indexed by arbitrary finite types with complex entries. Outcome sets and discarded-subsystem label sets are finite types; Alice's and Bob's label sets may depend on the outcome. Kraus matrices for the single-intervention milestones may be rectangular ($e\times d$), reflecting that the system after the intervention may differ from the original one; in the no-communication theorem both observers' matrices are square on a common space. The order on $\mathbb C$ used for "nonnegative probability" is the standard partial order ($z\ge 0$ iff $z$ is real and nonnegative). Complete positivity quantifies over ancillas $\mathbb C^n$ for every $n\in\mathbb N$, with $T\otimes\mathbb 1$ acting blockwise. Time reversal is encoded by the linear map $\rho\mapsto\rho^{T}$; on Hermitian matrices this coincides with complex conjugation, and only the linear extension gives a meaningful complete-positivity statement.

The goal keeps the hypotheses of the source setting (both POVMs complete, $\rho$ a density matrix); none of them can be dropped silently by a degenerate encoding, and the conclusion is an identity of complex numbers, so no hypothesis is vacuous: for instance, single-outcome trivial interventions with $A = B = \mathbb 1$ satisfy all of them.

Note: the sentence on p. 100 of the source claiming that commuting POVM elements are necessarily orthogonal projections is not included; as stated it fails (e.g. $E_1 = E_2 = \tfrac12\mathbb 1$).

Selected references

• A. Peres and D. R. Terno, Quantum information and relativity theory, Rev. Mod. Phys. 76, 93-123 (2004). https://doi.org/10.1103/RevModPhys.76.93
• K. Kraus, States, Effects, and Operations, Lecture Notes in Physics 190, Springer (1983). https://doi.org/10.1007/3-540-12732-1
• M.-D. Choi, Completely positive linear maps on complex matrices, Linear Algebra Appl. 10, 285-290 (1975). https://doi.org/10.1016/0024-3795(75)90075-0

Motivation

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

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

Setting

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

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

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

$$\frac{1}{p-1}\sum_{a=0}^{p-2}\sum_{b=0}^{p-2}|a,b,g^ax^{-b}\ (\mathrm{mod}\ p)\rangle \qquad (6.1)$$

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

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

$$T=rc+d-\frac{r}{p-1}\{c(p-1)\}_q .$$

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

$$|\{T\}_q|\le\tfrac12 \quad (6.10) \qquad\text{and}\qquad |\{c(p-1)\}_q|\le q/12 \quad (6.11).$$

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

Formalization targets

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

$$\sum_{\substack{0\le c,d<q\\ (c,d)\ \text{good}}}\ \sum_{y\in(\mathbb Z/p)^\times}\Pr[c,d,y]\ \ge\ \frac1{480}.$$

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

Milestones

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

$$\Pr[c,d,g^k]=\left|\frac{1}{(p-1)q}\sum_{\substack{0\le a,b\le p-2\\ a-rb\equiv k\ (p-1)}}\exp\Bigl(\frac{2\pi i}{q}(ac+bd)\Bigr)\right|^2 .$$

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

Setting

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

$$a = \sum_{j=0}^{l-1} 2^j a_j, \qquad 0 \le a < q = 2^l .$$

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

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

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

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

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

$$R_{l-1}\, S_{l-2,l-1}\, R_{l-2}\, S_{l-3,l-1}\, S_{l-3,l-2}\, R_{l-3} \cdots R_1\, S_{0,l-1}\, S_{0,l-2} \cdots S_{0,2}\, S_{0,1}\, R_0 ,$$

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

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

Formalization targets

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

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

$$\text{circuit}\,|a\rangle = \frac{1}{q^{1/2}}\sum_{b}\exp(2\pi i\,ac/q)\,|b\rangle, \qquad c = \text{bit reversal of } b .$$

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

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

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

$$2^{-l/2}\exp\Big(i\Big(\sum_{0\le j<l}\pi a_jb_j + \sum_{0\le j<k<l}\frac{\pi}{2^{k-j}}a_jb_k\Big)\Big).$$

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

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

$$\exp\Big(i\Big(\sum_{0\le j<l}\pi a_jb_j + \sum_{0\le j<k<l}\frac{\pi}{2^{k-j}}a_jb_k\Big)\Big) = \exp(2\pi i\,ac/q).$$

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

Neutrino oscillations are an interference phenomenon, so they are sensitive to any mechanism that degrades quantum coherence during propagation. The open quantum system description models such effects without specifying their microscopic origin: the neutrino is treated as a subsystem whose reduced density matrix evolves under a Markovian master equation. The dissertation of G. F. S. Alves (Instituto de Física, Universidade de São Paulo, 2020) develops this framework for two and three neutrino generations and uses public IceCube atmospheric data to constrain the new parameters. Its two-generation chapter derives closed-form oscillation probabilities under several choices of the dissipative term; this mission formalizes that chapter's mathematical content.

Setting

A density matrix is a positive semidefinite complex matrix of unit trace. For a two-level system (two neutrino mass eigenstates) the reduced state $\rho(t)\in\mathbb C^{2\times2}$ obeys the Lindblad equation with constant coefficients,

$$\dot\rho=-i[H,\rho]+D[\rho],\qquad D[\rho]=\tfrac12\sum_{i,j=1}^3 a_{ij}\bigl(2\sigma_i\rho\sigma_j-\{\sigma_j\sigma_i,\rho\}\bigr),$$

where $\sigma_1,\sigma_2,\sigma_3$ are the Pauli matrices and the $3\times3$ Kossakowski matrix $a=(a_{ij})$ is Hermitian positive semidefinite (the condition for complete positivity). In the mass basis the vacuum Hamiltonian is $H=\operatorname{diag}(0,\Delta m^2/2E)$, and the mixing matrix with Majorana phase $\alpha$ is

$$U=\begin{pmatrix}\cos\theta&e^{i\alpha}\sin\theta\\-e^{-i\alpha}\sin\theta&\cos\theta\end{pmatrix}.$$

The muon neutrino is produced in the state $\rho_\mu(0)=U^\dagger|\nu_1\rangle\langle\nu_1|U$, and the survival probability after a baseline $L$ is $P_{\nu_\mu\to\nu_\mu}=\operatorname{Tr}\{\rho(L)\rho_\mu(0)\}$. The linear entropy $S_l(\rho)=1-\operatorname{Tr}\rho^2$ and the von Neumann entropy $S(\rho)=-\operatorname{Tr}\rho\ln\rho$ measure the loss of purity.

Formalization targets

Goal: decoherent survival probability, eq. (3.24)

For the pure-decoherence Kossakowski matrix $a=\operatorname{diag}(0,0,\gamma)$, $\gamma\ge0$, every solution with $\rho(0)=\rho_\mu(0)$ satisfies, for all $L\ge0$,

$$P_{\nu_\mu\to\nu_\mu}=\frac14\Bigl(3+\cos4\theta+2e^{-2\gamma L}\cos\Bigl(\frac{\Delta m^2}{2E}L\Bigr)\sin^22\theta\Bigr).$$

Milestones

1. Range of the linear entropy, eq. (2.45), and of the von Neumann entropy, eqs. (2.40)–(2.41).
2. Non-negativity of the relative entropy, eq. (2.43).
3. Entropy increase whenever the maximally mixed state is a fixed point of $D$ (Appendix B.1, two-level case).
4. Pauli-basis form of the Dissipator, eq. (3.5).
5. Average-energy conservation holds iff $a=\operatorname{diag}(0,0,\gamma)$, eqs. (3.19)–(3.22).
6. The evolved state in case (1), eq. (3.23), and the population in case (4), eq. (3.26).

Significance

The goal is the formula used in the dissertation to show how decoherence damps oscillations: it reduces to the standard vacuum formula at $\gamma=0$, it tends to $\tfrac14(3+\cos4\theta)$ at large $L$ instead of oscillating, and it does not depend on $\alpha$. The milestones connect the formula to the structure of the Lindblad generator (energy conservation singles out this Dissipator) and to entropy growth. A formal development yields a checked two-level Lindblad toolkit (Pauli expansion of dissipators, explicit solutions, entropy bounds) reusable in other open-system missions. The results are proved informally in the source; none is known to be machine-checked.

Difficulty

The ODE part requires a uniqueness argument for a linear matrix ODE on $[0,\infty)$ given only one-sided derivatives at $t=0$, plus exact trigonometric bookkeeping. The entropy milestones need spectral calculus for Hermitian matrices (Klein's inequality, concavity of $-x\ln x$) and, for Appendix B.1, the monotonicity of relative entropy under completely positive trace-preserving maps together with complete positivity of Lindblad semigroups, neither of which is expected to be available off the shelf.

Formalization scope

Matrices are Matrix (Fin 2) (Fin 2) ℂ; the Kossakowski matrix is Matrix (Fin 3) (Fin 3) ℂ with indices $0,1,2$ for the thesis' $1,2,3$. Solutions are curves $\mathbb R\to\mathbb C^{2\times2}$ satisfying the Lindblad equation entrywise for $t\ge0$ (derivatives within $[0,\infty)$); the exponential $e^{\mathcal Lt}$ is not used. Entropies use the continuous functional calculus. Two printed formulas are corrected in the drafts: the sign of the $\rho_0\,\mathrm{Im}(a_{ij})$ terms in eq. (3.5), and the overall sign of the off-diagonal entries in eq. (3.23); both corrections are explained in the corresponding items. The two-generation cases (4) and (5) survival probabilities, eqs. (3.25) and (3.27), and the three-generation and IceCube analyses are out of scope.

Selected references

• G. F. S. Alves, Decoherence in Neutrino Oscillations in the IceCube Experiment, MSc dissertation, Instituto de Física, Universidade de São Paulo, 2020.
• G. Lindblad, On the generators of quantum dynamical semigroups, Commun. Math. Phys. 48 (1976) 119–130, https://doi.org/10.1007/BF01608499
• V. Gorini, A. Kossakowski, E. C. G. Sudarshan, Completely positive dynamical semigroups of N-level systems, J. Math. Phys. 17 (1976) 821–825, https://doi.org/10.1063/1.522979

Motivation

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

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

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

Setting

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

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

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

$$\mu\Big(\bigcap_{i \in S} F_i\Big) \le p^{|S|}.$$

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

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

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

$$E_0 = p, \qquad E_{h+1} = f\,E_h^{2},$$

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

Formalization targets

Goal — threshold theorem with polylogarithmic overhead

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

$$n\,E_h < q \qquad\text{and}\qquad K^{h} \;\le\; K^{2}\Big(\max\Big(1,\ \frac{\log(n/q)}{\log\big(1/(fp)\big)}\Big)\Big)^{\log_2 K}.$$

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

Supporting targets

The milestone list covers the closed form $E_h = f^{2^{h}-1} p^{2^{h}}$ of the concatenation recursion and its threshold form $E_h = (fp)^{2^{h}}/f$; convergence $E_h \to 0$ below threshold; the failure bounds $|\mathrm{locs}|\,p$ and $C\,|\mathrm{locs}|\,p$ for a network under the two error models; the criterion $2^{h} > \log(n/q)/\log(1/(fp))$ under which $n (fp)^{2^{h}} < q$; and the overhead estimate $K^{\lceil \log_2 L\rceil} \le K L^{\log_2 K}$.

Significance

The threshold theorem is the reason large-scale quantum computation is regarded as a physically meaningful goal rather than an idealization: it converts an engineering requirement that scales with the problem size into a fixed, size-independent accuracy target, and it fixes the currency — threshold value and overhead exponent — in which every later architecture is compared. The quasi-independent models matter separately: they show the conclusion does not depend on noise being stochastic, which is what rules out the objection that coherent over-rotations invalidate the stochastic analysis.

The paper's own argument is a physics-style derivation: a circuit-level construction, a combinatorial count of failure-inducing pairs of error locations, and a recursion. This mission formalizes the recursion, the probabilistic bounds and the resulting threshold and overhead statements. It does not formalize the circuit-level content — the $7$-qubit code, the cat-state syndrome extraction networks, transversality, or the count $f \le 337195$ itself; these enter the formal statements as the parameters $f$ and $K$. No machine-checked proof of the full threshold theorem, in the sense of a verified fault tolerant circuit construction, is known to the author of this proposal; formalizing the quantitative layer is a prerequisite for one.

Difficulty

The obvious route to "errors vanish under concatenation" is to iterate the bound $p \mapsto f p^{2}$ and observe the doubly exponential decay. That step is the easy half, and the milestone list makes it explicit. What the naive argument silently assumes is exactly what Section II must establish: that the level-$(h+1)$ failure events again obey a quasi-independent bound, with $k$ simultaneous encoded failures bounded by $(f p^{2})^{k}$ rather than merely each single failure bounded by $f p^{2}$. This is why the paper's failure declaration is defined backwards in time and demands disjoint pairs of contributing locations. A formalization that bounds only single-gate failure probabilities cannot close the induction.

The second difficulty is bookkeeping at the edges: the recursion is stated for a failure parameter that is a probability in one model and an operator strength in the other, and the overhead bound involves a real exponent $\log_2 K$ and a ceiling, whose interaction with the degenerate cases $p = 0$ and $n \le q$ has to be handled rather than assumed away.

Formalization scope

All parameters are real numbers: $f, p, q, K, C \in \mathbb{R}$, and the gate count $n$ is a natural number cast to $\mathbb{R}$. levelError is defined by recursion on the level and is total, so it is meaningful for every real $f, p$; the threshold hypothesis appears explicitly as $p < 1/f$ where it is needed.

The two error models are predicates on a measure $\mu$ on a measurable space, a Finset of error locations, and a family of failure events, with values in ENNReal; they quantify over all subsets $S$ of the location set, matching the paper's "at a given $k$ many error locations". The network failure bounds are stated for $\mu\big(\bigcup_{i} F_i\big)$, the probability that some location fails.

The goal is not vacuous: the hypotheses $f \ge 1$, $K \ge 2$, $0 \le p < 1/f$, $0 < q < n$ are simultaneously satisfiable (for instance $f = 1$, $K = 2$, $p = 10^{-6}$, $n = 10^{6}$, $q = 1/2$), and the conclusion asserts a strict inequality together with a quantitative overhead bound, so it cannot be discharged by a degenerate reading. Degenerate inputs are inside the statement rather than excluded: $p = 0$, and the case $\log(n/q)/\log(1/(fp)) \le 1$, are covered by the $\max$ and must be handled.

A complete development needs only Mathlib's real analysis (Real.log, Real.logb, Real.rpow, Nat.ceil) and the measure-theoretic union bound; nothing quantum is required by the formal statements. Contributions strengthening the milestone list towards the circuit level — a formal model of error locations in a network, of the induced next-level error model, or of stabilizer-code recovery — are welcome as further targets.

Selected references

• E. Knill, R. Laflamme, W. H. Zurek, Resilient Quantum Computation: Error Models and Thresholds, arXiv:quant-ph/9702058 (1997), https://arxiv.org/abs/quant-ph/9702058
• A. M. Steane, Error Correcting Codes in Quantum Theory, Physical Review Letters 77, 793 (1996), https://doi.org/10.1103/PhysRevLett.77.793
• P. W. Shor, Fault-tolerant quantum computation, Proceedings of the 37th Symposium on Foundations of Computer Science (1996), https://arxiv.org/abs/quant-ph/9605011
• D. Aharonov, M. Ben-Or, Fault-Tolerant Quantum Computation With Constant Error, arXiv:quant-ph/9611025 (1996), https://arxiv.org/abs/quant-ph/9611025
• A. Yu. Kitaev, Quantum computations: algorithms and error correction, Russian Mathematical Surveys 52, 1191 (1997), https://doi.org/10.1070/RM1997v052n06ABEH002155

Motivation

Quantum computations are performed on physical devices whose elementary operations are never exact: every gate, every idle qubit, every time step is subject to decoherence, damping and systematic inaccuracy. Without protection these errors accumulate and destroy the computation. In 1997 Dorit Aharonov and Michael Ben-Or proved that this can be overcome: as long as the error rate — the probability, per location per time step, that a fault occurs — is below a fixed positive threshold, an arbitrary quantum circuit can be simulated reliably with only polylogarithmic overhead (arXiv:quant-ph/9906129). This threshold theorem is the reason large-scale quantum computing is regarded as physically possible in principle, and the number it produces is the target every hardware programme is measured against.

The engine of the proof is not quantum mechanical but combinatorial. A circuit is encoded, then the encoded circuit is encoded again, $r$ times over. The locations of the resulting circuit are organised into a tree of nested rectangles, and the computation survives precisely when the set of faulty locations is sparse in a recursive sense. The mission formalizes that engine: the recursive sparseness calculus of §7.4–7.6 and §8.2 of the paper, which converts a constant error rate below the threshold into a doubly exponentially small failure probability.

Setting

Fix two natural numbers: $A$, the number of locations in a rectangle, and $k$, the number of faulty sub-rectangles a rectangle tolerates (in the paper $k=\lfloor d/l\rfloor$, where $d$ is the number of errors the code corrects and $l$ is the spread of a fault). A $0$-rectangle is a single location of the circuit, and an $(r+1)$-rectangle consists of $A$ many $r$-rectangles. A fault pattern of an $r$-rectangle records, for each of its $A^{r}$ locations, whether a fault occurred there.

Following Definition 18 of the paper, a fault pattern is $(r,k)$-sparse by recursion on $r$: at level $0$ it is sparse when the location carries no fault; at level $r+1$ it is sparse when at most $k$ of the $A$ constituent $r$-rectangles carry a pattern that is not $(r,k)$-sparse. Under independent probabilistic noise of rate $\eta$ each location is faulty with probability $\eta$, independently; write $P(r)$ for the probability that the pattern of an $r$-rectangle is $(r,k)$-sparse, and $1-P(r)$ for the probability that it is not.

Two thresholds appear. The threshold condition for probabilistic noise (Definition 19) is

$$\binom{A}{k+1}\,\eta^{k+1} < \eta ,$$

and the threshold condition for general noise (Definition 21) is

$$e\binom{A}{k+1}(2\eta)^{k+1} < 2\eta .$$

The corresponding thresholds are $\eta_c=\binom{A}{k+1}^{-1/k}$ and $\eta_c'=\tfrac12\bigl(e\binom{A}{k+1}\bigr)^{-1/k}$: every positive $\eta$ below them satisfies the respective condition.

Target

The goal is the quantitative core of Theorem 10. Below the threshold there are constants $C,c>0$ such that for every circuit size $v\ge 1$ and every accuracy $0<\varepsilon<1$ some recursion depth $r$ satisfies both

$$v\cdot\bigl(1-P(r)\bigr) < \varepsilon \qquad\text{and}\qquad A^{r} \le C\Bigl(1+\log\frac{v}{\varepsilon}\Bigr)^{c}.$$

The first inequality says that, over all $v$ rectangles of the simulated circuit, the probability that any of them carries a non-sparse fault pattern is below $\varepsilon$; the second says that the overhead per simulated location, $A^{r}$, is polylogarithmic in $v/\varepsilon$ — the cost claimed in Theorem 10.

The milestones build up to it: the two threshold conditions hold below the respective thresholds, the exponent gap $\delta$ of equation 7.5 exists, the base case $P(0)=1-\eta$, the union-bound recursion $1-P(r+1)\le\binom{A}{k+1}(1-P(r))^{k+1}$, Lemma 10 itself ($P(r)\ge 1-\eta^{(1+\delta)^r}$), and the analogous recursion 8.8–8.10 governing the bad part in the general-noise analysis.

Significance

Lemma 10 is where a constant error rate becomes a vanishing one. Each level of concatenation only has to improve reliability slightly, because the improvement compounds doubly exponentially in the number of levels; this is exactly why constant-rate noise can be tolerated while Shor's earlier scheme needed a polylogarithmically small rate. The same recursion, with $2\eta$ in place of $\eta$ and an extra factor of $e$, controls the trace norm of the bad part of the fault-path expansion in the general-noise model (§8.2), which is how the result is extended from probabilistic errors to decoherence, damping and systematic inaccuracy.

Formalizing this part of the paper yields a reusable, model-independent statement: nothing in the milestones mentions density matrices, so the sparseness calculus can later be plugged into a formal model of noisy quantum circuits, or reused for classical concatenated fault tolerance. What this mission does not do is formalize the circuit-level statement of Theorem 10 — that requires a full Lean model of quantum circuits with mixed states, fault-tolerant procedures, and the code constructions of §3–§6, and is deliberately out of scope here.

Difficulty

The obvious approach — bound the failure probability by a union bound over all fault sets of size $k+1$ and iterate — is exactly right, but the iteration is where the work is. The recursion $q_{r+1}\le\binom{A}{k+1}q_r^{k+1}$ only produces the doubly exponential decay $\eta^{(1+\delta)^r}$ once the threshold condition is converted into the strict exponent gap $\delta$ of equation 7.5, and the induction has to keep $q_r\le\eta$ alive to reuse that gap at every level. In the general-noise recursion there is a second trap: the factor $(1+b_r)^{A-k-1}$ exceeds $1$, so the recursion is not contracting termwise, and one needs $2\eta A\le 1$ to bound it by $e$.

On the probabilistic side, the statements are about a genuine product distribution on an exponentially large sample space, not a recursively defined real number: the union-bound step must be carried out over the actual set of fault patterns, where independence across the $A$ sub-rectangles is what makes the product bound valid.

Formalization scope

Fault patterns are a type defined by recursion on the level: $\mathrm{FaultPattern}(A,0)$ is the booleans and $\mathrm{FaultPattern}(A,r+1)$ is the functions from the $A$ sub-rectangles to $\mathrm{FaultPattern}(A,r)$; every level is a finite type with decidable equality. Sparseness is a decidable predicate following Definition 18 verbatim. The noise distribution is given by the weight of a pattern, the product over all locations of $\eta$ (faulty) or $1-\eta$ (clean), and the sparseness probability is the sum of these weights over the sparse patterns — an honest finite product measure, so no hypothesis $0\le\eta\le1$ is built into the definitions and each statement carries the range hypotheses it needs.

Two conventions are worth flagging. First, the thresholds are formalized as $\binom{A}{k+1}^{-1/k}$ and $\tfrac12(e\binom{A}{k+1})^{-1/k}$; the paper prints the exponent as $-k$ in equations 7.4 and 8.6, which is inconsistent with its own threshold conditions 7.3 and 8.5, and $-1/k$ is the exponent for which the paper's claim "any $\eta<\eta_c$ satisfies the threshold condition" is true. Second, Lemma 10 is stated with $\ge$ rather than the paper's strict $>$, because at $r=0$ the two sides are equal.

Nothing here is vacuous: all hypotheses are satisfiable — for instance $A=7$, $k=1$, $\eta=10^{-3}$ satisfies every hypothesis of the goal — and the goal quantifies over all circuit sizes and all accuracies, so it cannot be discharged by a degenerate choice. A complete development needs only real analysis, finite sums and binomial counting from Mathlib. Contributions that generalise the branching factor to a per-rectangle bound $A_i\le A$, or that connect the calculus to a formal model of noisy circuits, are welcome.

Selected references

• Dorit Aharonov and Michael Ben-Or, Fault-Tolerant Quantum Computation With Constant Error Rate, arXiv:quant-ph/9906129 (1999); preliminary version in Proc. 29th ACM STOC (1997). https://arxiv.org/abs/quant-ph/9906129
• Peter W. Shor, Fault-tolerant quantum computation, Proc. 37th FOCS (1996). https://arxiv.org/abs/quant-ph/9605011
• Dorit Aharonov, Alexei Kitaev and Noam Nisan, Quantum circuits with mixed states, Proc. 30th ACM STOC (1998). https://arxiv.org/abs/quant-ph/9806029