stationary_state
plain-language theorem explainer
The stationary state theorem shows that the recognition cost vanishes at the unit state, confirming the equilibrium for eigenstates in the RS quantum mechanics derivation. Workers on the Schrödinger equation from recognition principles cite this to anchor the zero-cost condition. The proof is a one-line term application of the Jcost unit lemma.
Claim. $J(1) = 0$, where $J(x) = (x-1)^2 / (2x)$ is the recognition cost function.
background
The module derives the Schrödinger equation from Recognition Science by treating the wave function ψ as a recognition amplitude whose squared modulus determines the quantum cost via J. Stationary states correspond to minima of this cost, specifically J = 0 at equilibrium. The Jcost function is defined in the Cost module as J(x) = (x-1)²/(2x), and the upstream result Jcost_unit0 establishes its value at x = 1. This provides the mathematical content for the stationary state condition stated in the module documentation. The local setting identifies five canonical systems (infinite square well, harmonic oscillator, hydrogen atom, free particle, finite square well) as having configDim D = 5, with stationary states as J-cost minima.
proof idea
The proof applies the Jcost_unit0 lemma directly as a term, which itself simplifies the Jcost definition to zero at argument 1.
why it matters
This theorem populates the stationary field of the schroedingerCert definition, which assembles the certification for the five quantum systems. It implements the module's key point that stationary states achieve J = 0, the recognition equilibrium. In the RS framework it connects to the J-uniqueness property and precedes the treatment of superpositions with positive cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.