Motivation

A qubit coupled to an environment loses the phase relation between its basis states $|0\rangle$ and $|1\rangle$: the off-diagonal entries of its density matrix decay. This decoherence is the main obstacle to storing quantum information, and a large body of work tries to counter it with external control fields. Lidar and Schneider (arXiv:quant-ph/0410048, Quantum Information and Computation 2005) ask a sharp question in the simplest nontrivial setting: if the controller may observe the state and choose the Hamiltonian at every instant (tracking control), can it keep the coherence of a dephasing qubit exactly constant, and for how long?

Their answer, stated in the abstract, is that "it is possible to maintain coherence for finite time durations, until the control field diverges." It was known that Hamiltonian control cannot hold the purity $\operatorname{Tr}\rho^2$ of a Markovian open system at its initial value (Ketterle and Pritchard, Phys. Rev. A 46, 4051 (1992), and Tannor and Bartana, J. Phys. Chem. A 103, 10359 (1999), refs. [25, 26] of the paper), and the paper's §II.A shows that under a unital Lindbladian the purity decreases whatever the Hamiltonian; the present result locates exactly how much of the coherence, as opposed to the purity, control can protect.

Setting

A qubit state is a complex $2\times2$ matrix $\rho$ with $\operatorname{Tr}\rho=1$, $\rho_{10}=\rho_{01}^*$ and $\operatorname{Tr}(\rho^2)\le1$. With the Pauli matrices $\sigma_x,\sigma_y,\sigma_z$, its Bloch vector is $\vec v=(v_x,v_y,v_z)$, $v_\alpha=\operatorname{Tr}(\rho\sigma_\alpha)$, so that $\rho=\tfrac12(I+\vec v\cdot\vec\sigma)$ (eq. (9)). The coherence is the squared radius of $\vec v$ in the $x$–$y$ plane,

$$c=v_x^2+v_y^2=4|\rho_{01}|^2 \quad\text{(eq. (11))}.$$

The controller applies the Hamiltonian $H(t)=\tfrac{\hbar}{2}\bigl(\omega_0(t)\sigma_z+\omega_1(t)\sigma_x-\omega_2(t)\sigma_y\bigr)$ (eq. (13)) with three real fields $\omega_0,\omega_1,\omega_2$, and the qubit undergoes pure dephasing at rate $\gamma>0$:

$$\frac{\partial\rho}{\partial t}=-\frac{i}{\hbar}[H,\rho]+\frac{\gamma}{2}(\sigma_z\rho\sigma_z-\rho)\quad\text{(eq. (32))}.$$

Equivalently the Bloch vector obeys $\dot{\vec v}=M(t)\vec v$ with

$$M(t)=\begin{pmatrix}-\gamma&-\omega_0&-\omega_2\\ \omega_0&-\gamma&-\omega_1\\ \omega_2&\omega_1&0\end{pmatrix}\quad\text{(eq. (30))}.$$

Without control the coherence decays as $e^{-2\gamma t}c$. The breakdown time of an initial state with coherence $c>0$ is

$$t_b=\frac{v_z(0)^2}{2\gamma c}\quad\text{(eq. (38))}.$$

The tracking fields are, with $s=\operatorname{sign}v_z(0)$, an arbitrary $\omega_0$, and $R(t)=v_z(0)^2-2\gamma ct$,

$$\omega_2(t)=s\,\frac{-\gamma v_x(0)-\omega_0(t)v_y(0)}{\sqrt{R(t)}},\qquad \omega_1(t)=s\,\frac{-\gamma v_y(0)+\omega_0(t)v_x(0)}{\sqrt{R(t)}}\quad\text{(eqs. (41)–(42))},$$

and the tracked state is $\tfrac12(I+\vec v(t)\cdot\vec\sigma)$ with $\vec v(t)=(v_x(0),v_y(0),s\sqrt{R(t)})$.

Formalization targets

Goal: coherence can be held exactly on $[0,t_b)$, and no longer

For $\hbar>0$, $\gamma>0$ and a qubit state $\rho_0$ with coherence $c>0$:

1. No-go. For all controls and every solution $\rho(t)$ of (32) on $[0,T)$ with $\rho(0)=\rho_0$ and constant coherence $c$,

$$v_z(t)^2=v_z(0)^2-2\gamma c\,t\quad(t\in[0,T)),\qquad T\le t_b .$$

2. Achievability. If $v_z(0)\ne0$, then for every $\omega_0$ the tracked state starts at $\rho_0$, is a qubit state, keeps $v_x,v_y$ fixed, and solves (32) at every $t\in[0,t_b)$ with the tracking fields.
3. Divergence. If $v_z(0)\ne0$, then $\omega_1(t)^2+\omega_2(t)^2\to+\infty$ as $t\to t_b^-$, whatever $\omega_0$ is.

Milestones

The milestones follow the paper's derivation: the Bloch parametrization (§II.B, p. 3); the equivalence of (32) and (30) (§III.B, p. 5); eq. (36), $\dot v_z=-\gamma c/v_z$ under constant coherence (p. 6); eqs. (37)–(38), $v_z(t)=(\pm)\sqrt{v_z(0)^2-2\gamma ct}$ and $T\le t_b$ (p. 6); eqs. (41)–(42), the tracking fields solve (30) and are forced once $v_x,v_y$ are frozen (p. 6); and the field-strength identity of §III.C (p. 8),

$$\omega_1(t)^2+\omega_2(t)^2=\frac{(\gamma^2+\omega_0(t)^2)\,c}{v_z(0)^2-2\gamma ct}.$$

Significance

The result gives an exact, state-dependent budget for coherence protection under dephasing. The time $t_b$ is inversely proportional to the coherence to be maintained and proportional to $v_z(0)^2=p(0)-c$, where $p=|\vec v|^2$ is the purity: the more coherent the initial state, the shorter the protection, and a state of maximal coherence for its purity ($v_z(0)=0$) cannot be protected at all. The no-go part holds for every control law, so it bounds any tracking strategy, not only the linearized one the paper constructs. The divergence of the fields is the physical cost: protection up to $t_b$ requires unbounded control amplitude, which any bounded actuator cuts short.

The paper proves these statements by direct calculation. As far as is known, none of them has a machine-checked proof. The mission turns a physics derivation, in which "the solution is" and "does not stay real" carry the logical weight, into precise statements about solutions of an ODE on a half-open interval, with the sign choice, the degenerate case $v_z(0)=0$ and the domain of the square roots made explicit.

Difficulty

The calculations are elementary, but the no-go statement quantifies over arbitrary, possibly discontinuous control fields and arbitrary solutions of the matrix equation. Nothing is assumed about the controls beyond being real functions of time, nothing about the solution beyond continuity on $[0,T)$ and the equation on $(0,T)$, and the conclusion constrains only the $z$-component while the hypothesis constrains only the $x$–$y$ components. The tempting shortcut, assuming that $v_x$ and $v_y$ are frozen as in the paper's explicit construction, proves a strictly weaker statement and is not the goal. On the achievability side, the square root is not differentiable where its argument vanishes, so differentiability has to be established on $[0,t_b)$, including the endpoint $t=0$, and the sign $\operatorname{sign}v_z(0)$ has to be carried through the derivative.

Formalization scope

Operators are Matrix (Fin 2) (Fin 2) ℂ in the basis $|0\rangle,|1\rangle$; the Pauli matrices are the published MIPRE.LCS.Pauli.X/Y/Z. Bloch vectors and controls are Fin 3 → ℝ: Bloch components in the order $x,y,z$, control components in the order $\omega_0,\omega_1,\omega_2$ (with $\omega_0$ multiplying $\sigma_z$, as in (13)). The Bloch vector is $v_\alpha=\operatorname{Re}\operatorname{Tr}(\rho\sigma_\alpha)$, following eq. (9); eq. (8) prints an extra factor $\tfrac12$, which contradicts (9) and is treated as a misprint. A trajectory solves (32) or (30) on $[0,T)$ if it is continuous on $[0,T)$ and has the prescribed derivative at every $t\in(0,T)$. Controls are arbitrary functions $\mathbb R\to\mathbb R$. The hypotheses $\gamma>0$ and $c>0$ are added, because $t_b$ divides by $2\gamma c$; $\hbar>0$ is a parameter. The sign $(\pm)$ of (37), (41), (42) is $\operatorname{sign}v_z(0)$.

