experimentalEvidence
plain-language theorem explainer
Experimental evidence for pointer states is compiled as a list of four laboratory domains: ion traps showing z-aligned decay, SQUIDs with classical flux outcomes, cavity QED yielding coherent states, and NMR with matching T2 times. A quantum theorist modeling open-system decoherence would cite it to anchor the neutral-window derivation in observed data. The definition is a direct enumeration of verified outcomes with no computation or lemmas.
Claim. The experimental evidence supporting pointer states consists of the verified cases: ion trap decoherence verifying exponential decay of off-diagonal terms, SQUID experiments showing flux superpositions decohere to classical flux, cavity QED where coherent states emerge as pointer states, and NMR relaxation where the $T_2$ time matches pointer state predictions.
background
Pointer states are the stable configurations preferred by decoherence, identified in the module as neutral windows in the J-cost landscape where J-cost is locally minimized. The J-cost itself is the non-negative cost of a recognition event, defined as Cost.Jcost e.state in ObserverForcing.cost and equivalently as the derived cost of a multiplicative recognizer comparator in MultiplicativeRecognizerL4.cost. Environment interactions drive systems toward these windows, producing the classical outcomes listed in the definition.
proof idea
This definition is a direct enumeration of experimental domains. It lists four cases with their verification outcomes: ion trap decoherence, SQUID experiments, cavity QED, and NMR relaxation. No lemmas or tactics are applied; the body simply records the observed pointer-state behavior in each setting.
why it matters
This definition supplies the empirical anchor for the pointer-state derivation in the QF-003 module, linking neutral windows in the J-cost landscape to laboratory results. It supports the Recognition Science claim that decoherence selects minimal-J-cost states, consistent with the phi-ladder calibration of costs from upstream structures such as LedgerFactorization.of and PhiForcingDerived.of. No downstream theorems reference it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.