pith. machine review for the scientific record. sign in
theorem proved tactic proof

entangled_higher_cost

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  57theorem entangled_higher_cost (N : ℕ) (hN : N > 1) (j_single α : ℝ) (hα : α > 0) :
  58    jcostEntangled N j_single α > jcostProduct N j_single := by

proof body

Tactic-mode proof.

  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². -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.