two_rotations
The product of two complex rotations by π/2 equals one rotation by π. Researchers grounding the imaginary unit in the eight-tick phase structure of Recognition Science cite this to link discrete ticks to continuous phase factors. The proof is a one-line wrapper that invokes the exponential addition law and then simplifies the combined exponent by ring normalization.
claim$e^{iπ/2} · e^{iπ/2} = e^{iπ}$
background
Recognition Science takes the tick as the fundamental time quantum, set to 1 in native units. The eight-tick phase assigns values kπ/4 for k in 0..7 and maps each to the unimodular complex number exp(i w). The local setting is MATH-001, whose module doc states that rotation by two ticks corresponds to multiplication by i while four ticks yield -1, so i × i equals rotation by π.
proof idea
The term proof first rewrites the product via the addition formula for the complex exponential, converting it to a single exp whose argument is the sum of the two π/2 phases. Ring normalization then collapses the coefficient of I from 1 to 2, producing the target phase π.
why it matters in Recognition Science
This step supplies the algebraic content of i² = -1 inside the eight-tick framework and directly supports the module goal of deriving the imaginary unit from phase rotations. It connects to the T7 eight-tick octave landmark and explains why complex phases appear in quantum mechanics. No downstream theorems are recorded yet, leaving the result as an isolated but foundational identity.
scope and limits
- Does not derive the eight-tick period from more primitive axioms.
- Does not compute the numerical value of π from tick counts.
- Does not address non-commutative or higher-dimensional phase structures.
formal statement (Lean)
84theorem two_rotations :
85 cexp (I * Real.pi / 2) * cexp (I * Real.pi / 2) = cexp (I * Real.pi) := by
proof body
Term-mode proof.
86 rw [← Complex.exp_add]
87 ring_nf
88
89/-- **THEOREM**: i² = -1 follows from 8-tick phase structure.
90
91 i = e^{iπ/2} (2 ticks from 1)
92 i² = e^{iπ} = -1 (4 ticks from 1) -/