`superposition`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.SchroedingerEquationFromRS
domain: Physics
line: 36 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.SchroedingerEquationFromRS on GitHub at line 36.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  33theorem stationary_state : Jcost 1 = 0 := Jcost_unit0
  34
  35/-- Superposition: J > 0. -/
  36theorem superposition {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  37    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  38
  39structure SchroedingerCert where
  40  five_systems : Fintype.card QMSystem = 5
  41  stationary : Jcost 1 = 0
  42  superposition_cost : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  43
  44def schroedingerCert : SchroedingerCert where
  45  five_systems := qmSystemCount
  46  stationary := stationary_state
  47  superposition_cost := superposition
  48
  49end IndisputableMonolith.Physics.SchroedingerEquationFromRS

papers checked against this theorem

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