Lindblad equation

The master equation of open quantum systems, formalised end to end: the flow of every Lindblad generator is completely positive -- literally, with the ancilla identification proved, not gestured at.

proved in corpus · proved here, no imported axiomsLean lindbladSemigroup_completelyPositive

In plain terms

Here is the problem. Real systems leak: they dephase, decay, decohere. The equation governing an open quantum system's density matrix is the Lindblad equation, and its defining virtue is supposed to be that it generates legitimate physics at every time -- probabilities stay probabilities, even when the system is entangled with a bystander.

That virtue -- complete positivity -- is precisely what is delicate to prove, because the flow is an exponential of a generator with competing parts. The corpus does it from first principles: split the generator into a drift that acts by conjugation and a jump part whose exponential is a positive series, reassemble by a Trotter product formula proved for the purpose, and then show the flow of the ancilla-amplified generator IS the identity-tensor-flow map, so amplified positivity is complete positivity in so many words.

A staple of every open-systems textbook, now with a kernel-checked proof.

In CSD

The open-system tier is where the programme prices imperfect isolation: the exhibited dephasing and amplitude-damping semigroups are Lindblad flows, and the general theorem certifies that every such flow -- for any Hermitian Hamiltonian and any jump operators -- is a legitimate quantum channel at every nonnegative time.

The supporting Banach-algebra Trotter formula was deliberately proved in Mathlib-upstreamable generality, and the label the corpus once carried -- that exponentiated positivity was out of reach -- was retired when the gate was re-checked and the route found to be entirely in-corpus.

Mathematically

lindbladSemigroup_completelyPositive: for Hermitian H, jump family L, t >= 0 and every finite ancilla, the identity-tensor amplification of the flow maps positive semidefinite matrices to positive semidefinite matrices. Route: the drift flow is conjugation by a matrix exponential; the jump exponential is a positive Kraus series with positivity closed under limits; the general Lie-Trotter formula assembles the flow; and the blockwise identification of the amplified generator's flow with id-tensor-Phi makes the amplified statement literally complete positivity.

The name

Goran Lindblad (1940-2022) was a Swedish mathematical physicist at the Royal Institute of Technology in Stockholm. His 1976 paper on generators of quantum dynamical semigroups gave the general form of the equation; Gorini, Kossakowski and Sudarshan published the finite-dimensional classification the same year, which is why careful writers say GKSL. By the standards of a result used daily across quantum optics and quantum information, its authors are remarkably rarely read.

Module
CsdLean4/LF6/LindbladPositivity.lean
Related
quantum channel, choi theorem, pointer basis, lie trotter formula

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy