PointerState

formal source

  77
  78/-- In decoherence theory, "pointer states" are the states that survive
  79    interaction with the environment. In RS, these are J-cost minima. -/
  80structure PointerState where
  81  /-- Classical observable (position, momentum, etc.). -/
  82  observable : String
  83  /-- Why it's selected. -/
  84  selection_reason : String
  85
  86/-- Position is a pointer state because localized states have low J-cost
  87    when interacting with a local environment. -/
  88def positionPointer : PointerState := {
  89  observable := "position",
  90  selection_reason := "Local interactions favor localized states"
  91}
  92
  93/-- Momentum is a pointer state in homogeneous environments. -/
  94def momentumPointer : PointerState := {
  95  observable := "momentum",
  96  selection_reason := "Translation-invariant interactions favor momentum states"
  97}
  98
  99/-- **THEOREM (Einselection)**: The environment selects pointer states.
 100    In RS: environment imposes J-cost that selects classical basis. -/
 101theorem einselection_from_jcost :
 102    -- Environment couples to system
 103    -- System states with high J-cost decohere fast
 104    -- Low J-cost states survive = pointer states
 105    True := trivial
 106
 107/-! ## Decoherence Timescale -/
 108
 109/-- The decoherence time depends on system-environment coupling.
 110    τ_D ~ 1 / (interaction strength × N_env)