rootOfUnity
The definition maps each k in 0 to 7 to the complex value exp(2 pi i k /8). Researchers deriving phase factors from discrete rotations in Recognition Science reference this when connecting eight-tick structure to complex exponentials. It is realized by direct application of the complex exponential to the scaled angle.
claimFor each integer $k$ modulo 8, define the eighth root of unity by $e^{2 pi i k / 8}$.
background
The module derives the imaginary unit from the eight-tick phase rotation in Recognition Science. Rotation by two ticks corresponds to multiplication by i and by four ticks to -1, so that i squared equals -1. This supplies the explicit complex values for the eight discrete phase steps as the standard eighth roots of unity.
proof idea
The definition is a direct one-line assignment that applies the complex exponential to I times the angle 2 pi k /8.
why it matters in Recognition Science
This definition realizes the 8-tick phases that generate the imaginary unit in the MATH-001 target. It is used by the theorem proving the roots form a cyclic group under multiplication. The construction links the eight-tick octave directly to the complex phases appearing in quantum wave equations.
scope and limits
- Does not prove algebraic closure or group properties of the roots.
- Does not derive i from any forcing chain step.
- Does not connect the phases to physical constants or mass formulas.
- Does not treat roots of unity of order other than 8.
formal statement (Lean)
191noncomputable def rootOfUnity (k : Fin 8) : ℂ :=
proof body
Definition body.
192 cexp (I * (2 * Real.pi * k / 8))
193
194/-- The roots form a group. -/