Motivation
The science of quantum information has arisen over the last two decades centered on the manipulation of individual quanta of information, known as quantum bits or qubits. Quantum computers, quantum cryptography and quantum teleportation are among the most celebrated ideas that have emerged from this new field. It was realized later on that using continuous-variable quantum information carriers, instead of qubits, constitutes an extremely powerful alternative approach to quantum information processing. This review focuses on continuous-variable quantum information processes that rely on any combination of Gaussian states, Gaussian operations, and Gaussian measurements. Interestingly, such a restriction to the Gaussian realm comes with various benefits, since on the theoretical side, simple analytical tools are available and, on the experimental side, optical components effecting Gaussian processes are readily available in the laboratory. Yet, Gaussian quantum information processing opens the way to a wide variety of tasks and applications, including quantum communication, quantum cryptography, quantum computation, quantum teleportation, and quantum state and channel discrimination. This review reports on the state of the art in this field, ranging from the basic theoretical tools and landmark experimental realizations to the most recent successful developments.
This mission is the statement-level formalization of Gaussian Quantum Information (arXiv:1110.3234v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Coherent-state moments, completeness, and exact overlap (§II.B.2 Eqs.(28)–(30): coherent state moments and overlap, 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.
Deferred results
24 results of the paper are not stated yet, because the library lacks an interface they need:
- §II.A.1, Eqs.(19)–(20): Gaussian states are completely characterized by first and second moments: Concrete multimode Weyl operators, mixed-state moment domain, and Gaussian density/Wigner representation (hard)
- §II.A.1 Eqs.(17)–(18): uncertainty and strict covariance positivity: Actual multimode mixed-state quadrature first and symmetrized second moments with their finite form domain (hard)
- §II.A.2 Eqs.(23)–(25): affine symplectic action: Concrete canonical Weyl representation and its affine symplectic unitary implementers (hard)
- §II.B.1 Eqs.(26)–(27): fixed-energy entropy maximizer: Unique entropy-maximizing thermal density, its Gaussian characteristic function, and mixed-state moments (hard)
- §II.B.5 Eq.(35): all one-mode Gaussian states: Actual displaced rotated squeezed thermal densities and Gaussian moment identification (hard)
- §II.B.7: EPR states purify thermal states: Actual two-mode Gaussian pure density, partial trace and EPR observable moments in the Eq.(42) convention (hard)
- §II.C.1 Eqs.(46)–(47): spectral entropy of Gaussian density operators: Identification of actual Gaussian density operators with their Williamson spectrum (hard)
- §II.C.1 Eqs.(48)–(49): operator thermal decomposition: Gaussian density thermal tensor product and concrete Weyl/metaplectic conjugation (hard)
- §II.C.1 Eq.(50): actual Gaussian purification: Actual Gaussian 2N-mode pure state with N-mode partial trace (hard)
- §II.C.2 Eqs.(51)–(52): Euler/Bloch–Messiah decomposition: Metaplectic operator representation and tensor squeezing/passive-unitary decomposition (hard)
- §II.E.3 Eqs.(64)–(65): Gaussian conditional covariance: Continuous homodyne and heterodyne instruments and almost-everywhere conditional normal states (hard)
- §III.A.2.a Eqs.(72)–(78): Gaussian power overlap: Actual Gaussian density powers and trace pairing with their physical moment/Williamson data (hard)
- §III.A.3 Eq.(80): one-mode Gaussian fidelity: Squared Uhlmann fidelity of actual Gaussian normal densities and their observable moments (hard)
- §IV.A Eqs.(100)–(101): teleportation with Gaussian resources: Unity-gain bosonic Bell instrument, conditional feedforward, and outcome-averaged fidelity (hard)
- §IV.B Eqs.(104)–(106): Gaussian cloner and anticlone: Actual three-mode symplectic cloner channel and its single-mode reduced densities (hard)
- §V.A Eqs.(108)–(110): Gaussian channel action and CP: Full trace-class CPTP Gaussian channel, Weyl dual law, and mixed-state moment action (hard)
- §V.A: Gaussian dilation with at most 2N environmental modes: Actual full-input Gaussian unitary Stinespring dilation with at most 2N pure environmental modes (hard)
- §II.C.1: erroneous Hermiticity/singular-value recipe: Consistent source statement with a specified normalization and approximation/domain where applicable (source-ambiguity)
- §II.B.7 Eqs.(39)–(42): incompatible EPR parameter/sign formulas: Consistent source statement with a specified normalization and approximation/domain where applicable (source-ambiguity)
- §III.B.3 Eq.(97): inconsistent homodyne scale: Consistent source statement with a specified normalization and approximation/domain where applicable (source-ambiguity)
- §V.B Eqs.(111)–(118), Table I: one-mode Gaussian canonical classification: Input/output Gaussian-unitary equivalence of actual one-mode channels and canonical dilations (hard)
- §VI.B.5.a Eqs.(141)–(142): covariance/noise mismatch: Consistent source statement with a specified normalization and approximation/domain where applicable (source-ambiguity)
- §VII.D Eqs.(174)–(176): Gaussian distortion sign/domain: Consistent source statement with a specified normalization and approximation/domain where applicable (source-ambiguity)
- §VII.F.1 Eqs.(179)–(181): unquantified approximate cubic state: Consistent source statement with a specified normalization and approximation/domain where applicable (source-ambiguity)
Selected references