pith. machine review for the scientific record. sign in
inductive definition def or abbrev high

QMSystem

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  26inductive QMSystem where
  27  | infiniteSquareWell | harmonicOscillator | hydrogenAtom | freeParticle | finiteSquareWell
  28  deriving DecidableEq, Repr, BEq, Fintype
  29

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.