Pointer basis

The apparatus does not measure what you ask it to. It measures what it can keep -- and what it can keep is decided by the interaction, not the experimenter.

proved in corpus · proved here, no imported axiomsLean einselectionN

In plain terms

Here is the problem. A measuring device is supposed to end up in one of several stable readings. But quantum mechanics happily writes down superpositions of pointer readings, and nobody has ever seen one. Why do pointers settle into some states and not others?

The standard answer, which CSD adopts, is einselection: the environment constantly interacts with the apparatus, and only certain states survive that interaction unscrambled. Those survivors are the pointer basis. A pointer position is robust because bumping into air molecules does not change it; a superposition of two positions is fragile because the first bump marks which.

The pointer basis is thus selected by what the interaction commutes with -- and since 2026 that selection is a theorem here, not a slogan: an observable survives the interaction at every time exactly when it commutes with it. What remains owed sits one level up -- which interaction a given apparatus realises is an input, and deriving it from the arena's own dynamics is open. The corpus says so where it says it.

In CSD

In the record layer the pointer basis is what makes a record a record: a stable, re-readable configuration the de-isolation dynamics writes and the environment does not erase. Be precise about what is proved. At general N the dephasing channel is DEFINED as the map sending a density matrix to its diagonal, so the statement that it kills coherences and preserves populations is a definitional unfolding, and the pointer basis is the computational basis by construction. The corpus flags this in the theorem's own docstring rather than leaving it to be discovered.

The content near it is real but narrower: the channel genuinely acts on a coherent state, the degenerate boundary is handled rather than waved at, and at the qubit the continuous-time law is exact. The commutation criterion itself is now a characterisation (PointerCommutation.lean, 2026): the pointer observables of a supplied interaction are exactly the commuting ones -- constants of the interaction motion, populations conserved in every state, a non-commuting projection provably disturbed. The ontic origin -- einselection from the arena's dynamics rather than from a supplied interaction -- is explicitly gated to a later tier.

The two-level reading applies here too: the pointer basis is a fact about the dynamics (ontic side); which pointer reading obtains for a given run is the record, selected by the trajectory.

Mathematically

einselectionN: the general-N dephasing channel zeroes off-diagonal terms in the pointer basis and preserves the diagonal populations. Stated alone this is definitional -- the channel is diagonal(rho i i), so "off-diagonal of a diagonal is zero" -- and the docstring says so. The content sits in the companions: that the channel acts non-trivially on a coherent state, that it restricts to the derived qubit reduction, and that at equal populations it degenerates to a multiple of the identity, invariant under any unitary conjugation, so no basis is preferred.

The genuinely dynamical statement is the qubit dephasing semigroup, where the off-diagonal coherence decays exactly as exp(-gamma t) with populations conserved and the limit at large t proved; amplitude damping is its companion. Both are two-level. At general N the criterion is characterised: pointer_invariant_iff_commute proves an observable is a constant of the interaction flow at every time iff it commutes with the Hermitian generator, with the disturbance of any non-commuting observable proved alongside. The interaction is the input; einselection from Sigma-dynamics is gated to the entangled tier.

Module
CsdLean4/Empirical/CSD/Einselection.lean
Related
de isolation, record layer, collapse, von neumann entropy

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