The textbook's second rule -- how a state changes when measured -- is not a second rule here. It is what the record layer does.
pointer_luders_born_prepHere is the problem. Measure a quantum system and two things happen: an outcome shows up, and the state afterwards is different. Textbooks handle this with a separate postulate -- the update rule -- bolted on beside the equation of motion. Two rules, no explanation of why the second exists or when it applies.
There is also a subtlety inside the update rule itself, and it is Luders who caught it. When several distinct states share the same measured value -- a degenerate measurement -- the naive update (jump to the eigenstate) is wrong. The right update projects onto the whole block of states sharing the value, disturbing nothing within the block. Get this wrong and repeated measurements give inconsistent answers.
Von Neumann's original 1932 rule got the degenerate case wrong. Luders fixed it in 1951, and the fix went largely unremarked for years -- a correction to the foundations of measurement theory, published quietly and absorbed silently.
In CSD the update is not a postulate at all. Records and the state update live on the same pointer arena, produced by the same construction: the record selects which region the trajectory realises, the Born weights come out of the volumes, and the post- measurement state is the block projection. One mechanism, two textbook rules recovered as its two faces.
The corpus treats the degenerate case as the general one, not a footnote. That ordering is forced by physics: real detectors are almost always degenerate -- reporting which region a particle landed in without resolving states within the region. A companion result sharpens the point: no fixed ray-level calibration reproduces the update for all preparations, so the block form is not optional.
On the pointer arena, the record-conditioned marginal reproduces the Born weights of the preparation, and the post-measurement state is the Luders block projection. The conditioning carries a smallness condition that should travel with the statement: the outcome's weight must exceed the width of the corridor the smooth witness leaves unrecorded, so the result says nothing about outcomes weighted below it. Degenerate block measurements are the case treated; rank-one projective measurements are the specialisation where every block is a single ray.
Companions: a swap-based apparatus reproduces the Luders marginal exactly when calibrated, and -- the sharper negative -- no fixed ray-level calibration works for every preparation, so calibration must be context-dependent. That negative is what forces the block treatment.
Gerhart Luders (1920-1995) was born in Hamburg, trained in the Gottingen orbit, and held a chair at Gottingen from 1960. The update rule is from a 1951 paper correcting von Neumann -- a graduate student's observation, in effect, that the great man's measurement postulate mishandled repeated eigenvalues.
He is at least equally remembered for the CPT theorem, proved independently around 1954: the statement that charge conjugation, parity and time reversal, composed, is a symmetry of every local relativistic field theory. Two results, both structural, both about what quantum theories must do rather than what any particular one does.
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.