Stinespring dilation

In plain terms

The basic evolution of quantum mechanics is reversible, so nothing is lost and running it backwards recovers the starting state exactly. Real processes aren't like that, as a qubit stored in a device gradually loses its coherence, a photon in a fibre is sometimes absorbed, and a measurement leaves the system changed in a way that can't be undone. The general description of such a process is a channel, a rule that turns states into states while respecting probabilities, and channels can lose information.

Stinespring's theorem reconciles the two pictures. Any channel, however lossy, is a reversible evolution of the system together with an environment, followed by ignoring the environment, where ignoring means averaging over everything the environment could be doing, an operation called the partial trace. The information isn't destroyed, as it has moved into correlations with the environment, where a description of the system alone can't see it. A bit flip that happens with some probability, for instance, is a reversible interaction with a single environment qubit that records whether the flip occurred, seen from the side that doesn't read that record.

In CSD

The theorem is the hinge between the programme's ontic and operational layers. The constraint surface carries system and environment together, and its dynamics is a volume-preserving flow that lifts a reversible evolution of the joint state space. The corpus proves that when such a flow acts on a preparation whose environment starts in a ready state, the density operator of the flowed preparation, seen from the system alone, is a channel applied to the density operator of the original preparation, and it identifies which channel, the one Stinespring's construction assigns to the joint evolution and the ready state. So the channels of quantum information aren't introduced into the programme, as they're what its flows look like from inside. The measurement flow yields the de-isolation channel in this way, and the bit-flip errors of the three-qubit code arise from a flow on the register with a four-level environment. A mixed environment is covered as well, through the spectral decomposition of its density operator.

Mathematically

Channel.ofIsometry builds the channel Tr_env(V rho V^H) from an isometry V into system times environment, and apply_eq_traceRight_stinespring together with stinespringIsom_isom shows every Kraus channel arises this way, with the Kraus operators as the environment blocks of V. stinespringChannel U hU e_0 (LF2/FlowChannel.lean) is the channel of a joint unitary with a ready environment, and traceRight_barycenter_flow states that for a flow lifting U in the projector sense (IsUnitaryLift) and a preparation that is a product with the environment ready, almost everywhere in the representative, the reduced barycentre of the flowed preparation is that channel applied to the system's barycentre. isUnitaryLift_unitSection removes the section hypothesis for projective actions, stinespringChannelMixed handles a mixed environment, and channelEquiv (LF2/ChannelBridge.lean) transports the construction between the corpus's two channel structures.

The name

W. Forrest Stinespring (1929-2012) taught at the University of Illinois at Chicago for most of his career. The dilation theorem is in a short 1955 paper in the Proceedings of the American Mathematical Society, written in the language of positive maps on operator algebras and generalising Naimark's dilation of a positive operator measure. Its reading as the statement that every quantum channel is a unitary on a larger space, with the environment traced away, came with Kraus's work on operator-sum representations in the 1970s and 1980s, long after the mathematics was settled.

Related entries

• Quantum channelThe most general thing that can happen to a quantum state is captured in CSD as a concrete structure, a family of operators with one completeness law, and every certificate of its physicality is proved rather than assumed.
• Naimark dilationEvery noisy, imperfect measurement made in a real laboratory is an ideal textbook measurement carried out on a larger system, and that single fact is what lets CSD's derivation of the Born weights cover actual experiments rather than idealised ones.
• Partial traceMathlib has no partial trace for matrices, so the corpus built one, the staple operation of quantum information, with its working properties proved and staged for contribution upstream.
• De-isolationNothing collapses, as a measured system stops being isolated, and measurement is what de-isolation dynamics looks like from inside.
• Measurement flowA deterministic, volume-preserving flow carries out a measurement, and the volumes of its pointer blocks are the Born weights, for every preparation.