QMSystem
plain-language theorem explainer
QMSystem enumerates the five canonical quantum systems that realize configuration dimension D equals 5 in the Recognition Science derivation of the Schrödinger equation. Researchers connecting RS cost functions to standard QM would cite this enumeration when counting systems or certifying stationary-state equilibria. The declaration is a bare inductive type whose constructors are listed explicitly and whose standard typeclass instances are derived automatically with no proof body.
Claim. The type of canonical quantum mechanical systems is generated by the five constructors: infinite square well, harmonic oscillator, hydrogen atom, free particle, and finite square well.
background
In the Recognition Science setting the wave function ψ is interpreted as a recognition amplitude whose squared modulus, after normalization, enters the J-cost function J(|ψ|²). Stationary states are defined to be the J-cost minima (eigenstates) while superpositions carry positive J-cost. The module states that the time-dependent Schrödinger equation iℏ ∂ψ/∂t = Ĥψ describes recognition-state evolution and that the five listed systems together realize configDim D = 5.
proof idea
Direct inductive definition; the five constructors are enumerated explicitly and the deriving clause automatically supplies DecidableEq, Repr, BEq and Fintype instances. No lemmas, tactics or reduction steps are applied.
why it matters
The enumeration supplies the finite set whose cardinality is proved equal to 5 by the downstream theorem qmSystemCount; that cardinality populates the five_systems field of SchroedingerCert. It thereby anchors the configDim D = 5 step in the RS-to-QM bridge, where stationary states map to J-cost zero equilibria and superpositions map to positive J-cost uncertainty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.