qmSystemCount
plain-language theorem explainer
The theorem fixes the number of canonical quantum systems at exactly five by computing the cardinality of the QMSystem inductive type. Researchers deriving the Schrödinger equation from recognition costs cite this to set configDim D = 5 before enumerating stationary states. The proof is a one-line decide tactic that evaluates the Fintype instance on the five-constructor inductive definition.
Claim. The finite type of quantum mechanical systems has cardinality five: $|QMSystem| = 5$, where the systems are the infinite square well, harmonic oscillator, hydrogen atom, free particle, and finite square well.
background
The module identifies the wave function with recognition amplitude and the Hamiltonian with J-cost, so that the time-dependent Schrödinger equation governs recognition-state evolution. QMSystem is the inductive type whose five constructors list the standard solvable models; it derives DecidableEq, Repr, BEq, and Fintype. The upstream equilibrium theorem states that Jcost 1 = 0, confirming that stationary states are recognition equilibria with zero cost.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the expression Fintype.card QMSystem, which Lean evaluates from the inductive definition and its derived Fintype instance.
why it matters
The result supplies the five_systems field of schroedingerCert, which certifies the full Schrödinger derivation in the module. It matches the module statement that five canonical systems equal configDim D = 5 and sits inside the Recognition Science chain that forces D = 3 spatial dimensions from the eight-tick octave. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.