Quantum channel

In plain terms

Unitary evolution, the reversible evolution of the Schrodinger equation, is what happens to a perfectly isolated system, and nothing is perfectly isolated. Send a photon down a real optical cable and it attenuates, loses the coordination between the components of its state, and mixes with noise, and the general description of any such process, any physically realisable transformation of quantum states, is called a channel.

The structure theorem for channels says every one of them can be written as a family of simpler operators, each applied to the state in turn with the results summed. This is the Kraus form, and it comes with one completeness condition on the family that guarantees probabilities still add up to one afterwards.

The corpus formalises channels in exactly that form and then proves the certificates, so the total probability is preserved, positivity is preserved and no probability turns negative, and Choi's matrix criterion for complete positivity holds in both directions.

In CSD

Channels are the vocabulary of the programme's open-system and coarse-graining tiers. The dephasing and damping semigroups are families of channels indexed by time, the coarse-graining of the field arena that traces out modes is a channel built from an explicit isometry, a map that preserves lengths, and the error budget for a renormalisation step is stated as a distance between the outputs of two channels.

The layer is breadth on the operational stratum, formalised to the corpus's usual standard, so no property of a channel is used anywhere without a named theorem carrying it.

Since the constraint surface carries both the system and its environment, the channels the programme reasons about aren't introduced by hand. A volume-preserving flow on the surface that lifts a unitary on the joint state space acts on a preparation, and the density operator of the flowed preparation, seen from the system alone, is a channel applied to the density operator of the original preparation, so the channel is the environment's marginal of the flow. The measurement flow produces the de-isolation channel in this way, and the bit-flip errors of the three-qubit code are produced by a flow on the register together with a four-level environment. The corpus keeps two spellings of the notion, an indexed Kraus family in the operational layer and the staged Mathlib structure, and it proves them equivalent, with actions, dilations and compositions agreeing.

Mathematically

QuantumChannel is an indexed Kraus family with the completeness law summing adjoint- products to the identity, and apply is the Kraus sum.

The proved properties are trace preservation, PSD preservation, unitality criteria, and choiMatrix_posSemidef, the easy direction of Choi, with the converse in the companion module closing the equivalence. Composition and the dilation-side constructions live where their consumers need them.

The bridge channelEquiv (LF2/ChannelBridge.lean) is an equivalence between QuantumChannel and the staged Channel, with the action, the unitary channels, the Stinespring dilations and the composition Channel.comp (Mathlib/QuantumInfo/ChannelComp.lean) transported. For channels from flows, traceRight_barycenter_flow (LF2/FlowChannel.lean) states that for a flow lifting a unitary on system times environment, and a preparation that is a product with the environment ready, the reduced barycentre of the flowed preparation equals stinespringChannel applied to the system's barycentre, and stinespringChannelMixed covers a mixed environment through its spectral Kraus family. The instances are measurementFlow_traceRight_barycenter_unitSection (LF6/MeasurementFlowChannel.lean), bitFlipFlow_traceRight_barycenter and registerFlow_traceRight_barycenter (Empirical/CSD/QEC/).

Related entries

• Stinespring dilationEvery noisy quantum process is a reversible process on a larger system with part of that system ignored, and in CSD the larger system is the constraint surface itself, so every channel the programme uses is the environment's marginal of a volume- preserving flow.
• Choi's theoremA transformation of quantum states is physically allowed exactly when one matrix built from it passes a single positivity test, and CSD proves both directions, so whether a map is physical becomes a decidable question of linear algebra.
• 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.
• Holevo boundA quantum system can be prepared in infinitely many distinct ways, yet no reader can extract more classical information from it than from a classical system of the same size, and the measurement channel of CSD is proved to pass exactly one bit per qubit.
• Helstrom boundThe Helstrom bound says how well any measurement can tell two quantum states apart, and the answer is exactly the trace distance between them, attained by one specific test.