All missions

Motivation

We investigate Gaussian quantum states in view of their exceptional role within the space of all continuous variables states. A general method for deriving extremality results is provided and applied to entanglement measures, secret key distillation and the classical capacity of Bosonic quantum channels. We prove that for every given covariance matrix the distillable secret key rate and the entanglement, if measured appropriately, are minimized by Gaussian states. This result leads to a clearer picture of the validity of frequently made Gaussian approximations. Moreover, it implies that Gaussian encodings are optimal for the transmission of classical information through Bosonic channels, if the capacity is additive.

This mission is the statement-level formalization of Extremality of Gaussian quantum states (arXiv:quant-ph/0509154v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1, (2): general Gaussian extremality (original seed) (Lemma 1, (2): general Gaussian extremality (original seed), PDF p. 1). 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

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

• Unnumbered application (i): distillable-entanglement minimum: Operational extended LOCC conversion rate for full oscillator inputs and one arbitrary fixed multipartite normalized target (hard)
• Unnumbered sufficient covariance distillability criterion: Positive computed full-oscillator bipartite LOCC distillation rate (hard)
• Proposition 2: collective-attack distillable secret key: Computed collective-attack multipartite secret-bit rate on full oscillator densities (hard)
• Proposition 3: optimal Gaussian average encoding under additivity: Full-mode E_F convex roof, its global strong-superadditivity hypothesis, and constrained regularized capacity linked to the same Gaussian dilation (hard)
• Unnumbered single-mode coherent Gaussian ensemble: Restrictions on the fixed channel/dilation making inverse images of optimal joint Gaussian-roof components coherent input states (source-ambiguity)
• Introduction: distillable-randomness claim: Source-selected operational randomness resource, communication restrictions and unit (source-ambiguity)
• Conclusion: claimed translation to Fermionic systems: Source-selected CAR covariance, parity, local tensor and operational resource conventions (source-ambiguity)

Selected references

• Extremality of Gaussian quantum states, arXiv:quant-ph/0509154v1, https://arxiv.org/abs/quant-ph/0509154v1

Motivation

Additivity of the Holevo capacity is proved for product channels, under the condition that one of the channels is in a certain class of unital qubit channels, with the other completely arbitrary. This qubit class includes the depolarizing channel. As a byproduct this proves that the Holevo bound is the ultimate information capacity of such qubit channels (assuming no prior entanglement between sender and receiver). Additivity of minimal entropy and multiplicativity of p-norms are also proved under the same assumptions.

This mission is the statement-level formalization of Additivity for a class of unital qubit channels (arXiv:quant-ph/0103156v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Unital qubit channels: norm multiplicativity and entropy and Holevo additivity (Theorem 1, equations (5)–(7), PDF p. 4). 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

• Additivity for a class of unital qubit channels, arXiv:quant-ph/0103156v2, https://arxiv.org/abs/quant-ph/0103156v2

Motivation

We study the symmetric-side-channel-assisted private capacity of a quantum channel, for which we provide a single-letter formula. This capacity is additive, convex, and, for degradable channels, equal to the unassisted private capacity. While a channel's (unassisted) capacity for for private classical communication may be strictly larger than its quantum capacity, we will show that these capacities are equal for degradable channels, thus demonstrating the equivalence of privacy and quantum coherence in this context. We use these ideas to find new bounds on the key rate of quantum key distribution protocols with one-way classical post-processing. For the Bennett-Brassard-84 (BB84) protocol, our results demonstrate that collective attacks are strictly stronger than individual attacks.

This mission is the statement-level formalization of The private classical capacity with a symmetric side channel and its application to quantum cryptography (arXiv:0705.3838v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5 (seed paper result): single-letter ss-private capacity (Theorem 5 (seed paper result): single-letter ss-private 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

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

• Equation (5): combined convex-hull BB84 bound: Meaning of conv and its admissible interpolation domain for the nonlinear independent-error channel family (source-ambiguity)
• Unnumbered main result: collective attacks outperform individual attacks on BB84: Matched individual/collective optimized protocol model and numerical comparison witness (source-ambiguity)
• Section IV.E: degradable-mixture collective attacks and their key-rate bound: Exact optimized key rate after the specified environmental measurement (source-ambiguity)

Selected references

• The private classical capacity with a symmetric side channel and its application to quantum cryptography, arXiv:0705.3838v1, https://arxiv.org/abs/0705.3838v1

Learning the dynamics from logged data

Offline reinforcement learning and off-policy evaluation start from a single logged trajectory of a controlled system. The policy that generated the log is often unknown, history-dependent and not stationary. Model-based methods first estimate the transition probabilities of the system from this log, then plan or evaluate policies in the estimated model (Agarwal, Kakade & Yang, 2020; Li et al., 2024). How many samples that estimate needs is the question of Banerjee, Honnappa & Rao.

For an uncontrolled, geometrically ergodic Markov chain on $d$ states, Wolfer & Kontorovich (2021) showed that the transition matrix can be learned to accuracy $\varepsilon$ in the $\infty$-norm from of order $d/(\pi_\star\varepsilon^2)$ samples, where $\pi_\star$ is the smallest stationary probability, and that this rate is minimax. Banerjee, Honnappa and Rao extend this to controlled chains whose controls may depend arbitrarily on the past. Stationarity, irreducibility and aperiodicity then need not hold.

Controlled Markov chains and the empirical estimator

A controlled Markov chain with $d$ states and $k$ controls consists of:

1. a state process $X_0,X_1,\dots$ in $\chi=\{1,\dots,d\}$;
2. a control process $a_0,a_1,\dots$ in $\mathbb I=\{1,\dots,k\}$;
3. a row-stochastic transition matrix $M^{(l)}$ for each control $l$.

Both processes are adapted to a filtration $\{\mathcal F_i\}$, and

The controls are otherwise arbitrary.

From a sample of length $m$, the visit counts are $N^{(l)}_s=\sum_{i=1}^m\mathbb 1[X_i=s,a_i=l]$ and $N^{(l)}_{s,t}=\sum_{i=1}^m\mathbb 1[X_i=s,X_{i+1}=t,a_i=l]$. The empirical estimator is $\hat M^{(l)}_{s,t}=N^{(l)}_{s,t}/N^{(l)}_s$, and its error is measured by

Three conditions control the chain:

1. Assumption 1 asks for sets $S_i$ of state–control pairs with $0<\zeta_2\le\mathbb P((X_i,a_i)\in S_i)\le\zeta_1<1$. Put $\zeta^{(\max)}=\max\{\zeta_1,1-\zeta_2\}$.
2. Assumption 2 bounds the return times. Let $H_0=0$ and let $H_i$ be the $i$-th time $n\ge1$ with $(X_n,a_n)=(s,l)$. The return times $\tau^{(i)}_{s,l}=H_i-H_{i-1}$ must satisfy $\sup_{s,l,i}\mathbb E[\tau^{(i)}_{s,l}\mid\mathcal F_{H_{i-1}}]<T$ almost surely.
3. Assumption 4 asks for geometric decay of the weak mixing coefficient $\bar\eta_{i,j}$. This coefficient is the largest change, caused by changing $(X_i,a_i)$ while the history before $i$ is kept fixed, in the conditional probability of an event of the window $(X_j,a_j),\dots,(X_m,a_m)$. The decay is $\bar\eta_{i,j}\le((\mathbb C_\Delta-1)/\mathbb C_\Delta)^{j-i}$ for a constant $\mathbb C_\Delta>1$.

The uniform mixing coefficient $\phi_{i,j}$ compares the conditional law of the window given the whole history up to $i$ with its unconditional law. With $\rho_\star=\max_{s,l}\sup_{1\le i\le m}\mathbb P(X_i=s,a_i=l)$ the paper defines

and $\mathbb C_{T,\delta}=\mathbb C_T\log(6dk/\delta)$, $\mathbb C_{\zeta,\delta}=\mathbb C_\zeta\log(6dk/\delta)$. Here $\mathbb C_{pel}$ depends on $\mathbb C_\Delta$ only.

Formalization targets

Goal: Theorem 2, both clauses

(a) Sample complexity. There are a universal $c>1$ and a positive function $\mathbb C_{pel}(\mathbb C_\Delta)$ such that every controlled Markov chain satisfying Assumptions 1, 2 and 4 has, for $\varepsilon>0$ and $\delta\in(0,1)$,

The printed threshold lacks the second and third terms and is false without them: i.i.d. uniform states satisfy all assumptions with $T=d+1$, but the printed threshold is then $O(d(\log d)^3)$, far below the $d^2$ samples that are needed.

(b) Minimaxity. This is the paper's Appendix G.3 Part 1. For $d\ge d_0$ (a universal threshold), $0<p_\star<1/(d+1)$ and $\sigma\in\{-1,1\}^{\lfloor d/2\rfloor}$, let $M_\sigma$ be the transition matrix on $d+1$ states whose first $d$ rows are $b=((1-p_\star)/d,\dots,(1-p_\star)/d,p_\star)$ and whose last row is $b$ perturbed by $\pm16\sigma_i\varepsilon/d$ in consecutive pairs of coordinates (the page takes $d$ even; for odd $d$ the leftover coordinate is left unperturbed). These chains exist. They satisfy the three assumptions with $\zeta_1=\zeta_2=p_\star$, $T=\lceil3/p_\star\rceil$ and $\mathbb C_\Delta=4/3$. For $0<\varepsilon<1/32$ and $\delta<1/2$,

Since $T\asymp1/p_\star$ on this family, the term $dT/\varepsilon^2$ of (a) cannot be improved beyond a universal constant.

Milestones

1. Proposition 1 (row error at bounded visit counts, corrected).
2. Lemma 2 (bounds on $\mathbb E[N^{(l)}_s]$).
3. Lemma 1 (weak vs. uniform mixing, corrected).
4. Lemma 9 (covariance inequality, corrected).
5. Proposition 3 (a Bernstein bound for $N^{(l)}_s$, corrected).
6. The elementary step $m\ge2x(\log x)^2\Rightarrow m/(\log m)^2\ge x$.
7. The Varshamov–Gilbert packing.
8. The bound $\mathrm{KL}(\eta(\sigma)\|b)\le512\varepsilon^2$.
9. The chain rule (G.22).
10. The stationary distribution (G.23).

Significance

Clause (a) gives an estimate of all $k$ transition matrices from one trajectory logged by an arbitrary adapted policy, with explicit dependence on the return-time constant $T$, the visitation constants $\zeta_1,\zeta_2$ and the mixing constant. Error bounds for off-policy evaluation and for recovering optimal values follow from it in the paper's Section 5. Clause (b) shows that no estimator does better than the empirical one by more than a universal factor in the leading term.

Neither clause has a machine-checked proof. Four printed statements on the path are false as stated and are posed here in corrected form, each with a counterexample in its item:

• the threshold of Theorem 2;
• Proposition 1;
• Lemma 1;
• Lemma 9.

Proposition 3 is posed in the regime where its printed bound holds. A complete formalization would give the first checked minimax result for estimating a controlled Markov chain. It would also give the first checked concentration inequality for visit counts of a non-stationary mixing process.

Difficulty

Under arbitrary adapted controls the visit counts are not sums of independent or stationary terms, and the number of transitions observed from a state is random and correlated with the transitions themselves. Applying a fixed-sample-size concentration bound row by row therefore fails. The deviation of $N^{(l)}_s$ around its mean has to be controlled by a Bernstein-type inequality for non-stationary, geometrically mixing bounded sequences, with constants that depend on the mixing rate alone. The constants must not depend on $d$, $k$ or the chain. Such an inequality is not in Mathlib. The lower bound needs Fano's method, or an equivalent, for path laws of Markov chains.

Formalization scope

• States are Fin d and controls Fin k, with $d,k\ge1$, and time is $\mathbb N$ from $0$.
• The chain is a structure on a probability space with a Mathlib Filtration ℕ. It carries adapted $X$, $a$, row-stochastic matrices and the conditional transition law.
• The counts run over $i=1,\dots,m$ and $N^{(l)}_{s,t}$ reads $X_{m+1}$. $\hat M$ uses Lean's $0/0=0$.
• $\|\cdot\|_\infty$ is the maximum row $\ell^1$ sum, not the largest entry: under the largest-entry norm the hard family's members are only $32\varepsilon/d$ apart and clause (b) is false.
• Visit times take values in $\mathbb N\cup\{\infty\}$, with the first visit at a time $n\ge1$.
• Assumption 2 uses Mathlib's conditional expectation with respect to the σ-algebra at the previous visit. It requires the return times to be almost surely finite and integrable, and bounds the supremum strictly by $T$.
• $\bar\eta$ and $\phi$ are finite maxima over the window up to $m$, using elementary conditional probabilities. Assumption 4 holds for $0\le i<j\le m$, and Assumption 1 at the times $1\le i\le m$.
• The constants $c$, $c_2$, $d_0$ and the function $\mathbb C_{pel}$ are quantified before the chain. A $c$ or $\mathbb C_{pel}$ that depends on $d$, $k$, $T$ or the chain would make (a) a different, weaker statement.
• Clause (b) quantifies over every estimator, i.e. every function of $X_0,\dots,X_{m+1}$, and asserts that the hard chains exist. A family that cannot be realized would make (b) vacuous.

A complete development needs several pieces of infrastructure, all reusable beyond this mission:

• the strong Markov property at visit times;
• a Bernstein inequality for $\phi$-mixing sequences;
• Fano's inequality with a packing;
• KL chain rules for Markov path laws.

Contributions of any of these, and proofs of the milestones, are welcome.

Selected references

• I. Banerjee, H. Honnappa, V. Rao, Offline Estimation of Controlled Markov Chains: Minimaxity and Sample Complexity, Operations Research, 2025; arXiv:2211.07092v5. https://arxiv.org/abs/2211.07092
• G. Wolfer, A. Kontorovich, Statistical estimation of ergodic Markov chain kernel over discrete state space, Bernoulli 27(1), 2021. https://arxiv.org/abs/1902.00080
• F. Merlevède, M. Peligrad, E. Rio, Bernstein inequality and moderate deviations under strong mixing conditions, High Dimensional Probability V, IMS Collections 5, 2009. https://arxiv.org/abs/0902.0582
• A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009. https://doi.org/10.1007/b13794
• A. Agarwal, S. Kakade, L. F. Yang, Model-based reinforcement learning with a generative model is minimax optimal, COLT 2020. https://arxiv.org/abs/1906.03804
• G. Li, L. Shi, Y. Chen, Y. Chi, Y. Wei, Settling the sample complexity of model-based offline reinforcement learning, Annals of Statistics 52(1), 2024. https://arxiv.org/abs/2204.05275

This problem asks for a formal proof of the complete conditional geometric K24 change-of-slice result, including its regularity obstruction. The source gives informal analytic arguments; this publication does not claim a new proof or a new unsolved conjecture for the standard perturbation lemma. It does not assert existence of the still-missing geometric organizer in the four-dimensional Einstein research program.

Let $M$ be a closed smooth real four-manifold with an actual common smooth circle action. Write $\Pi_0$ for its normalized Haar average on the relevant tensor, covector, or vector bundle and $\Pi_\perp=I-\Pi_0$. Let the positive metrics $\widehat g$ and $z$ be invariant under that same action; the actual nearby positive metric $g$ need not be invariant. The scalar $\lambda$ is arbitrary. Define

where $\beta_h u=-\operatorname{div}_h u+\tfrac12d\operatorname{tr}_h u$, $\delta_h^*$ is the symmetrized covariant derivative with factor $1/2$, and $\mathcal K_hY=\mathcal L_Yh$. These are actual geometric differential operators, not freely supplied linear maps.

Fix the numerical data for a uniformly bounded local finite-cover system, metric ellipticity and coefficient bounds, $0<\alpha<1$, and a uniform pullback bound $H\ge1$ for the common action. These bounds are fixed before the conclusion constants are chosen. Covering degree is not globally bounded, and the downstairs overlap count is kept separate from the internal coordinate atlas on each covering manifold. The proposition requires all of the following.

1. Exact tensor identities and genuine differentiation. Prove the full product rule

Invariance makes the middle term vanish. On the genuine zero-Haar-mean tensor sector, identify the difference of the fixed-reference and re-anchored derivatives as

The target also includes the actual connection/Bianchi coefficient expansions, principal-symbol identification by a quadratic-jet test and its intrinsic norm bound, sector preservation and equivariance. It requires the displayed variation to be the Fréchet derivative in the specified section norms on a positive-radius metric neighborhood, not just a pointwise or directional derivative.

2. Uniform tensor estimates in both scales. For one uniform $C_T$,

For every real $s>4$, with the corresponding fixed local Sobolev coefficient/atlas bounds, require a uniform $C_S$ with

The Sobolev clause is not restricted to integer order and does not impose higher Hölder regularity on the metric. It uses local real-order metric and inverse-metric bounds; it does not impose a fixed global bound on the degree-dependent norm of the whole metric.

3. Both vector errors and the correct regularity. For the actual projected operator $B_{\widehat g,g}Y=\Pi_\perp\beta_{\widehat g}\mathcal L_Yg$, retain both terms:

Prove the natural $C^{2,\alpha}\to C^{0,\alpha}$ estimate by a uniform constant times $(\|\widehat g-z\|_{C^{2,\alpha}}+\|g-z\|_{C^{2,\alpha}})\|Y\|_{C^{2,\alpha}}$. For the shifted $C^{3,\alpha}\to C^{1,\alpha}$ pair, both metric differences must instead be controlled in $C^{3,\alpha}$. The actual Bianchi–Killing/rough-Laplacian identity is also included.

4. Geometric inverse transfer. In each stated pair of actual zero-mean section spaces, suppose the re-anchored projected operator is a bounded linear isomorphism with inverse bound $C_A$ (or $C_B$). If that bound times the norm of the actual difference operator is strictly below $1/2$, prove that the fixed-reference operator is an isomorphism with inverse bound at most $2C_A$ (respectively $2C_B$), including surjectivity and the corresponding Banach-dual gap. Mere absence of kernel is not substituted for the initial isomorphism. Norm, completeness, Haar integrability/boundedness and projection facts needed for this argument are requested conclusions about the concrete spaces; they are not assumed copies of the desired theorem.

5. Actual flat-torus sharpness. On the genuine four-torus with coordinates of period $2\pi$, use the flat metric, the circle translation in $x_2$, $V=\sin(x_2)\partial_{x_1}$ and

Require positivity of $g_n=g_0+f_n$ for $n\ge2$, finite norms, $\|f_n\|_{C^{2,\alpha}}\to0$, bounded $C^{3,\alpha}$ norms, and a lower bound $\pi^{-\alpha}$ for the $C^{1,\alpha}$ norm of the projected actual vector-operator difference tested on $V$. Consequently no uniform shifted estimate using only the $C^{2,\alpha}$ metric difference can hold. This is a statement about genuine torus tensors and operators, not an abstract sequence of scalar exponents.

Norm and formalization choices. The definition packages specify full big Hölder norms from actual iterated derivatives and top-order Hölder seminorms, hierarchical local finite covers, and real-order Bessel–Sobolev norms with explicit partitions. Sobolev carriers use the continuous/C² representatives justified by the requested ranges; their completeness and norm properties remain to be proved. The adapted Sobolev norm is an explicit upstairs sum and is not identified with downstairs $L^2$ independently of covering degree. Haar averaging is pointwise in finite-dimensional fibers, avoiding an unsupported assumption of norm-continuous action on big Hölder space. The projection bounds are $H$ and $1+H$; $1$ and $2$ apply only in the isometric case. Raw inverse, derivative and integral definitions are totalized in Lean, while positivity, regularity, integrability and the analytic properties are enforced by the full statement's hypotheses or required conclusions. Definitions have no admissions or new axioms. There is exactly one intentional unproved theorem placeholder.

Remaining application boundary. K24 does not construct the common marked action, the required same-window $C^2$/$C^3$ closeness, or the adapted re-anchored inverse from an arbitrary Einstein degeneration. Those organizer inputs remain open. The nonlinear diffeomorphism-chart and quadratic-remainder applications in K16/K21 are separate supporting questions; they require their own loss-aware regularity hypotheses/proofs. Neither those applications nor the original Einstein conjecture is claimed proved by this publication.

Motivation

Fault-tolerant quantum computers implement Clifford gates cheaply and the non-Clifford T gate expensively, because T gates are obtained by magic-state distillation (Fowler, Stephens and Groszkowski). Single-qubit rotations by small, arbitrary angles appear throughout quantum simulation and must be compiled into Clifford+T circuits, so the T-count of a small rotation is a standard cost measure. Selinger's ancilla-free method uses about $4\log_2(1/\theta)$ T gates for a $Z$-rotation by $\theta$ (arXiv:1212.6253), and the paper's own search puts optimal ancilla-free Clifford+T synthesis near $3\log_2(1/\theta)$ (Sec. VI).

Wiebe and Kliuchnikov (arXiv:1305.5528) proposed non-deterministic circuits with ancillas and measurement, the gearbox circuit and its recursive composed gearbox circuit, which, like the linear-combination-of-unitaries circuits of Childs and Wiebe, turn a coarse rotation into a much finer one and whose failures are undone by a Clifford gate, so they can be repeated until they succeed. The cost of such a repeat-until-success scheme is a random variable. Theorem 2 of the paper computes its mean exactly and bounds its variance; this mission formalizes that result together with the circuit identities it rests on.

Setting

A qubit has basis $|0\rangle,|1\rangle$; a gate is a $2\times2$ unitary $U$ with entry $U_{1,0}=\langle1|U|0\rangle$. Let $X=\begin{pmatrix}0&1\\1&0\end{pmatrix}$ and $e^{-i\varphi X}=\cos\varphi\,\mathbb 1-i\sin\varphi\,X$.

Gearbox circuit $C^{(d)}(U^1,\dots,U^d)$. Prepare $d$ ancillas in $|0\rangle$ and a target in $|\psi\rangle$. Apply $U^1\otimes\cdots\otimes U^d$ to the ancillas, then a $d$-controlled $-iX$ on the target (active when every ancilla is $|1\rangle$), then $U^{1\dagger}\otimes\cdots\otimes U^{d\dagger}$, and measure the ancillas in the computational basis. Outcome $0\cdots0$ is success.

Composed gearbox circuit (Definition 1). $C^{\circ1}(U)$ is $C^{(1)}(U)$, and $C^{\circ d}(U)=C^{\circ1}(C^{\circ(d-1)}(U))$: the gate fed to the outer gearbox is the rotation the inner composed circuit enacts on success. Write $\theta_0\in[0,\pi/2]$ for the angle with $\sin^2\theta_0=|U_{1,0}|^2$ and, for $q\ge1$,

Cost. Level $q$ of $C^{\circ d}(U)$ is attempted until its measurement succeeds; the number of attempts $N_q$ is geometric on $\{1,2,\dots\}$. Each attempt at level $q\ge2$ needs one successful copy of $C^{\circ(q-1)}(U)$ and one of its inverse. With $x_d$ the number of applications of $C^{\circ1}(U)$ before $C^{\circ d}(U)$ succeeds, Appendix A's equation (A1) reads

with $\eta_i,\chi_i$ distributed as $x_{d-1}$ and everything independent. Each $C^{\circ1}(U)$ uses one $U$ and one $U^\dagger$, so the number of applications of $U$ or $U^\dagger$ is $n_d=2x_d$.

Formalization targets

Goal: Theorem 2 (p. 6)

For every unitary $U$ and $d\ge1$,

and, for $\theta_0<\pi/4$,

Both clauses are stated as printed; the mean is exact for every $\theta_0\in[0,\pi/2]$.

Milestones

1. Theorem 1 (p. 2): on outcome $0$ the gearbox circuit leaves $\sqrt{\cos^4\theta+\sin^4\theta}\,e^{-iX\tan^{-1}(\tan^2\theta)}|\psi\rangle$, where $\sin^2\theta=\prod_\ell|U^\ell_{1,0}|^2$; this has probability $\cos^4\theta+\sin^4\theta$; every other outcome enacts $e^{i\pi X/4}$ up to a scalar.
2. Corollary 1 (p. 5): on success, $C^{\circ d}(U)=e^{-i\tan^{-1}(\tan^{2^d}\theta_0)X}$.
3. Appendix A, p. 14: the level-$q$ success probability is $P_q$; $\mathbb E(N_q)=1/P_q$ and $\mathbb V(N_q)=(1-P_q)/P_q^2$.
4. (A3): $\mathbb E(x_d)=2\,\mathbb E(N_d)\,\mathbb E(x_{d-1})$.
5. (A6): $\mathbb V(x_d)=2\,\mathbb V(x_{d-1})\,\mathbb E(N_d)+4\,\mathbb V(N_d)\,(\mathbb E(x_{d-1}))^2$.
6. Appendix A, p. 15: $P_q$ increases with $q$ when $\theta_0<\pi/4$.

Significance

The theorem shows that the composed gearbox reaches a rotation angle of order $\tan^{2^d}\theta_0$, doubly exponentially small in $d$, while using $\Theta(2^d)$ applications of $U$ in expectation, with a variance of the same squared order. Since $d\approx\log_2\log(1/\theta)$ levels give angle $\theta$, the gate cost scales like $\log(1/\theta)$ with a constant that depends on $U$ only through $P_1,P_2,\dots$; this is the basis of the paper's floating-point synthesis scheme, which combines a mantissa rotation with an exponent rotation produced this way (Sections IV–V).

The result has a complete written proof in Appendix A. As far as is known it has no machine-checked proof. The formalization adds three things: the circuit identities of Theorem 1 and Corollary 1 as exact matrix statements, including the boundary case $|U_{1,0}|=1$; the identification of the circuit's Born-rule success probabilities with the closed forms $P_q$; and the random-sum identities (A3), (A6) in a form where infinite moments cannot be hidden.

Difficulty

The computational parts are elementary but long. The real difficulty is that the theorem joins two models: a quantum circuit, whose success probabilities come from matrix entries of a post-selected block, and a nested random sum whose summands are themselves random sums. A naive approach postulates the success probabilities $P_q$ and proves a lemma about compound geometric sums. That approach proves nothing about the circuit: the content linking the two is milestone 3, which needs Theorem 1 at every level of the recursion and Corollary 1 to identify the gate fed to level $q$. On the probabilistic side, the variance identity for a random number of independent summands requires finiteness of all second moments, and the bound requires unfolding a recursion whose coefficients $1/P_q$ vary with the level, which is where the monotonicity of $P_q$ enters.

Formalization scope

States are vectors Fin 2 → ℂ; gates are Matrix (Fin 2) (Fin 2) ℂ, unitarity is membership in Matrix.unitaryGroup, and $|0\rangle,|1\rangle$ are indices 0, 1. The $d$ ancillas are Fin d → Fin 2, and the joint space is (Fin d → Fin 2) × Fin 2 with ancillas first; the controlled gate fires on the all-ones string. The rotation is the matrix $\cos\varphi\,\mathbb 1-i\sin\varphi\,X$, so $e^{i\pi X/4}$ is the rotation by $-\pi/4$. Because Lean's Real.tan returns $0$ at $\pi/2$, the angles $\tan^{-1}(\tan^2\theta)$ and $\tan^{-1}(\tan^{2^d}\theta_0)$ are defined to be $\pi/2$ when the cosine vanishes, the paper's value $\tan^{-1}(\infty)$; the case $|U_{1,0}|=1$ is not excluded. $C^{\circ d}(U)$ is the recursively defined success unitary: the outcome-$0$ block of the one-ancilla gearbox fed with $C^{\circ(d-1)}(U)$, normalized by the norm of its first column.

The number of applications of $U$ or $U^\dagger$ used to enact $C^{\circ d}(U)$ is modelled by Appendix A's recursion (A1): Theorem 2 speaks of "a given attempt", but its proof defines $x_d$ as the count until $C^{\circ d}(U)$ succeeds, and that is the quantity formalized. Laws are Mathlib PMF ℕ with independence built into bind; the geometric law is Mathlib's geometricMeasure shifted to $\{1,2,\dots\}$; means and variances are ℝ≥0∞-valued sums.

Three trivializing formalizations are ruled out. The law of $n_d$ uses the circuit's Born-rule success probabilities, never $P_q$ supplied as an input, so Theorem 1 and Corollary 1 are needed for the goal. Moments are in $[0,\infty]$, so a divergent variance is $\infty$, never the junk value $0$ that would make the bound trivially true. The angle convention above excludes the false reading $\tan(\pi/2)=0$ in Theorem 1 and Corollary 1.

Everything needed is in Mathlib: matrices, unitaryGroup, Real.arctan, PMF.bind/PMF.map, geometricMeasure. Reusable beyond this mission: the moments of the shifted geometric law and the mean and variance identities for a sum of a random number of i.i.d. summands, in ℝ≥0∞ form. Contributions to any milestone are welcome; the probabilistic milestones (3–6) do not depend on the circuit milestones except through part 1 of milestone 3.

Selected references

• N. Wiebe and V. Kliuchnikov, Floating point representations in quantum circuit synthesis, arXiv:1305.5528v3, 2013. https://arxiv.org/abs/1305.5528v3
• P. Selinger, Efficient Clifford+T approximation of single-qubit operators, Quantum Inf. Comput. 15, 2015. https://arxiv.org/abs/1212.6253
• A. M. Childs and N. Wiebe, Hamiltonian simulation using linear combinations of unitary operations, Quantum Inf. Comput. 12, 2012. https://arxiv.org/abs/1202.5822
• A. G. Fowler, A. M. Stephens and P. Groszkowski, High-threshold universal quantum computation on the surface code, Phys. Rev. A 80, 052312, 2009. https://arxiv.org/abs/0803.0272

Motivation

Quantum information carried by continuous variables, such as the quadratures $x$ and $p$ of an optical mode, is cheap to manipulate with beam splitters, squeezers and homodyne detectors, but these Gaussian tools cannot protect Gaussian states against Gaussian noise: Niset, Fiurášek and Cerf proved in 2008 that no Gaussian error-correcting code can do better than direct transmission against Gaussian channels (arXiv:0811.3128). Peter van Loock's note (arXiv:0811.3616) shows that this no-go does not cover non-Gaussian noise: a stochastic error that displaces a mode by a fixed amount with probability $\gamma$ turns a Gaussian state into a discrete mixture, and against it a purely Gaussian three-mode repetition code (offline squeezing, two beam splitters, homodyne detection, feedforward) reduces the error probability from $\gamma$ to $\gamma^3$.

The example is the continuous-variable analogue of the three-qubit bit-flip code. Unlike that code, it identifies double errors as well as single ones, so it improves on direct transmission without the qubit code's requirement $\gamma<1/2$.

Setting

A single optical mode is described by its Wigner function $W(x,p)$, a real function on phase space $\mathbb R^2$; three modes by a function of $x=(x_1,x_2,x_3)$ and $p=(p_1,p_2,p_3)$. Units are those in which the vacuum has variance $1/4$.

• Input: the coherent state with mean $(\bar x_1,\bar p_1)$, $W_{\mathrm{in}}(x_1,p_1)=\frac2\pi e^{-2(x_1-\bar x_1)^2-2(p_1-\bar p_1)^2}$.
• Ancillas: two x-squeezed vacua with squeezing parameter $r$, $W_{\mathrm{anc}}(x,p)=\frac2\pi e^{-2e^{2r}x^2-2e^{-2r}p^2}$.
• Tritter: the orthogonal matrix $D$ with rows $(1,1,1)/\sqrt3$, $(\sqrt{2/3},-1/\sqrt6,-1/\sqrt6)$, $(0,1/\sqrt2,-1/\sqrt2)$, acting on $x$ and on $p$. Encoding maps $W$ to $W(Dx,Dp)$, decoding maps $W$ to $W(D^{\mathsf T}x,D^{\mathsf T}p)$.
• Channel: each mode independently is displaced by $\bar x_2>0$ in $x$ with probability $\gamma\in(0,1)$; on a single mode, $W\mapsto(1-\gamma)W(x,p)+\gamma W(x-\bar x_2,p)$.
• Syndrome and recovery: after decoding, modes 2 and 3 are measured by x-homodyne detection (integrating out $p_2,p_3$), mode 1 is displaced by a feedforward $\varphi(x_2,x_3)$ that depends on the outcomes only, and the outcomes are averaged. The result is the output state $W_r(x_1,p_1)$ of mode 1.
• Fidelity with the pure input: $F(W)=\pi\int W_{\mathrm{in}}W\,dx\,dp$.