`cost_difference_scales_quadratically`

proved

show as: view math explainer →

module: IndisputableMonolith.Quantum.ClassicalEmergence
domain: Quantum
line: 71 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Quantum.ClassicalEmergence on GitHub at line 71.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  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. -/
  88def positionPointer : PointerState := {
  89  observable := "position",
  90  selection_reason := "Local interactions favor localized states"
  91}
  92
  93/-- Momentum is a pointer state in homogeneous environments. -/
  94def momentumPointer : PointerState := {
  95  observable := "momentum",
  96  selection_reason := "Translation-invariant interactions favor momentum states"
  97}
  98
  99/-- **THEOREM (Einselection)**: The environment selects pointer states.
 100    In RS: environment imposes J-cost that selects classical basis. -/
 101theorem einselection_from_jcost :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.