There's a workable meaning of bigger for operators, and it brings a strange discovery, as taking square roots respects it while taking squares can break it.
Quantum information theory runs on inequalities, so this entropy is at most that one and this channel loses at least this much information. But the objects being compared are operators, matrices acting on states, rather than plain numbers, and it isn't obvious what it means to say one matrix is at most another.
The Loewner order answers as follows. A matrix is called positive semidefinite if it never produces a negative number, so whatever state you evaluate it in the expected value is zero or more, which is the same as saying that all its eigenvalues, the stretch factors along its special directions, are at least zero. One operator is at most another when their difference, the second minus the first, is positive semidefinite. Some pairs of operators can't be compared either way, so this is a partial order rather than a complete ranking, and that's fine.
The genuine surprise is which functions respect the order. Suppose one operator is below another, and apply the same function to both by applying it to each eigenvalue. Take square roots and the order is preserved, and take squares and the order can flip. Intuition trained on ordinary numbers, where squaring two positive numbers keeps them in order, fails at the second example, and half the classic blunders in operator inequalities are exactly this failure.
The entropy and channel results in CSD's machine-checked corpus are statements in this order. Data processing, the fact that no channel can increase the information a state carries, subadditivity, the fact that the entropy of a whole is at most the sum of the entropies of its parts, and the contraction of trace distance, the fact that a channel can't make two states easier to tell apart, all compare operators, and so do the operator-convexity results that support them.
The machinery is imported and not claimed. What the corpus adds is formal verification, which for this topic has unusual value, because intuition about numbers fails silently here, so this is exactly the terrain where an informal proof can be confidently wrong and where machine-checking pays for itself.
A is at most B iff B minus A is positive semidefinite. Operator monotone functions, those respecting the order under the functional calculus, are characterised by Loewner's theorem as precisely the functions that continue analytically to map the upper half-plane to itself, so square root and logarithm qualify and the square doesn't.
The corpus consumes the order throughout its entropy and channel chains.
Charles Loewner (1893-1968), born Karel Lowner near Prague, studied under Georg Pick at the German university there. His 1923 attack on the Bieberbach conjecture introduced an evolution equation that waited eighty years to become spectacularly famous, as the Loewner in Schramm-Loewner evolution, now central to two-dimensional statistical physics.
The operator-monotone characterisation dates from 1934. Five years later the Nazi occupation forced him out of Prague, and he restarted in America almost from zero, at Louisville, Syracuse, and finally Stanford from 1951, where he taught to the end. He left two results, each half a century ahead of its audience, and he had to rebuild his life in the middle.
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.
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.