Robertson uncertainty relation

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.

proved in corpus · proved here, no imported axiomsLean kahler_robertson_ontic_variance

In plain terms

Here 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.

In CSD

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.

Mathematically

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.

The name

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.

Module
CsdLean4/LF4/UncertaintyKahler.lean
Related
hermitian operator, pauli matrices, poisson bracket

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.

Privacy policy