Statements about $t_b$, the tracked state and the fields are restricted to $[0,t_b)$, because Lean's square root and division are total ($\sqrt{x}=0$ for $x<0$, $x/0=0$); a statement that only asserts that the closed-form curve solves the ODE would be the achievability half alone, and the goal requires the no-go half over all controls as well.

A complete development needs the Bloch dictionary for $2\times2$ matrices, the passage from (32) to (30), and one-variable real analysis on half-open intervals. The Bloch dictionary and the reduction of a Lindblad equation to Bloch form are reusable for other qubit control problems. Proofs of any milestone, and sorry-free lemmas on the Pauli algebra, are welcome.

Selected references

• D. A. Lidar and S. Schneider, Stabilizing qubit coherence via tracking-control, Quantum Information and Computation (2005); arXiv:quant-ph/0410048v1, 2004. https://arxiv.org/abs/quant-ph/0410048
• W. Ketterle and D. E. Pritchard, Atom cooling by time-dependent potentials, Physical Review A 46, 4051 (1992). https://doi.org/10.1103/PhysRevA.46.4051

Motivation

The cyclotomic Birman–Wenzl–Murakami algebra is an algebra of braids and contractions equipped with an additional cyclotomic relation. It connects diagram algebras, representation theory, and knot theoretic constructions. For calculations over a coefficient ring, one needs to know whether the diagrammatic spanning elements remain independent after parameters are specialized. The freeness theorem of Goodman and Hauschild Mosley answers that question for admissible integral ground rings: the algebra has a basis of the size predicted by labeled Brauer diagrams. The paper also identifies the algebra with a cyclotomic Kauffman tangle algebra. This mission targets the algebra's freeness and rank assertion.

The cited paper builds on admissibility relations developed with Wilcox and Yu. Its earlier definitions and preliminary statements already appear in Prove2Me mission 92e1197e-907f-4ab8-92be-01ea44f6cfef. The present mission reuses that published layer and poses the deferred freeness theorem and the intermediate results that support it. The distinction matters because two algebras with similar names but different generators or parameter conventions need not have the same rank statement.

Setting

A ground ring $S$ is a commutative unital ring with a positive integer $r$ and parameters $\rho,q,\delta_0,\delta_1,\ldots,u_1,\ldots,u_r$. The parameters $\rho,q,\delta_0,u_1,\ldots,u_r$ are units, and they satisfy

$$\rho^{-1}-\rho=(q^{-1}-q)(\delta_0-1).$$

The algebra $W_{n,S,r}$ is generated over $S$ by invertible braids $g_i$, contractions $e_i$, and an invertible affine generator $y_1$. It obeys the affine BMW relations of Definition 2.1 and the cyclotomic relation $\prod_{j=1}^r(y_1-u_j)=0$ of Definition 2.8. The shared published presentation uses indices $i=0,\ldots,n-2$ for $g_i$ and $e_i$, corresponding to the paper's $g_{i+1}$ and $e_{i+1}$. At $n=0$ there are no generators.

The parameters are admissible when $q-q^{-1}$ is nonzero and not a zero divisor, weak admissibility holds for every integer shift of the $\delta$ relations, and $e_1,y_1e_1,\ldots,y_1^{r-1}e_1$ are $S$-linearly independent in $W_{2,S,r}$. These are the conditions of Definition 3.3, expressed using condition (1) of Theorem 3.2. A morphism of ground rings preserves all $\delta_j$ and $u_i$ and permits exactly the four paired sign actions on $\rho$ and $q$ in Definition 2.13. Consequently, base change includes the sign twists allowed by the paper.

For the generic case, $F=\mathbb Q(q,u_1,\ldots,u_r)$ is the rational function field in algebraically independent variables. Put $p=\prod_j u_j$, set $\rho=p$ for odd $r$ and $\rho=q^{-1}p$ for even $r$, and define $\delta_a=\sum_j\gamma_j u_j^a$, where $\gamma_j$ is the rational expression in equation (3.6). A shape in $\Gamma_n$ is an $r$-tuple of Young diagrams whose total number of boxes is at most $n$ and congruent to $n$ modulo two. An up–down tableau of shape $\lambda$ is a path from the empty tuple to $\lambda$, adding or removing one box at each step. Its set is $T(n,\lambda)$.

Formalization targets

The central target is the freeness half of Theorem 6.1. For every admissible integral ground ring $S$ and every $n\ge0$,

$$W_{n,S,r}\cong_S S^{\,r^n(2n-1)!!}.$$

Here $(-1)!!=1$, so the asserted rank at $n=0$ is one. A basis indexed by a finite type of that cardinality states both freeness and rank.

The milestone path includes the paper's admissibility equivalences, generic parameter construction, universal admissible integral domain, base change, the spanning family of $r^n(2n-1)!!$ elements, the relevant Jones ideal and Hecke quotient results, and the generic structure results. At the generic field, Theorem 4.8 supplies split matrix blocks indexed by $\Gamma_n$, with block size $|T(n,\lambda)|$. The count in the proof of Theorem 5.2 is

$$\sum_{\lambda\in\Gamma_n}|T(n,\lambda)|^2=r^n(2n-1)!!,$$

which agrees with the generic dimension asserted by Theorem 5.2. The final theorem applies over an admissible integral domain, rather than only over $F$.

Significance

The result supplies an exact finite basis for $W_{n,S,r}$ throughout the admissible integral-domain regime. It fixes the module rank independently of a choice of specialization and gives a numerical benchmark for presentations and representations of these algebras. The generic matrix decomposition also records the simple-block labels and their sizes; the tableau identity explains how those dimensions total the same rank.

Goodman and Hauschild Mosley proved these results. This mission asks for machine-checked proofs of the statements already known in the paper. Its reusable output includes ground-ring morphisms with sign twists, the generic parameter model, and finite tableau types. The published preliminary layer in mission 92e1197e-907f-4ab8-92be-01ea44f6cfef contains two proved and four open results among the six referenced milestones; none of the eight new theorem statements is presented here as already machine proved.

Difficulty

A spanning family alone does not show a basis: specializations can introduce linear dependence, and an equality of dimensions over one field does not itself establish independence over every integral ground ring. The argument also has to maintain the exact admissibility conditions when moving between coefficient rings. Over the generic field, identifying the right semisimple blocks requires the branching shapes and tableau sizes, while the final statement concerns arbitrary admissible integral domains. These are distinct algebraic regimes, and the same presentation and parameter conventions must be kept through each one.

Formalization scope

Lean uses the published GroundParameters, BMW, BMWAdmissible, UAdmissible, and equation (3.6) gamma expression from QAlgorithms.Papers.Independent.Support21.P14. The algebra is the quotient of a free algebra by the source's relations, with zero-based generator indices. The new definition layer records all four sign cases of Definition 2.13, the generic field as a fraction ring of a multivariate polynomial ring over $\mathbb Q$, and shapes and tableaux as finite-indexed Young diagrams. A generic ground-parameter value is asserted to exist as a theorem because the required unit and compatibility proofs are substantive.

The universal-ring milestone states all five parts of Theorem 3.19 for $\overline R_0$ and $\overline R_+$; part (5) is read inside $F$, where the universal $u$-admissible ring is the subring generated by $q^{\pm1}$, $(q^{-1}-q)^{-1}$, $\delta_0^{-1}$ and $u_i^{\pm1}$. The base-change statement uses $S'\otimes_S W$ for the source's $W\otimes_S S'$. Theorem 4.8 is expressed as a product of full matrix algebras with tableau-sized blocks, combining its split and labeling clauses with the block dimensions stated elsewhere in §4. Theorem 6.1's Kauffman-tangle isomorphism is not posed because a corresponding tangle algebra has not been provided here. The cited spanning set is expressed as an indexed family, which remains meaningful when a degenerate coefficient ring identifies elements.

The goal requires an actual basis of cardinality $r^n(2n-1)!!$ over an admissible integral domain. A mere dimension equality or spanning claim does not satisfy it. Contributions toward the missing generic decomposition, tableau count, base-change isomorphism, and passage to arbitrary admissible domains are all within scope. The ground-parameter and quotient-presentation definitions are reusable independently of this mission.

Selected references

• F. M. Goodman and H. Hauschild Mosley, Cyclotomic Birman–Wenzl–Murakami algebras, II: Admissibility Relations and Freeness, 2008, arXiv:math/0612065v5.

