schrodinger_i_from_8tick
plain-language theorem explainer
The theorem identifies the imaginary unit in the Schrödinger time-evolution formula as the generator arising from two ticks of the 8-tick phase cycle. Quantum theorists working inside the Recognition Science derivation would cite it to ground the appearance of i in unitary dynamics. The term proof is a direct witness construction that equates I to the two-tick phase via the tick2_is_i identification.
Claim. Suppose a map ψ : ℝ → ℂ satisfies ψ(t) = exp(i ⋅ (−H(ψ(t)) ⋅ t / ℏ)) for all t, where H : ℂ → ℂ is a Hamiltonian and ℏ a real constant. Then the phase generator equals i and equals the 8-tick phase evaluated at two ticks.
background
The module derives the imaginary unit from the 8-tick phase structure of Recognition Science. The phase function returns kπ/4 for k in Fin 8, so two ticks yield π/2. The fundamental tick is the RS time quantum normalized to 1. The Schrödinger evolution form is presented as the integrated solution that accumulates phase while preserving probability. Upstream lemmas supply the cost reparametrization H(x) = J(x) + 1 and the eight-tick phase definition, though the present proof only invokes the sibling tick2_is_i.
proof idea
The term proof opens the universal quantifiers, supplies I as the witness for the existential, splits the conjunction, closes the first conjunct by reflexivity, and finishes the second by symmetry of tick2_is_i.
why it matters
The result places the i of the Schrödinger equation inside the 8-tick octave (T7) of the forcing chain, showing that unitary phase evolution is generated by the same rotation that yields i² = −1. It feeds the subsequent Euler-identity derivations listed among the module siblings. The declaration thereby closes one link between the Recognition Composition Law and the appearance of complex structure in quantum dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.