BasisState

formal source

  39/-! ## What Are Pointer States? -/
  40
  41/-- A basis state in Hilbert space. -/
  42structure BasisState (n : ℕ) where
  43  amplitudes : Fin n → ℂ
  44  normalized : ∑ i, ‖amplitudes i‖^2 = 1
  45
  46/-- A pointer state is one that survives decoherence. -/
  47structure PointerState (n : ℕ) extends BasisState n where
  48  /-- Stability under environment interaction -/
  49  stable : Bool := true
  50  /-- Minimum J-cost in local neighborhood -/
  51  cost_minimized : Bool := true
  52
  53/-! ## The Environment and Decoherence -/
  54
  55/-- An environment model - many degrees of freedom. -/
  56structure Environment where
  57  degrees_of_freedom : ℕ
  58  temperature : ℝ
  59  interaction_strength : ℝ
  60  temp_pos : temperature > 0
  61
  62/-- A typical macroscopic environment (room temperature, many particles). -/
  63def roomEnvironment : Environment := {
  64  degrees_of_freedom := 10^23,
  65  temperature := 300,
  66  interaction_strength := 0.1,
  67  temp_pos := by norm_num
  68}
  69
  70/-! ## Neutral Windows in J-Cost Landscape -/
  71
  72/-- A neutral window is a region where J-cost is locally flat/minimal.