Partial trace

In plain terms

This is the formal-methods reader's problem more than the physicist's. Ignoring part of a quantum system, tracing out the environment and keeping a description of the subsystem, is the single most common operation in quantum information, and the operation that does it is called the partial trace. Ask what a library of formalised mathematics offers for it and, in the case of Mathlib, the community library for the Lean proof assistant, the answer at the level of matrices is nothing.

The corpus's staging tree, its collection of general-purpose results written for eventual contribution to Mathlib, fills the gap. It provides the partial trace over either factor of a composite system, together with the lemmas you actually need, which are linearity, preservation of the total trace, so probability is conserved, preservation of positivity, the fact that the reduced state of a density matrix is again a density matrix, and the defining identities that pair a joint operator against observables of one side only.

Nothing in it is specific to CSD. It's general infrastructure, built to be given away.

In CSD

The partial trace is load-bearing across the corpus. Reduced states in the decoherence and einselection tiers, the parts of the programme that describe how interaction with an environment singles out certain states as stable, marginals of the composite field arena, where local observations on entangled points are exactly expectations in the reduced state, and the subadditivity arguments of the entropy tier all consume it.

A small story of library hygiene attaches. The defining reduced-trace identities were originally proved in the entropy module, and when the work on entangled weights needed them without the rest of the entropy machinery they were moved to sit beside the definition, so the rule is that the defining property of an operation lives with the operation.

On the constraint surface the partial trace is the operation that turns the joint description into the system's own. A preparation of system and environment together is flowed, its density operator on the joint space is formed, and tracing out the environment gives the system's density operator after the interaction. That reduced operator is what a channel acts on, so the partial trace is the exact point at which the programme's ontic flows become the operational channels of quantum information.

Mathematically

partialTraceRight and partialTraceLeft on Matrix (n x m) (n x m), with bundled linearity, trace preservation, Kronecker reduction, the trace of the traced-out factor scaling the survivor, Hermiticity and positivity preservation via tensor witness vectors, and density-to-density.

The reduced-trace identities Tr(M (X (x) I)) = Tr(Tr_B M X) and its mirror are proved alongside, and all of it is foundational-triple-only.

Two spellings coexist, Matrix.traceRight and Matrix.traceLeft in Mathlib/LinearAlgebra/Matrix/PartialTrace.lean and the QuantumInfo pair above, and the Stinespring module uses the former. The reduced flowed barycentre is computed by barycenterMatrix_kronecker_of_ae (a product preparation has a Kronecker barycentre, almost everywhere in the representative) and traceRight_barycenter_flow (LF2/FlowChannel.lean).

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.
• 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.
• Entropy subadditivityThe information missing from a whole never exceeds the sum of what's missing from its parts, and that's von Neumann's subadditivity inequality, proved at the matrix level with the operator-logarithm step informal proofs usually wave through.
• Kronecker productTwo quantum systems become one by multiplying their descriptions rather than adding them, which is why quantum resources multiply where classical ones merely add.
• De-isolationNothing collapses, as a measured system stops being isolated, and measurement is what de-isolation dynamics looks like from inside.