Naimark dilation

Every messy real-world measurement is a clean textbook measurement in a bigger room. That one fact is why the Born derivation covers actual experiments.

proved in corpus · proved here, no imported axiomsLean povm_born_eq_dilated_volume_uncond

In plain terms

Here is the problem. Textbook measurements are clean: mutually exclusive outcomes, sharp boundaries, one projector each. Real detectors are not like that. They are noisy, they blur neighbouring outcomes, they sometimes have more outcomes than the system has states. The general gadget describing them -- the POVM -- looks like a genuinely different, worse-behaved kind of object.

Naimark's theorem says the mess is an illusion of perspective. Any generalised measurement, however noisy, is an ordinary sharp measurement performed on the system plus an extra piece of apparatus. Enlarge the room and the complicated thing becomes the simple thing.

So there is no separate theory of realistic measurements. There is one theory, viewed sometimes through a keyhole.

In CSD

Without this, CSD's Born derivation would cover only idealised measurements -- a serious hole for a programme claiming to be about physics rather than textbooks, since essentially every real experiment is a POVM. With it, the volume argument transfers: dilate to the big room, run the same volume-ratio derivation there, pull the answer back. The generalised case closes by transfer, not by a second derivation.

The corpus does this constructively and then spends it: SIC measurements, mutually unbiased bases, trine measurements, unambiguous state discrimination, weak measurements -- each built through the canonical dilation, each inheriting the volume statement for free. The POVM chapter of the reconstruction is recorded as closed on exactly this mechanism.

Mathematically

For a POVM with a Naimark dilation, the Born weight of an effect equals the Fubini- Study volume of the corresponding outcome region in the dilated space, and the frequency statement transfers. Unconditional -- no genericity hypothesis.

The dilation is constructed, not assumed: from the effect square roots, canonically, so existence comes with an explicit witness. Instances in the corpus then inherit the theorem rather than re-proving it.

The name

Mark Naimark (1909-1978) was born in Odessa, the son of an artist, and worked in Moscow at the Steklov Institute, teaching at the Moscow Institute of Physics and Technology. The dilation theorem is from 1940 -- with close cousins by Stinespring and Sz.-Nagy forming a little family of extension theorems discovered across a war-divided decade.

His best-known work is the 1943 Gelfand-Naimark theorem characterising C-star algebras, written with Israel Gelfand, whose Moscow seminar was one of the most productive mathematical institutions of the century -- a weekly event that ran for fifty years and treated functional analysis as a contact sport.

Module
CsdLean4/LF4/BornRegionUncond.lean
Related
born weight, luders rule
Referenced
Wikipedia

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