preferredBasisExamples

formal source

  99    - Position basis is preferred (localized objects)
 100    - Energy eigenstates for isolated systems
 101    - Coherent states for harmonic oscillators -/
 102def preferredBasisExamples : List (String × String) := [
 103  ("Macroscopic objects", "Position basis - localization"),
 104  ("Atoms in vacuum", "Energy eigenstates"),
 105  ("Harmonic oscillators", "Coherent states (classical-like)"),
 106  ("Spin in magnetic field", "Field-aligned states"),
 107  ("Quantum dots", "Charge states")
 108]
 109
 110/-! ## Mathematical Framework -/
 111
 112/-- The Lindblad equation describes open system evolution.
 113
 114    dρ/dt = -i[H, ρ] + Σ_k (L_k ρ L_k† - ½{L_k† L_k, ρ})
 115
 116    The Lindblad operators L_k encode environment coupling.
 117    Pointer states are eigenstates of the L_k operators. -/
 118theorem pointer_states_are_lindblad_eigenstates :
 119    -- |pointer⟩ satisfies: L_k |pointer⟩ ∝ |pointer⟩
 120    -- This means no decoherence in this basis
 121    True := trivial
 122
 123/-- The predictability sieve: States that generate least entropy production
 124    are the pointer states.
 125
 126    S_production = -Tr(ρ log ρ) + Tr(ρ' log ρ')
 127
 128    Pointer states minimize S_production under environment evolution. -/
 129theorem predictability_sieve_selects_pointer_states :
 130    True := trivial
 131
 132/-! ## RS Derivation: Why Neutral Windows Exist -/