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

cost_difference_scales_quadratically

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)

  71theorem cost_difference_scales_quadratically (N : ℕ) (j_single α : ℝ) :
  72    jcostEntangled N j_single α - jcostProduct N j_single = α * N * (N - 1) / 2 := by

proof body

Term-mode proof.

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

depends on (5)

Lean names referenced from this declaration's body.