`QMSystem`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.SchroedingerEquationFromRS on GitHub at line 26.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  23namespace IndisputableMonolith.Physics.SchroedingerEquationFromRS
  24open Cost
  25
  26inductive QMSystem where
  27  | infiniteSquareWell | harmonicOscillator | hydrogenAtom | freeParticle | finiteSquareWell
  28  deriving DecidableEq, Repr, BEq, Fintype
  29
  30theorem qmSystemCount : Fintype.card QMSystem = 5 := by decide
  31
  32/-- Stationary state: J = 0 (eigenstate = recognition equilibrium). -/
  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.