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.
lindbladSemigroup_completelyPositiveHere 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.
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.
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.
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.
CsdLean4/LF6/LindbladPositivity.leanSource 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.
Google Analytics counts visits to this page, which stores cookies in your browser. They record how the page was reached, not who you are, and nothing is passed on. Blocking cookies for this site breaks nothing here. Details.