PointerState
plain-language theorem explainer
PointerState encodes a normalized basis vector in n-dimensional Hilbert space that remains stable under environmental coupling and sits at a local J-cost minimum. Decoherence theorists and quantum information researchers cite it when mapping Recognition Science's neutral windows onto the pointer basis selected by einselection. The definition is a direct structure extension of BasisState that adds two boolean flags defaulting to true, with no computational content beyond the field declarations.
Claim. A pointer state in an $n$-dimensional Hilbert space is a normalized vector with amplitudes in Fin $n$ to $ℂ$ satisfying $∑_i ‖amplitudes i‖² = 1$, together with the properties that it is stable under environment interaction and that its J-cost is minimized in the local neighborhood.
background
BasisState supplies the underlying normalized vector in $ℂ^n$. J-cost is the recognition cost of a state, defined in ObserverForcing.cost as Cost.Jcost e.state and derived from the multiplicative recognizer comparator in MultiplicativeRecognizerL4.cost. The module setting is QF-003, which identifies pointer states with neutral windows in the J-cost landscape: configurations where superpositions acquire high entanglement cost while certain basis states remain at local minima. Upstream LedgerFactorization.of and PhiForcingDerived.of calibrate the J function on positive ratios, while NucleosynthesisTiers.of and CPM2D.model supply the discrete tier and fluid-model context in which these costs are evaluated.
proof idea
This is a structure definition extending BasisState with two boolean fields defaulting to true. No lemmas are applied; the declaration simply records the stability and cost_minimized predicates as part of the data type.
why it matters
The structure supplies the RS-native carrier for pointer states that ClassicalEmergence instantiates in positionPointer and momentumPointer. Those downstream definitions cite the J-cost minimum property to recover einselection: local interactions favor localized states while translation-invariant ones favor momentum states. It directly implements the MODULE_DOC claim that pointer states are the stable states preferred by decoherence, closing the link from RecognitionLatticeFromRecognizer.neighborhood to the emergence of classical observables inside the eight-tick octave and phi-ladder framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.