The uncertainty principle, with its ontic half computed: the variances in Robertson's inequality are honest integrals over the arena, not just Hilbert-space expectations.
kahler_robertson_ontic_varianceHere is the problem. The uncertainty principle is quantum mechanics' most famous export and its most misquoted. The precise statement is Robertson's: for any two observables, the product of their spreads in a given state is bounded below by half the expectation of their commutator. No measurement-disturbance story required -- it is a fact about statistics.
The corpus proves Robertson's inequality and then does the part that belongs to the arena picture: it identifies each variance as an integral over the ontic space, so the spread the inequality bounds is the spread of a genuinely distributed quantity, not an abstract expectation.
Two concrete witnesses pin it down, including a case where the bound is saturated -- the inequality is tight, and the formalisation exhibits the tightness.
This is the observable-correspondence tier: Hermitian observables acquire ontic representatives whose Lebesgue integrals reproduce Hilbert-space expectations, via a genuine spectral expansion on one side and the fibre partition on the other. Robertson's inequality then holds with the left-hand side read ontically -- the uncertainty bound as a statement about spreads of arena quantities.
The witnesses are Pauli pairs on explicit states: saturation at the qubit, and the parametric axis version quantified over unit directions.
kahler_robertson_ontic_variance: the product of ontic-side variances dominates the commutator bound, with the variance identification running through the spectral-region integral identities -- the ontic centred second moment equals the Hilbert-space variance. Companions: pauli_xy_robertson_saturation with both sides equal to one, and the parametric pauliDot version over arbitrary axes.
Howard Percy Robertson (1903-1961) was an American mathematical physicist at Caltech and Princeton, known jointly for the Robertson-Walker metric of cosmology and the 1929 general uncertainty relation -- a one-page Physical Review note sharpening Heisenberg's heuristic into an inequality for arbitrary observable pairs, later refined by Schrodinger with the covariance term.
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.