Motivation

Photosynthetic light-harvesting complexes move an electronic excitation from the pigment that absorbed a photon to a reaction centre, where its energy is stored chemically. In the Fenna–Matthews–Olson (FMO) complex this transfer is close to lossless, and two-dimensional spectroscopy showed long-lived quantum coherence during it (Engel et al. 2007). This raised a concrete question in open-system quantum dynamics: does the environment, whose noise destroys coherence, hinder transport, or can it help?

Numerical studies of FMO models found that local dephasing raises transfer efficiency compared with purely coherent evolution (Mohseni et al. 2008; Plenio and Huelga 2008; Rebentrost et al. 2009). Caruso, Chin, Datta, Huelga and Plenio (arXiv:0901.4454, J. Chem. Phys. 2009) isolated a mechanism behind this in a model that can be solved exactly: the fully connected network (FCN). There, coherent evolution traps most of the excitation by destructive interference, and any amount of uniform dephasing removes the trap. This mission formalizes that exact result.

Setting

The network has $N$ sites. The single-excitation space has orthonormal basis $|0\rangle, |1\rangle, \dots, |N\rangle, |N+1\rangle$: $|0\rangle$ is the zero-exciton state (population lost to the environment), $|j\rangle$ for $1 \le j \le N$ is one excitation on site $j$, and $|N+1\rangle$ is the sink (the reaction centre). The operators $\sigma_j^+ = |j\rangle\langle 0|$ and $\sigma_j^- = |0\rangle\langle j|$ create and destroy the excitation on site $j$.

The FCN Hamiltonian $H$ (with $\hbar = 1$) has $\langle j|H|j\rangle = \omega_j$, the site energies, and $\langle i|H|j\rangle = J$ for every pair of distinct sites, and vanishes on $|0\rangle$ and $|N+1\rangle$. For a real rate $r$ and an operator $c$ write

$$\mathcal D_{r,c}(\rho) = r\,\bigl[2c\rho c^\dagger - \{c^\dagger c, \rho\}\bigr].$$

The state $\rho(t)$, a complex $(N+2)\times(N+2)$ matrix, obeys the Lindblad master equation $\dot\rho = \mathcal L(\rho)$ with

$$\mathcal L(\rho) = -i[H,\rho] + \sum_{j=1}^N \mathcal D_{\Gamma_j,\,\sigma_j^-}(\rho) + \sum_{j=1}^N \mathcal D_{\gamma_j,\,|j\rangle\langle j|}(\rho) + \mathcal D_{\Gamma_{N+1},\,|N+1\rangle\langle k|}(\rho).$$

The terms are coherent hopping, dissipation to the environment at rates $\Gamma_j$, pure dephasing at rates $\gamma_j$, and irreversible decay into the sink from a chosen site $k$ at rate $\Gamma_{N+1}$. So $\rho(t) = e^{t\mathcal L}\rho(0)$. The initial state is $\rho(0) = |1\rangle\langle 1|$, and transport is measured by the sink population

