jcostProduct

formal source

  45/-! ## The Scaling Argument -/
  46
  47/-- J-cost for a product state of N particles. -/
  48noncomputable def jcostProduct (N : ℕ) (j_single : ℝ) : ℝ :=
  49  N * j_single
  50
  51/-- J-cost for a fully entangled state of N particles.
  52    Entanglement adds cross-terms that scale quadratically. -/
  53noncomputable def jcostEntangled (N : ℕ) (j_single : ℝ) (α : ℝ) : ℝ :=
  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