The symmetry condition that makes measured numbers real -- and hands you, free of charge, the whole machinery of outcomes and eigenstates.
Here is the problem. Quantum mechanics represents measurable quantities by operators, but operators are matrices of complex numbers, and laboratory dials read real. Which operators are legitimate observables?
The answer is a symmetry condition: the operator must equal its own conjugate transpose -- Hermitian. That single requirement buys everything a theory of measurement needs. The eigenvalues -- the possible outcomes -- are forced real. The eigenvectors -- the states giving each outcome with certainty -- form a complete orthogonal set. Measurement becomes sorting into perfectly distinguishable bins.
Drop the condition and all of it collapses: complex outcomes, non-orthogonal certainties, no consistent sorting. The reality of experimental numbers, traced back, is this one algebraic symmetry.
Everything measurable in the corpus is Hermitian -- observables, Hamiltonians, density operators -- and the spectral theorem that Hermiticity unlocks is used constantly. The most load-bearing instance: diagonalising a density operator before integrating against it, the step on which the trace-versus-norm bridge in the channel work stands.
One workmanlike convention worth knowing: the corpus states Hermiticity as a predicate on plain matrices rather than bundling it into a subtype. Statements stay close to the mathematics, proofs stay close to the library, and the finite-dimensional spectral facts consumed are proved, not assumed.
A matrix equal to its own conjugate transpose. Real eigenvalues; unitary diagonalisability with orthogonal eigenspaces; hence the functional calculus -- applying real functions to operators through their spectra -- that the corpus's entropy and channel chains consume throughout.
Charles Hermite (1822-1901) was born at Dieuze in Lorraine with a malformed right foot, and the Ecole Polytechnique -- having admitted him -- forced him out over the disability, ending the engineering career he had trained for. Mathematics got him instead. He eventually taught at the Polytechnique that had rejected him, at the Ecole Normale and at the Sorbonne; Poincare was his student.
His 1873 proof that e is transcendental was the first for any naturally occurring number, and his method handed Lindemann the transcendence of pi nine years later -- closing the squaring of the circle after two millennia. He never sought the second result himself, writing that he dared not attempt it: one of history's more consequential displays of mathematical modesty.
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.