theorem
proved
qmSystemCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.SchroedingerEquationFromRS on GitHub at line 30.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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