What 'bigger' means for operators -- and the strange discovery that taking squares breaks it while taking square roots does not.
Here is the problem. Quantum information runs on inequalities -- this entropy is at most that one, this channel loses at least this much -- but the objects being compared are operators, not numbers. What does A is at most B even mean for matrices?
The Loewner order answers: A is at most B when their difference B minus A is positive semidefinite -- when it never produces a negative number from any state. Some pairs are simply incomparable; it is a partial order, and that is fine.
The genuine surprise is which functions respect it. Send A and B, with A below B, through the square-root function: order preserved. Through the SQUARE: order can flip. Intuition trained on numbers fails at the second example, and half the classic blunders in operator inequalities are exactly this failure.
The corpus's entropy and channel results are statements IN this order -- data processing, subadditivity, trace-distance contraction all compare operators. So are the operator-convexity results that support them.
The machinery is imported, not claimed; what the corpus adds is formal verification, which for this topic has unusual value. Because naive number-intuition fails silently here, this is exactly the terrain where an informal proof can be confidently wrong -- and where machine-checking pays for itself.
A 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: precisely the functions analytically continuing to map the upper half-plane to itself. Square root and logarithm qualify; the square does not. 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 is from 1934. Five years later the Nazi occupation forced him out of Prague; he restarted in America almost from zero -- Louisville, Syracuse, finally Stanford from 1951, where he taught to the end. Two results, each a half-century ahead of its audience, from a man who 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.