i_is_rotation
plain-language theorem explainer
Multiplication by the imaginary unit on any complex number equals multiplication by exp(i π/2), which rotates the argument by π/2 or two ticks in the 8-tick phase structure. Researchers deriving the Schrödinger equation or Euler formula from Recognition Science phase rotations would cite this to justify i in wave mechanics. The proof is a short tactic sequence that reduces the exponential via trigonometric identities at π/2 then applies commutativity.
Claim. For every complex number $z$, multiplication by the imaginary unit $i$ satisfies $i z = z e^{i π / 2}$.
background
Recognition Science obtains the imaginary unit from the 8-tick phase structure in which each tick is a π/4 rotation. Rotation by two ticks (π/2) corresponds to multiplication by i and by four ticks (π) to multiplication by -1, so that i² = -1 follows by composition. The module MATH-001 targets this derivation to explain why complex numbers appear in quantum mechanics and why the Schrödinger equation contains i.
proof idea
The tactic proof introduces an arbitrary z : ℂ. It proves exp(I π / 2) = I by rewriting the complex exponential, inserting the known values cos(π/2) = 0 and sin(π/2) = 1, and simplifying. The final step substitutes the equality and rewrites using commutativity of multiplication.
why it matters
The result anchors the generator of 8-tick phase rotations (T7) and supplies the algebraic step needed for downstream claims such as the Schrödinger equation containing i and Euler's identity from the eight-tick octave. It directly addresses the module question of why imaginary numbers are required for phase in Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.