positionPointer
plain-language theorem explainer
Position is instantiated as a pointer state because localized states minimize J-cost under local interactions. Researchers modeling decoherence and the quantum-to-classical transition would cite this construction when building the many-body J-cost argument. The definition is a direct record instantiation of the PointerState structure.
Claim. The position observable is a pointer state whose observable field is the string ``position'' and whose selection reason is ``Local interactions favor localized states''.
background
The module QF-011 derives classical emergence from many-body J-cost minimization: single-particle superpositions carry low J-cost while correlated many-body states scale as N squared or worse, so product states are selected for large N. PointerState is the structure that records which classical observables survive environmental interaction; in RS these are precisely the J-cost minima. The supplied definition populates that structure for the position observable.
proof idea
Direct record construction that supplies the two fields of the PointerState structure.
why it matters
This supplies one concrete instance inside the classical-emergence derivation of QF-011. It illustrates how the J-cost framework selects the position basis without invoking external measurement postulates. The module targets the paper proposition that classical behavior follows from many-body J-cost minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.