entangled_higher_cost

formal source

  54  N * j_single + α * N * (N - 1) / 2
  55
  56/-- **THEOREM**: Entangled states have higher J-cost for large N. -/
  57theorem entangled_higher_cost (N : ℕ) (hN : N > 1) (j_single α : ℝ) (hα : α > 0) :
  58    jcostEntangled N j_single α > jcostProduct N j_single := by
  59  unfold jcostEntangled jcostProduct
  60  -- Need: N * j_single + α * N * (N - 1) / 2 > N * j_single
  61  -- Simplifies to: α * N * (N - 1) / 2 > 0
  62  have hN_pos : (N : ℝ) > 0 := Nat.cast_pos.mpr (by omega)
  63  have hN_m1_pos : (N : ℝ) - 1 > 0 := by
  64    have : N ≥ 2 := hN
  65    have h : (N : ℝ) ≥ 2 := Nat.cast_le.mpr this
  66    linarith
  67  have h_extra_pos : α * ↑N * (↑N - 1) / 2 > 0 := by positivity
  68  linarith
  69
  70/-- **THEOREM**: The cost difference scales as N². -/
  71theorem cost_difference_scales_quadratically (N : ℕ) (j_single α : ℝ) :
  72    jcostEntangled N j_single α - jcostProduct N j_single = α * N * (N - 1) / 2 := by
  73  unfold jcostEntangled jcostProduct
  74  ring
  75
  76/-! ## Pointer States -/
  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. -/