theorem proved tactic proof high

`i_is_rotation`

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.

claimFor 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 in Recognition Science

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.

scope and limits

Does not prove i² = -1 (handled by a sibling theorem).
Does not treat rotations by angles other than π/2.
Does not connect the rotation to recognition cost or defect distance.
Does not claim uniqueness of i within the full forcing chain.

formal statement (Lean)

  75theorem i_is_rotation :
  76    ∀ z : ℂ, I * z = z * cexp (I * Real.pi / 2) := by

proof body

Tactic-mode proof.

  77  intro z
  78  have h : cexp (I * Real.pi / 2) = I := by
  79    rw [Complex.exp_mul_I, Complex.cos_pi_div_two, Complex.sin_pi_div_two]
  80    simp
  81  rw [h, mul_comm]
  82
  83/-- Two rotations by π/2 equals rotation by π. -/