$$p_{\rm sink}(t) = 2\Gamma_{N+1}\int_0^t \rho_{kk}(t')\,dt'.$$

The goal concerns the FCN of §II.A: $\omega_j = 0$, $\Gamma_j = 0$, the sink attached at $k = N$, and a uniform dephasing rate $\gamma_j = \gamma \ge 0$.

Formalization targets

Goal: noise-free and dephased limits

For $N \ge 2$, $J \ne 0$ and $\Gamma_{N+1} > 0$:

$$\gamma = 0:\quad \lim_{t\to\infty} p_{\rm sink}(t) = \frac{1}{N-1}, \qquad\qquad \gamma > 0:\quad \lim_{t\to\infty} p_{\rm sink}(t) = 1.$$

The first limit is Eq. (5) of the paper. The second is the claim of §II.C, confirmed for uniform dephasing in Appendix A.3, Eq. (A30). The coupling $J$, the sink rate and the dephasing rate are left free; neither limit depends on them.

Milestones

1. (A7) Population sum rule: $1 = \sum_{j=1}^N \rho_{jj}(t) + \rho_{00}(t) + p_{\rm sink}(t)$ for all $t$.
2. §II.A spectrum. $|\phi\rangle = N^{-1/2}\sum_j |j\rangle$ has energy $J(N-1)$. The states $|\psi_j\rangle = |1\rangle - |j\rangle$, $j = 2,\dots,N$, have energy $-J$, and together with $|\phi\rangle$ they span the site space.
3. Eq. (8). $|1\rangle = \frac{1}{N-1}\bigl[\sum_{j=2}^{N-1}|\psi_j\rangle + \sqrt N|\phi\rangle - |N\rangle\bigr]$.
4. Invariant states. In the noiseless FCN, an eigenstate of $H$ with no overlap with site $N$ does not evolve, and $p_{\rm sink} \equiv 0$.
5. Eqs. (6)–(7). For $N \ge 3$, $\rho(t) \to \frac{N-2}{N-1}|\Psi\rangle\langle\Psi| + \frac1{N-1}|N+1\rangle\langle N+1|$.
6. (A14). The closed form of $\rho_{NN}(t)$ for the noiseless FCN, $N \ge 3$.
7. Appendix A.1. The closed linear system of six equations for $\Lambda = \sum_{i,j}\rho_{ij}$, $X + iY = \sum_j \rho_{Nj}$, $\rho_{NN}$, $\rho_{00}$ and $p_{\rm sink}$ under uniform $\omega$, $\Gamma$, $\gamma$.

Significance

The result. The noise-free limit $1/(N-1)$ shows that a perfectly coherent, fully symmetric network is a poor transporter: for $N = 10$ only $1/9$ of the excitation reaches the sink, whereas a classical random walk on the same graph delivers all of it. The dephased limit $1$ shows that arbitrarily weak local noise restores complete transfer. Together they are the cleanest exactly solvable instance of dephasing-assisted transport. The invariant-subspace argument behind them (milestones 2–5) also predicts which states are protected from a sink, a mechanism related to coherent population trapping in quantum optics and condensed-matter systems.

Formalizing it. The paper derives these limits from Laplace-domain calculations and residue computations, some of them only sketched. A machine-checked proof would settle the exact constants, the hypotheses under which each limit holds (the necessity of $J \ne 0$ and $\Gamma_{N+1} > 0$, and the case $N = 2$), and the passage from the matrix exponential to the collective variables. As far as is known, none of these results has been formalized. The development also produces reusable pieces: the Lindblad generator of a single-excitation network with a sink, the trace identity (A7), and the spectrum of the complete-graph hopping Hamiltonian.

Difficulty

The obvious route is to compute $e^{t\mathcal L}$, but $\mathcal L$ acts on an $(N+2)^2$-dimensional space for arbitrary $N$, so no fixed-size computation applies. The noise-free limit hinges on an exact cancellation: $\frac{N-2}{N-1}$ of the weight lies in an $H$-eigenspace that is invisible to the sink, and the remainder must be shown to drain completely, which is a statement about the spectrum of a non-normal generator on the complementary subspace. Under dephasing that invariant subspace no longer exists, but the reduced six-variable system still has to be shown to have $p_{\rm sink} = 1$ as its only attracting steady state, for every $\gamma > 0$ and every $N$. In the paper this is done through a final-value theorem applied to a fifth-order characteristic polynomial (A26), which is misprinted. A proof that the limit exists, and not only what it equals, is part of the task.

Formalization scope

• Basis and operators. The basis is Fin (N + 2) in the paper's numbering (0 = zero-exciton state, 1…N = sites, N + 1 = sink), with natural-number indices cast into it. Operators are Matrix (Fin (N + 2)) (Fin (N + 2)) ℂ.
• Hopping and rates. The hopping is normalized as $\langle i|H|j\rangle = J$, which matches (A1), (A34) and the spectrum on p. 4. The rates multiply $2c\rho c^\dagger - \{c^\dagger c,\rho\}$ with no factor ½, as in Eqs. (2)–(4).
• Evolution. $\rho(t)$ is semigroupEvolution of the published definition P16, that is, NormedSpace.exp of $t\mathcal L$, applied to $|1\rangle\langle 1|$.
• Sink population. $p_{\rm sink}$ is the interval integral of the real part of $\rho_{kk}$, as defined on p. 3. It is not the sink entry $\rho_{N+1,N+1}$; that the two agree is part of milestone 1.
• Added hypotheses. The goal assumes $N \ge 2$, $J \ne 0$ and $\Gamma_{N+1} > 0$; without any one of them the limits fail. Milestones 5 and 6 assume $N \ge 3$, where $|\Psi\rangle$ and the closed form are defined.
• Uniform dephasing. The dephased clause is stated only for a uniform rate $\gamma_j = \gamma$, which is the case the paper solves. It is quantified over every $\gamma > 0$.

A trivializing formalization is ruled out by construction: $N$ and $\gamma$ are free, $p_{\rm sink}$ unfolds to an integral of an entry of the matrix exponential of the literal generator, and none of the limits is built into a definition.

Needed infrastructure includes calculus for $t \mapsto e^{tL}X$ (derivatives, HasDerivAt of entries, the fundamental theorem of calculus for $p_{\rm sink}$), invariant-subspace arguments for linear ODEs, and asymptotics of linear systems with a stable matrix. Contributions of general lemmas about Lindblad semigroups (trace preservation, Hermiticity preservation, stationary states) are welcome and reusable beyond this mission.

Not formalized here: Eq. (9) (static disorder), Eq. (10) (dissipation), §II.D–§V, the Laplace-domain route (A9)–(A13) and (A25)–(A29), the two-level system (A32), and the general networks of (A39)–(A40).

Selected references

• F. Caruso, A. W. Chin, A. Datta, S. F. Huelga, M. B. Plenio, Highly efficient energy excitation transfer in light-harvesting complexes: The fundamental role of noise-assisted transport, J. Chem. Phys. 131, 105106 (2009). https://arxiv.org/abs/0901.4454v2 — https://doi.org/10.1063/1.3223548
• G. S. Engel et al., Evidence for wavelike energy transfer through quantum coherence in photosynthetic systems, Nature 446, 782 (2007). https://doi.org/10.1038/nature05678
• M. Mohseni, P. Rebentrost, S. Lloyd, A. Aspuru-Guzik, Environment-assisted quantum walks in photosynthetic energy transfer, J. Chem. Phys. 129, 174106 (2008). https://doi.org/10.1063/1.3002335
• M. B. Plenio, S. F. Huelga, Dephasing-assisted transport: quantum networks and biomolecules, New J. Phys. 10, 113019 (2008). https://doi.org/10.1088/1367-2630/10/11/113019
• P. Rebentrost, M. Mohseni, I. Kassal, S. Lloyd, A. Aspuru-Guzik, Environment-assisted quantum transport, New J. Phys. 11, 033003 (2009). https://doi.org/10.1088/1367-2630/11/3/033003
• G. Lindblad, On the generators of quantum dynamical semigroups, Commun. Math. Phys. 48, 119 (1976). https://doi.org/10.1007/BF01608499

Motivation

Prior entanglement between sender and receiver, which exactly doubles the classical capacity of a noiseless quantum channel, can increase the classical capacity of some noisy quantum channels by an arbitrarily large constant factor depending on the channel, relative to the best known classical capacity achievable without entanglement. The enhancement factor is greatest for very noisy channels, with positive classical capacity but zero quantum capacity. Although such quantum channels can be simulated classically, no violation of causality is implied, because the simulation requires at least as much forward classical communication as the entanglement-assisted classical capacity of the channel being simulated. We obtain exact expressions for the entanglement-assisted capacity of depolarizing and erasure channels in d dimensions.

This mission is the statement-level formalization of Entanglement-Assisted Classical Capacity of Noisy Quantum Channels (arXiv:quant-ph/9904023v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract main result / equation (3): depolarizing assisted capacity (Abstract main result / equation (3): depolarizing assisted capacity, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

4 results of the paper are not stated yet, because the library lacks an interface they need:

• Unnumbered C <= CE <= FCCC: A resource-counted finite adaptive bipartite channel-simulation model with arbitrary local ancillas, message-independent prior pure entanglement, free backward classical communication, an actual forward classical arm, and asymptotically faithful reference-preserving simulation. (hard)
• Erasure flags simulate depolarization and all corresponding capacity inequalities: Source-compatible Q2 from counted noisy-channel calls interleaved with adaptive finite LOCC, initially with no shared entanglement. (hard)
• Again the difference between the bounds approaches H2(x): A source-pinned noise regime for the asserted limit of the signed quantum-bound gap. (source-ambiguity)
• Author note [9]: A transpose/label convention or restriction making the three induced classical transition matrices literally identical. (source-ambiguity)

Selected references

• Entanglement-Assisted Classical Capacity of Noisy Quantum Channels, arXiv:quant-ph/9904023v5, https://arxiv.org/abs/quant-ph/9904023v5

Motivation

How correlated are two quantum systems from the perspective of a third? We answer this by providing an optimal quantum state redistribution protocol for multipartite product sources. Specifically, given an arbitrary quantum state of three systems, where Alice holds two and Bob holds one, we identify the cost, in terms of quantum communication and entanglement, for Alice to give one of her parts to Bob. The communication cost gives the first known operational interpretation to quantum conditional mutual information. The optimal procedure is self-dual under time reversal and is perfectly composable. This generalizes known protocols such as the state merging and fully quantum Slepian-Wolf protocols, from which almost every known protocol in quantum Shannon theory can be derived.

This mission is the statement-level formalization of The operational meaning of quantum conditional information (arXiv:quant-ph/0612050v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exact state-redistribution rate region and optimal corner (Main result: exact state-redistribution rate region and corner, Eqs. (1)–(2), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

2 results of the paper are not stated yet, because the library lacks an interface they need:

• w-state: Independently moderated correction of the printed W-state numerical communication cost (source-ambiguity)
• zero-communication-entanglement: Independently moderated correction of the printed flagged-state entanglement-cost sign (source-ambiguity)

Selected references

• The operational meaning of quantum conditional information, arXiv:quant-ph/0612050v2, https://arxiv.org/abs/quant-ph/0612050v2

Motivation

The information carrying capacity of the d-dimensional depolarizing channel is computed. It is shown that this capacity can be achieved by encoding messages as products of pure states belonging to an orthonormal basis of the state space, and using measurements which are products of projections onto this same orthonormal basis. In other words, neither entangled signal states nor entangled measurements give any advantage for information capacity. The result follows from an additivity theorem for the capacity of the product of the depolarizing channel with an arbitrary channel. We establish the Amosov-Holevo-Werner p-norm conjecture for this product channel for all p >= 1, and deduce from this the additivity of the minimal entropy and of the Holevo quantity.

This mission is the statement-level formalization of The capacity of the quantum depolarizing channel (arXiv:quant-ph/0204172v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Depolarizing channel: exact unassisted classical capacity (Theorem 1 / abstract: exact unassisted classical capacity and basis strategy, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Selected references

• The capacity of the quantum depolarizing channel, arXiv:quant-ph/0204172v2, https://arxiv.org/abs/quant-ph/0204172v2

Motivation

The quantum analog of the classical erasure channel provides a simple example of a channel whose asymptotic capacity for faithful transmission of intact quantum states, with and without the assistance of a two-way classical side channel, can be computed exactly. We derive the quantum and classical capacities for the quantum erasure channel and related channels, and compare them to the depolarizing channel, for which only upper and lower bounds on the capacities are known.

This mission is the statement-level formalization of Capacities of Quantum Erasure Channels (arXiv:quant-ph/9701015v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exact capacities of the qubit quantum erasure channel (Eq. (2), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Selected references

• Capacities of Quantum Erasure Channels, arXiv:quant-ph/9701015v2, https://arxiv.org/abs/quant-ph/9701015v2

Motivation

Based on the monogamy of entanglement, we develop the technique of quantum conditioning to build an {\it additive} entanglement measure: the conditional entanglement of mutual information. Its {\it operational} meaning is elaborated to be the minimal net "flow of qubits" in the process of partial state merging. The result and conclusion can also be generalized to multipartite entanglement cases.

This mission is the statement-level formalization of An additive and operational entanglement measure: conditional entanglement of mutual information (arXiv:0804.3683v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 1: bipartite additivity (Proposition 1: bipartite additivity (the page-1 seed pinned to its numbered theorem), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

4 results of the paper are not stated yet, because the library lacks an interface they need:

• Unnumbered: fixed-extension partial state merging cost and route independence: Admissible resource/protocol class and ancillary-work accounting for the signed net-qubit PSM/PSD minimum (source-ambiguity)
• Proposition 2: CEMI as optimized partial state merging cost: Admissible resource/protocol class and ancillary-work accounting for the signed net-qubit PSM/PSD minimum (source-ambiguity)
• Proposition 4: multipartite CEMI as optimized partial state merging cost: Admissible resource/protocol class and ancillary-work accounting for the signed net-qubit PSM/PSD minimum (source-ambiguity)
• Unnumbered: reversed process partial state distribution: Admissible resource/protocol class and ancillary-work accounting for the signed net-qubit PSM/PSD minimum (source-ambiguity)

Selected references

• An additive and operational entanglement measure: conditional entanglement of mutual information, arXiv:0804.3683v2, https://arxiv.org/abs/0804.3683v2

Motivation

Gelfand duality identifies compact Hausdorff spaces with commutative unital C*-algebras: a space $X$ corresponds to the algebra $C(X)$ of continuous complex functions, and continuous maps correspond contravariantly to unital *-homomorphisms (Gelfand 1941; in categorical form, Negrepontis 1971). Measure theory has an analogous expectation. A measurable space with a σ-ideal of negligible sets yields the commutative von Neumann algebra $L^\infty$ of bounded measurable functions modulo equality almost everywhere, and every commutative von Neumann algebra should arise in this way. Making that expectation precise as an equivalence of categories requires deciding which measurable spaces to allow and which maps between them to identify.

Timeline. Stone (1936–1937) established the duality between Boolean algebras and Stone spaces, and between complete Boolean algebras and extremally disconnected ones. Segal (1951) introduced localizable measure spaces. Dixmier (1951) characterized the Gelfand spectra of commutative von Neumann algebras as the hyperstonean spaces. Loomis (1947) and Sikorski (1948) represented σ-complete Boolean algebras as measurable sets modulo meager sets on their Stone spaces. Von Neumann (1932), Maharam (1958), Ionescu Tulcea (1965), Vesterstrøm–Wils (1969), Edgar (1976) and Graf (1980) gave criteria for lifting homomorphisms of measure algebras to point maps. Pavlov (arXiv:2005.05284, J. Pure Appl. Algebra) assembled these ingredients into one equivalence of categories. That equivalence is the subject of this mission.

Setting

An enhanced measurable space $(X,M,N)$ is a set $X$, a σ-algebra $M$ of subsets of $X$, and a σ-ideal $N\subseteq M$ of the power set $2^X$, the negligible sets. A premap $f\colon(X,M,N)\to(X',M',N')$ is a map defined on a conegligible subset of $X$ with $f^*M'\subseteq M$ and $f^*N'\subseteq N$. Two premaps are weakly equal almost everywhere, $f\approx g$, when $f^*m\oplus g^*m\in N$ for every $m\in M'$. The space is compact if some compact class $K\subseteq M$ (a family with the finite intersection property for all subfamilies) has a non-negligible member inside every non-negligible measurable set. It is strictly localizable if it is isomorphic, through premaps, to a coproduct of a small family of spaces carrying faithful finite measures. CSLEMS is the category of compact strictly localizable spaces with $\approx$-classes of premaps.

A frame is a complete lattice in which finite meets distribute over arbitrary joins; the category of locales is the opposite of the category of frames. A complete Boolean algebra is localizable if $1$ is the supremum of the elements $a$ for which $aA$ carries a finite faithful continuous valuation. MLoc, the category of measurable locales, is the full subcategory of locales on the localizable Boolean algebras. A hyperstonean locale is a Stonean locale (coherent, regular, $\neg x\vee\neg\neg x=1$) in which every nonzero open has a positive normal valuation not vanishing on it. A hyperstonean space is a sober space whose locale of opens is hyperstonean. HStoneanLoc and HStonean take open maps as morphisms. CVNA is the category of commutative von Neumann algebras (C*-algebras with a predual) and normal unital *-homomorphisms.

Formalization targets

Goal: Theorem 1.1

$$\mathsf{HStonean}\simeq\mathsf{HStoneanLoc},\qquad \mathsf{HStoneanLoc}\simeq\mathsf{MLoc},\qquad \mathsf{CSLEMS}\simeq\mathsf{MLoc},\qquad \mathsf{MLoc}\simeq\mathsf{CVNA}^{\mathrm{op}}.$$

The goal is the existence of the four equivalences. It does not fix the functors.

The four equivalences with their functors

• Proposition 2.72: the equivalence $\mathsf{HStonean}\simeq\mathsf{HStoneanLoc}$ is implemented by the locale of opens $\Omega$.
• Proposition 2.73: the equivalence $\mathsf{HStoneanLoc}\simeq\mathsf{MLoc}$ is implemented by the compact opens $\mathrm{COpen}$.
• Theorem 3.20: the equivalence $\mathsf{MLoc}\simeq\mathsf{CVNA}^{\mathrm{op}}$ has inverse $\mathsf{ProjLoc}$, given by projections and restriction.
• Theorem 5.19: the equivalence $\mathsf{CSLEMS}\simeq\mathsf{MLoc}$ is implemented by $\mathsf{ML}$, the functor $(X,M,N)\mapsto M/N$, $f\mapsto f^*$.

Supporting milestones

The supporting milestones, in proof order:

• normal valuations versus continuous valuations on compact opens (Lemma 2.58);
• localizability through valuations (Lemma 2.53);
• completeness of $\mathsf{ProjAlg}(A)$ (Proposition 3.8);
• $A_*$ as continuous valuations (Proposition 3.9);
• $\mathsf{ProjAlg}$ as a functor (Lemma 3.11);
• σ-complete algebras with faithful valuations (Lemma 4.55);
• strict localizability implies localizability (Proposition 4.54);
• compactness of induced subspaces (Lemma 4.61);
• measurable images (Proposition 4.65);
• $\mathrm{TM}$ on hyperstonean spaces (Proposition 5.4);
• $\mathsf{ML}$ on morphisms (Lemma 5.11);
• the isomorphism $(X,M,N)\cong\mathrm{Spec}(\mathsf{ML}(X,M,N))$ (Proposition 5.16).

Significance

The result. Theorem 1.1 replaces commutative von Neumann algebras, a class of operator algebras, by measurable locales, which are pointless spaces. It also gives a point-set model, CSLEMS, in which morphisms are measurable maps modulo a null relation. With it, constructions on commutative von Neumann algebras can be carried out measure-theoretically and transported back: products, pushforwards of measures, and the identification of the predual with valuations. It also explains why the obvious choices fail. With localizable instead of strictly localizable spaces, with equality almost everywhere instead of weak equality, or without compactness, the measure-theoretic category is not dual to CVNA (Remarks 4.23 and 5.18).

Formalization. The theorem is proved in the paper. None of the five categories, and none of the equivalences, has a machine-checked form in Mathlib or on the platform. Mathlib has W*-algebras (WStarAlgebra), locales, Stonean spaces and Baire-measurable sets, but no normal homomorphisms, measure algebras or lifting theorems. The published module QAlgorithms_Papers_Independent_Support21_P20 formalizes this paper's valuations, enhanced measurable spaces and premaps, and poses several lemmas, three of which are milestones here. Completing the mission means formalizing Stone and Stonean duality for locales, the spectral theory of commutative von Neumann algebras through projections, and the von Neumann–Maharam lifting theorem for strictly localizable spaces.

Difficulty

The equivalences in §2 restrict classical dualities and are mostly bookkeeping once those dualities are available. Even so, Mathlib's Stone duality is not stated for locales with open maps. The central difficulty is Proposition 5.16. An object of CSLEMS must be isomorphic, through point maps, to the Stone spectrum of its own measure algebra. In one direction this needs a lifting $M/N\to M$ that is a Boolean homomorphism, and that uses strict localizability through the von Neumann–Maharam theorem. In the other direction it needs a point map from the spectrum back to $X$, constructed from the compact class. The natural first idea, choosing representatives class by class, does not give a homomorphism: liftings exist only through a transfinite construction. A second difficulty is Lemma 5.11. A Boolean homomorphism induced by a measurable map preserves countable suprema, but in general it does not preserve arbitrary ones (Remark 5.12). Compactness and the measurable image of Proposition 4.65 are what rule this out.

Formalization scope

All five categories live in one universe, with objects in Type u. The encoding commits to these conventions:

• CSLEMS. Morphisms are partial premaps (X → Option Y) modulo weak equality almost everywhere. Theorem 1.1's bullet speaks of maps of sets, but with total maps the theorem is false: $(\mathrm{pt},2^{\mathrm{pt}},2^{\mathrm{pt}})$ has no map to $\varnothing$ (Remarks 4.9, 4.15). Strict localizability uses a small index family and isomorphism in PreEMS; the faithful finite measures of its σ-finite pieces are countably additive maps $M\to\mathbb C$ with absolutely convergent sums (Remark 4.29), because Definition 4.28's saturation clause alone would also admit merely finitely additive ones. Compactness quantifies over arbitrary subfamilies, not countable ones.
• MLoc. The full subcategory of Mathlib's Locale on localizable Boolean algebras.
• HStoneanLoc and HStonean. Morphisms are open frame maps (Definition 2.15) and open continuous maps. Hyperstonean spaces are sober spaces whose frame of opens is hyperstonean.
• CVNA. Commutative CStarAlgebras with WStarAlgebra. Normality is stated as "pulls normal functionals back to normal functionals", which is equivalent to Definition 3.3 by Sakai's uniqueness of the predual.
• No nontriviality. The empty space, the one-element Boolean algebra and the zero algebra are allowed.

The equivalence milestones assert an equivalence together with a description of its functor. They never take a functor as a hypothesis, so none of the statements reduces to rfl or to an instance argument.

Reusable parts:

• the CSLEMS category, with the category laws of Propositions 4.7 and 4.14 proved inline;
• the quotient $M/N$ and the pull-back;
• $\mathrm{TM}$ and the Stone spectrum;
• the projection Boolean algebra.

Contributions are welcome at every level: proofs of the milestones, Stone and Stonean duality for locales, and a lifting theorem.

Selected references

• D. Pavlov, Gelfand-type duality for commutative von Neumann algebras, J. Pure Appl. Algebra 226 (2022); arXiv:2005.05284v3. https://arxiv.org/abs/2005.05284
• J. Dixmier, Sur certains espaces considérés par M. H. Stone, Summa Brasil. Math. 2 (1951), 151–182.
• M. H. Stone, Algebraic characterizations of special Boolean rings, Fund. Math. 29 (1937), 223–303. https://eudml.org/doc/212943
• I. E. Segal, Equivalences of measure spaces, Amer. J. Math. 73 (1951), 275–313. https://doi.org/10.2307/2372178
• D. Maharam, On a theorem of von Neumann, Proc. Amer. Math. Soc. 9 (1958), 987–994. https://doi.org/10.1090/S0002-9939-1958-0105479-6
• D. H. Fremlin, Measure Theory, Vol. 3 (Measure algebras), Torres Fremlin, 2002.
• P. T. Johnstone, Stone Spaces, Cambridge University Press, 1982.
• S. Sakai, C*-algebras and W*-algebras, Springer, 1971.

Motivation

In quantum mechanics, a system that interacts with an environment is described by a density matrix: a positive semidefinite complex matrix of trace one. When nothing is known about the joint state of the system and its environment, a natural model is to take that joint state to be a uniformly random pure state and to trace out the environment. The resulting law on density matrices, the induced measure of Życzkowski and Sommers (Życzkowski–Sommers 2001), is a standard model of a "typical" mixed state. It is used in quantum information to study the typical entanglement of bipartite pure states, as in Page's conjecture on average entropy (Page 1993).

Nechita (arXiv:quant-ph/0702154v3, Ann. Henri Poincaré 2007) studies the asymptotics of this ensemble. In the regime where the system dimension $n$ and the environment dimension $k(n)$ grow proportionally, the spectrum of the random density matrix, magnified by $cn$, has the same almost sure limit as the spectrum of a Wishart matrix: the Marchenko–Pastur law (Marchenko–Pastur 1967). The mission formalizes this result (Theorem 5) together with the chain of statements the paper uses to derive it.

Setting

Throughout, $\mathcal N_{\mathbb C}(0,1)$ denotes the law of $Z = X + iY$ where $X, Y$ are independent real Gaussians of mean $0$ and variance $1/2$, so that $\mathbb E|Z|^2 = 1$.

• Wishart matrix. If $X$ is an $n \times k$ complex matrix with i.i.d. $\mathcal N_{\mathbb C}(0,1)$ entries, $W = XX^*$ is a Wishart matrix of parameters $n$ and $k$.
• Pure states. A pure state of $\mathbb C^m$ is a ray $|\psi\rangle$: a nonzero vector up to a nonzero scalar factor. Its pure density matrix is $|\psi\rangle\langle\psi| = \psi\psi^*/\|\psi\|^2$, a rank-one orthogonal projection. The set $E_m$ of pure states carries a unique probability measure $\nu_m$ invariant under all unitaries $U \in U(m)$.
• Induced measure. Let $\mathcal H = \mathbb C^n$ (the system) and $\mathcal K = \mathbb C^k$ (the environment). If $|\psi\rangle$ has law $\nu_{nk}$ on the pure states of $\mathcal H\otimes\mathcal K$, the law of

$$\rho = \operatorname{Tr}_{\mathcal K}\,|\psi\rangle\langle\psi|$$

is the induced measure $\mu_{n,k}$ on $n\times n$ density matrices. Here $\operatorname{Tr}_{\mathcal K}$ is the partial trace over the environment.

• Empirical spectral measure. For an $n \times n$ matrix $A$ with eigenvalues $\lambda_1(A), \dots, \lambda_n(A)$ (counted with multiplicity) and a scale $s$, put $L^s(A) = \frac1n\sum_i \delta_{s\lambda_i(A)}$.
• Marchenko–Pastur law. For $c > 0$, with $a = (\sqrt c-1)^2$ and $b = (\sqrt c+1)^2$,

$$\mu_c = \max\{1-c,0\}\,\delta_0 + \frac{\sqrt{(x-a)(b-x)}}{2\pi x}\,\mathbf 1_{[a,b]}(x)\,dx .$$

Formalization targets

Goal: Theorem 5 (p. 14)

Let $c \in (0,\infty)$, let $k(n)$ be integers with $k(n)/n \to c$, and let $\rho_n$ have law $\mu_{n,k(n)}$ for every $n$. Then, almost surely,

$$L_n = \frac1n\sum_{i=1}^n \delta_{c\,n\,\lambda_i(\rho_n)} \;\Longrightarrow\; \mu_c \quad \text{weakly}.$$

Milestones, in the order the proof uses them

1. Proposition 1 (p. 4): $\nu_n$ exists and is unique.
2. Proposition 2, item 1 (p. 4): the class of a vector with law $\mathcal N^n_{\mathbb C}(0,I_n)$ has law $\nu_n$.
3. Eq. (12) (p. 6): if the coordinates $\psi_{ij}$ are arranged in an $n \times k$ matrix $X$, then $\operatorname{Tr}_{\mathcal K}|\psi\rangle\langle\psi| = XX^*/\operatorname{Tr}(XX^*)$.
4. Lemma 1 (p. 6): if $X$ has i.i.d. $\mathcal N_{\mathbb C}(0,1)$ entries, then $XX^*/\operatorname{Tr}(XX^*)$ has law $\mu_{n,k}$.
5. Eq. (24) (p. 9): the eigenvalues of $W/\operatorname{Tr} W$ are $\lambda_i/\sum_j\lambda_j$.
6. Theorem 2 (p. 8, quoted from Haagerup–Thorbjørnsen): almost surely, $\frac1n\sum_i\delta_{n^{-1}\lambda_i(W_n)} \Rightarrow \mu_c$ for Wishart matrices $W_n$ of parameters $n$ and $k(n)$.
7. Lemma 2, (45) (p. 13): $\operatorname{Tr} W_n/(n\,k(n)) \to 1$ almost surely.
8. The perturbation step (p. 14, eqs. (51)–(53)): dilating the atoms of a weakly convergent sequence by factors $t_n \to 1$ does not change a compactly supported weak limit.

Significance

The result. Theorem 5 says that the reduced state of a large random bipartite pure state has a deterministic spectral profile at scale $1/(cn)$. When $c < 1$, the environment is smaller than the system, and an atom of mass $1-c$ at $0$ records that $\rho_n$ has rank $k(n) < n$. When $c \ge 1$, the spectrum fills the interval $[a, b]$. The result transfers the classical Wishart limit to the induced measure, and with it quantitative information on the typical entanglement spectrum of bipartite pure states.

Formalizing it. The theorem is proved on paper, and none of it is machine-checked. The mission produces the induced-measure layer in Lean: complex Gaussian matrices, the invariant law on pure states, the partial-trace construction of $\mu_{n,k}$, and the Marchenko–Pastur law with its atom. Lemma 1 and eq. (12) connect these objects to Wishart matrices. The step that needs the most new library is Theorem 2, the Marchenko–Pastur theorem itself, which the paper quotes without proof. The perturbation step is posed as a statement about weak convergence. The paper argues it through convergence of moments, and in that argument weak convergence of $L_n^W$ is used as if it gave convergence of moments. The statement posed here is true as stated and needs no moment control.

Difficulty

The reduction from Theorem 5 to Theorem 2 is short on paper. The work lies elsewhere.

• Theorem 2 is a full random-matrix limit theorem. It needs a method that identifies the limit (moments, Stieltjes transforms, or free probability) and concentration strong enough to give almost sure convergence with no coupling between different $n$.
• Proposition 1 needs the invariant measure on complex projective space and a uniqueness argument for it. Mathlib's Haar-measure uniqueness is stated for groups, not for homogeneous spaces of $U(n)$.
• Lemma 1 needs the unitary invariance of the complex Gaussian vector $\mathcal N^{nk}_{\mathbb C}(0,I)$ and the image of a law under partial trace.

The naive route of "taking moments" in the perturbation step fails: weak convergence does not give convergence of moments, so (52)–(53) cannot be compared without extra tightness or moment bounds.

Formalization scope

• Pure states. Rays of $\mathbb C^m$ are represented by their rank-one projections (IsPureDensity: Hermitian, idempotent, trace one). A law on $E_m$ is a probability measure on $m\times m$ complex matrices carried by that set. Unitary invariance is invariance under $\rho \mapsto U\rho U^*$ (IsPureStateLaw).
• Induced law. "$\rho$ has law $\mu_{n,k}$" is the predicate HasInducedLaw: the law of $\rho$ is the image under the partial trace of some unitarily invariant law on pure states of $\mathbb C^n\otimes\mathbb C^k$. Proposition 1 makes this law unique.
• Indexing and partial trace. $\mathbb C^n\otimes\mathbb C^k$ is indexed by Fin n × Fin k with the environment on the right. The partial trace is the published WildeQIT.partialTraceRight. $\mathcal N_{\mathbb C}(0,1)$ is the published SpikedWishart.SoftEdge.stdComplexGaussian, with variance $1/2$ per real coordinate.
• Eigenvalues and convergence. Eigenvalues are roots of the characteristic polynomial, counted with multiplicity. Weak convergence is $\int f\,dL_n \to \int f\,d\mu_c$ for all bounded continuous $f$, with one null set for all $f$.
• Disclosed conventions. The hypotheses hold for $n \ge 1$ with $k(n)\ge 1$, since there are no pure states in dimension $0$. All random matrices live on one probability space, and nothing is assumed about their joint law across different $n$: the paper never couples them, and the almost sure statements hold for every coupling.
• Trivializations ruled out. Three trivializing formalizations are excluded:
  • stating the law of $\rho_n$ through the Wishart formula $W_n/\operatorname{Tr}W_n$, which would make Lemma 1 a hypothesis;
  • dropping the atom of $\mu_c$ or leaving the limit measure free;
  • stating "for each $f$, almost surely" in place of one null set for all $f$.

Solvers are welcome to contribute in four places:

• the general measure-theoretic pieces: Gaussian invariance, image laws under partial trace, and the dilation lemma, which are reusable beyond this mission;
• the deterministic linear algebra of eqs. (12) and (24);
• Lemma 2 through Borel–Cantelli;
• any proof of Theorem 2.

Selected references

• I. Nechita, Asymptotics of random density matrices, Ann. Henri Poincaré 8 (2007); arXiv:quant-ph/0702154v3. https://arxiv.org/abs/quant-ph/0702154v3
• K. Życzkowski, H.-J. Sommers, Induced measures in the space of mixed quantum states, J. Phys. A 34 (2001) 7111–7125. https://doi.org/10.1088/0305-4470/34/35/335
• U. Haagerup, S. Thorbjørnsen, Random matrices with complex Gaussian entries, Expo. Math. 21 (2003) 293–335. https://doi.org/10.1016/S0723-0869(03)80036-1
• V. A. Marchenko, L. A. Pastur, Distribution of eigenvalues for some sets of random matrices, Math. USSR-Sb. 1 (1967) 457–483. https://doi.org/10.1070/SM1967v001n04ABEH001994
• D. N. Page, Average entropy of a subsystem, Phys. Rev. Lett. 71 (1993) 1291–1294. https://doi.org/10.1103/PhysRevLett.71.1291

Motivation

The ultimate rates of quantum communication over optical fibre — how many secret bits or entangled pairs per channel use a lossy line can carry with unlimited local operations and classical communication (LOCC) — are bounded through a technique called teleportation stretching (Pirandola, Laurenza, Ottaviani, Banchi, arXiv:1510.08863). The idea is that if a channel $\mathcal E$ can be simulated by teleporting its input through a fixed resource state $\rho_{\mathcal E}$, then any adaptive protocol using $\mathcal E$ $n$ times can be rewritten as LOCC acting on $\rho_{\mathcal E}^{\otimes n}$, and every LOCC monotone of $\rho_{\mathcal E}$ bounds the protocol's output.

For the pure-loss channel the natural resource is the Choi state $\mathcal I\otimes\mathcal E_\eta(\Phi_{\rm EPR})$ of an ideal Einstein–Podolsky–Rosen state, which is not a normalizable state: it is the limit $\xi\to1$ of two-mode squeezed states and has infinite energy. R. Namiki (arXiv:1603.05292, 2016) observed that this limit can be avoided for lossy channels. Finite-squeezing teleportation, in the Braunstein–Kimble scheme (Braunstein and Kimble, PRL 80, 869, 1998), does not teleport perfectly, but its imperfection is itself a pure loss. Composing it with a second pure-loss channel therefore reproduces the target channel exactly, with a finite-energy resource.

Setting

A single bosonic mode is described on the Fock space $\ell^2(\mathbb N)$ with number basis $|n\rangle$. Every operator is handled through its number-basis kernel $K(m,n)=\langle m|X|n\rangle$; an operator on two modes has kernel $K((r,b),(r',b'))$, the first index labelling the first mode.

• The displacement $D(z)=e^{za^\dagger-\bar z a}$, $z\in\mathbb C$, has explicit matrix entries $\langle m|D(z)|n\rangle$; conjugation $\mathcal L_{D(z)}(X)=D(z)XD(z)^\dagger$ acts on kernels by matrix products.
• The pure-loss channel $\mathcal E_\eta$, $\eta\in(0,1)$, is the vacuum beam splitter of transmissivity $\eta$: $a\mapsto\sqrt\eta\,a$ with vacuum noise. $\mathcal I\otimes\mathcal E_\eta$ applies it to the second mode.
• The two-mode squeezed state with parameter $\xi\in(0,1)$ is $|\psi_\xi\rangle=\sqrt{1-\xi^2}\sum_{n\ge0}\xi^n|n\rangle|n\rangle$ on modes $(A',B)$.
• The CV-Bell states are $|\Phi_\beta\rangle=(\mathbb 1\otimes D^\dagger(\beta))|\Phi_0\rangle$ with $|\Phi_0\rangle=(2\pi)^{-1/2}\sum_n|n\rangle|n\rangle$; they are improper vectors with $\iint|\Phi_\beta\rangle\langle\Phi_\beta|\,dx\,dp=\mathbb 1$, where $\beta=(x+ip)/\sqrt2$.

Alice holds a two-mode state $\rho_{RS}$ ($S$ the signal, $R$ a reference) and Alice and Bob share a resource $\omega_{A'B}$. The unnormalized branch for outcome $\beta$ is the kernel on $(R,B)$

$$\langle\Phi_\beta|_{SA'}(\rho\otimes\omega)|\Phi_\beta\rangle_{SA'}=\frac1{2\pi}\sum_{n,n',k,k'}\langle n|D(\beta)|k\rangle\,\rho\big((\cdot,n),(\cdot,n')\big)\,\omega\big((k,\cdot),(k',\cdot)\big)\,\overline{\langle n'|D(\beta)|k'\rangle}.$$

Formalization targets

Goal: the Theorem (26)–(27), corrected protocol

For $0<\eta<\xi^2<1$ put $\eta'=\eta/\xi^2$ and $\rho_{\mathcal E'}=\mathcal I\otimes\mathcal E_{\eta'}(\psi_\xi)$, the effective Choi state. For every two-mode density $\rho_{AB}$,

$$\mathcal I\otimes\mathcal E_\eta(\rho_{AB})=\iint_{\mathbb R^2}\mathcal L_{\mathbb 1\otimes D(\sqrt{\eta'}\xi\bar\beta)}\Big(\langle\Phi_\beta|_{SA'}(\rho_{AB}\otimes\rho_{\mathcal E'})|\Phi_\beta\rangle_{SA'}\Big)\,dx\,dp ,$$

entry by entry, with every series and integral convergent, and $\eta\le\eta'<1$. The parameters and the protocol are independent of $\rho_{AB}$.

Milestones

1. (18) Displacement covariance: $\mathcal E_\eta(D(\beta)\rho D^\dagger(\beta))=D(\sqrt\eta\beta)\mathcal E_\eta(\rho)D^\dagger(\sqrt\eta\beta)$ for every density.
2. Composition (App. B): $\mathcal E_\eta\circ\mathcal E_{\eta'}=\mathcal E_{\eta\eta'}$.
3. (20), coherent input, corrected: $\langle\Phi_\beta|(|\alpha\rangle\langle\alpha|\otimes\psi_\xi)|\Phi_\beta\rangle=\frac{1-\xi^2}{2\pi}e^{-(1-\xi^2)|\alpha-\bar\beta|^2}|\xi(\alpha-\bar\beta)\rangle\langle\xi(\alpha-\bar\beta)|$.
4. (22), coherent input: the weights $\frac{1-\xi^2}{2\pi}e^{-(1-\xi^2)|\alpha-\bar\beta|^2}$ integrate to $1$ over $dx\,dp$.
5. (23), coherent input, corrected: after $\mathcal E_\eta$ the branch of milestone 3 becomes the same weight times $|\sqrt\eta\xi(\alpha-\bar\beta)\rangle\langle\sqrt\eta\xi(\alpha-\bar\beta)|$.
6. (24), every density, corrected: $\iint D(\sqrt\eta\xi\bar\beta)\,\mathcal E_\eta(T_{\beta,\xi}\rho T_{\beta,\xi}^\dagger)\,D^\dagger(\sqrt\eta\xi\bar\beta)\,dx\,dp=\mathcal E_{\eta\xi^2}(\rho)$.

Significance

The result. The Theorem shows that one use of a pure-loss channel, on any input including half of an entangled state, is reproduced exactly by LOCC on the finite-energy state $\mathcal I\otimes\mathcal E_{\eta'}(\psi_\xi)$. In the paper's §II.C this is the step that would let entanglement-measure bounds for $n$ adaptive channel uses be evaluated on a genuine density operator, without the limit $\xi\to1$ that the ideal-EPR argument needs. The relation (24) also makes precise in which sense the realistic teleportation family $\{T_{\beta,\xi}\}$ is not teleportation-stretching in the finite-dimensional sense, yet simulates the channel after an outcome-dependent displacement.

Formalizing it. The result is proved in the paper by a short computation through the Glauber–Sudarshan $P$ representation, which is heuristic for nonclassical inputs. No machine-checked version exists. A formal proof requires an argument valid for every density operator, together with all convergence statements. The formalization also records a sign slip: with the paper's own definitions (4), (16), (A4) and $D(\beta)=e^{\beta a^\dagger-\beta^*a}$, the step $\langle\alpha^*|D(\beta)=\langle\alpha^*+\beta^*|$ in (20) should read $\langle\alpha^*-\beta|$. Consequently (20) and (23) hold with $\alpha-\bar\beta$ in place of $\alpha+\beta$, and the correction in (24) is $D(\sqrt\eta\xi\bar\beta)$ rather than $D^\dagger(\sqrt\eta\xi\beta)$; a numerical evaluation of the printed (24) for the input $0.6|0\rangle+0.8i|1\rangle$ gives an error of $0.38$ in the output matrix, against $8\times10^{-5}$ (grid-limited) for the corrected one. The Theorem itself, existential in the protocol, is unaffected.

Difficulty

The obvious route is the paper's: write $\rho=\int P_\alpha|\alpha\rangle\langle\alpha|\,d^2\alpha$, compute everything for coherent states, and integrate. For nonclassical states $P$ is not a function, or even a measure, so this route is not a proof; passing from coherent inputs to all densities needs a density or continuity argument in trace norm, with interchange of the outcome integral and the infinite Fock series. The Bell projection itself is a contraction against improper vectors, here encoded as an absolutely convergent four-fold series whose convergence for arbitrary trace-class inputs is part of the work. Finally, the composition $\mathcal E_\eta\circ\mathcal E_{\eta'}=\mathcal E_{\eta\eta'}$ and the covariance (18) are standard on covariance matrices but must be established on number-basis kernels, where they are identities between infinite series with binomial weights.

Formalization scope

• Representation. All states and outputs are number-basis kernels. Inputs are bounded operators on $\ell^2(\mathbb N)$ or $\ell^2(\mathbb N\times\mathbb N)$ satisfying the published density predicates (trace class, self-adjoint, positive, unit trace), from QAlgorithms_Papers_Independent_Dependency50_P39; the loss channel is the vacuum-loss kernel of QAlgorithms_Papers_Independent_Frontier30_P21; coherent states use its coherentDensity.
• Bell projection. It is the Fock form of (16) with (A4), with the factor $(2\pi)^{-1}$ explicit; the CV-Bell states are not formalized as vectors. The outcome is $\beta=(x+ip)/\sqrt2$ and the average is over $\mathbb R\times\mathbb R$ with Lebesgue measure, the paper's $dx\,dp$.
• Conventions. The resource has Alice's mode $A'$ first and Bob's mode $B$ second; the loss of $\rho_{\mathcal E'}$ acts on $B$. Every series is asserted summable and every integrand integrable as part of the conclusion, so default values of divergent series or non-integrable functions never satisfy a statement.
• Corrected sign. Milestones (20), (23), (24) and the goal use $\alpha-\bar\beta$ and the correction $D(\sqrt{\eta'}\xi\bar\beta)$, as explained above.
• Coherent-input restriction. Milestones (20), (22), (23) are stated for coherent inputs ($P$ a point mass), because the $P$ representation (19) is not available for general states; (24) and the goal are stated for every density, as printed.
• LOCC. The general class of LOCC maps is not formalized; $\Lambda$ is the explicit protocol of (24). An existential "there is a map $\Lambda$ with $\Lambda(\rho_{\mathcal E'})=\mathcal I\otimes\mathcal E_\eta(\rho_{AB})$" would be trivially true (take $\Lambda$ constant) and is ruled out by stating the protocol, with $\eta'$, $\xi$ and the correction fixed before $\rho_{AB}$; likewise the Bell branch is the defining series, never its closed form.
• Not covered. The thermal-loss and amplifier versions (§III, (30)–(33)), the $n$-use relative-entropy bound (§II.C), and the finite-dimensional review (§II.A). The statement $\mathcal E_\eta(|\alpha\rangle\langle\alpha|)=|\sqrt\eta\alpha\rangle\langle\sqrt\eta\alpha|$ used inside (20) is the existing Open goal Frontier30.P21.coherentOutput and is not posed again.
• Reusable parts. Proofs of displacement covariance and of channel composition on Fock kernels, and summability lemmas for displacement matrices against trace-class kernels, are useful beyond this mission; contributions of such lemmas are welcome.

Selected references

• R. Namiki, Teleportation stretching for single-mode Gaussian channels, arXiv:1603.05292v1, 2016. https://arxiv.org/abs/1603.05292
• S. Pirandola, R. Laurenza, C. Ottaviani, L. Banchi, Fundamental limits of repeaterless quantum communications, arXiv:1510.08863v3, 2015. https://arxiv.org/abs/1510.08863
• S. L. Braunstein, H. J. Kimble, Teleportation of continuous quantum variables, Phys. Rev. Lett. 80, 869, 1998. https://doi.org/10.1103/PhysRevLett.80.869