A quantum whole can be perfectly known while its parts are maximally unknown. Entropy is where that stops being a metaphor and becomes arithmetic.
vonNeumannEntropy_subadditiveHere is the problem. Entropy measures missing information, and for ordinary things it behaves sensibly: know everything about a machine and you know everything about its parts. Quantum mechanics breaks the sensible behaviour in a specific, quantifiable way.
Two entangled particles can be in a jointly definite state -- entropy zero, nothing left to learn about the pair -- while each particle alone is in the most uncertain state possible, maximum entropy. The information is not hiding in one particle or the other. It lives in the relationship, and no inspection of the parts separately can find it.
Von Neumann's entropy is the quantity that makes this precise, and the inequalities it obeys -- how the entropy of a whole constrains the entropies of its parts -- are the working arithmetic of quantum information. They are also, it turns out, most of thermodynamics.
The corpus uses entropy for two jobs, and they are different jobs. First: it measures the irreversibility created when a pure state is coarse-grained into a record. The substrate conserves entropy exactly; the record does not; the gap between those two statements is where the second law -- and arguably the arrow of time -- enters this programme.
Second: the inequalities are load-bearing machinery. Subadditivity is the specific step that turns an entropy statement into the Landauer heat bound; remove it and that derivation does not close. The corpus proves subadditivity at positive-definite marginal scope, and carries the much harder strong subadditivity separately, derived from an explicit data-processing premise -- a scope decision recorded in the ledger, not discovered by a reader.
For a bipartite density operator, the entropy of the whole is at most the sum of the entropies of the marginals. Proved here at positive-definite marginal scope -- for pure global states, that means full Schmidt rank. The standard equality condition, that the bound is attained exactly on product states, is stated in the module as the reason the inequality is not vacuous; it is not itself formalised, so do not cite it as proved.
Strong subadditivity, the three-party inequality of Lieb and Ruskai from which most structural results of quantum information follow, is not re-proved from scratch: it is derived from an explicit data-processing hypothesis, and the ledger says so.
John von Neumann (1903-1957), born Neumann Janos in Budapest to an ennobled banking family, did a chemistry degree in Zurich and a mathematics doctorate in Budapest more or less simultaneously. Berlin, Hamburg, then Princeton in 1930 and the Institute for Advanced Study at its founding. The entropy is in his 1932 book that gave quantum mechanics its Hilbert-space form -- fifteen years before Shannon.
The naming story is the good part. When Shannon later needed a name for his own uncertainty quantity, von Neumann reportedly told him: call it entropy. Two reasons -- your formula already exists in statistical mechanics under that name, and nobody knows what entropy really is, so in a debate you will always have the advantage. Shannon took the advice. The joke has been paying dividends ever since.
CsdLean4/Mathlib/QuantumInfo/Subadditivity.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.