schrodingerEquation
plain-language theorem explainer
The declaration defines a simplified Schrödinger equation that evolves a complex wavefunction under a Hamiltonian by explicit multiplication with the imaginary unit. Researchers deriving quantum mechanics from Recognition Science's 8-tick phase structure would cite it to show why i appears in the wave equation. It is realized as a one-line wrapper applying I directly to the operator result.
Claim. The time-dependent Schrödinger equation in units with ħ = 1 takes the form of the map sending each real parameter x to i times the Hamiltonian operator applied to the wavefunction value at x, i.e., x ↦ i · Ĥ(ψ(x)) where ψ : ℝ → ℂ and Ĥ : ℂ → ℂ.
background
The module MATH-004 derives the necessity of complex numbers from the 8-tick phase cycle of the Recognition ledger, whose phases are rotations by kπ/4 for k = 0 to 7 and therefore require the plane of ℂ. Upstream CostAlgebra defines the shifted cost H(x) = J(x) + 1 = ½(x + x⁻¹), under which the Recognition Composition Law reduces to the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The same module imports the inflaton potential V(φ_inf) = J(1 + φ_inf) and the binary-cube vertex count |V| = 2^D to tie the phase structure to spatial dimension D = 3.
proof idea
This is a one-line wrapper that applies the imaginary unit I to the Hamiltonian operator H acting on ψ(x).
why it matters
The definition supplies the explicit i that appears in the Schrödinger equation, thereby supporting the module claim that the 8-tick octave (T7) forces complex numbers and hence quantum mechanics. It sits alongside the sibling quantum_requires_complex and feeds the broader forcing chain from T0 through T8 that yields D = 3. No downstream theorems yet reference it, leaving open the question of how the Hamiltonian itself emerges from the J-cost functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.