roots_form_group
plain-language theorem explainer
The eighth roots of unity close under multiplication to form a cyclic group of order 8. Researchers modeling discrete phase rotations in Recognition Science or quantum mechanics would reference this result to ground the appearance of the imaginary unit in an eight-tick structure. The proof reduces the product of two complex exponentials to a single exponential by applying the addition formula for the exponential function and simplifying the modular arithmetic on the indices using basic natural number identities.
Claim. Let $j,k$ range over integers $0$ to $7$. Let $r_j = e^{2π i j/8}$. Then $r_j · r_k = r_{(j+k) mod 8}$.
background
In Recognition Science the imaginary unit is generated by the eight-tick phase structure: each tick is the fundamental time quantum $τ_0 = 1$, rotation by two ticks corresponds to multiplication by $i$, and four ticks yields $-1$. The rootOfUnity map therefore sends each index in Fin 8 to the corresponding point on the unit circle in the complex plane. This theorem shows that these phase factors form a group under multiplication whose operation mirrors addition of the indices modulo 8.
proof idea
The tactic proof introduces the indices, unfolds rootOfUnity to a complex exponential, rewrites the product via Complex.exp_add, and reduces the summed index using Fin.val_add together with Nat.div_add_mod. It then applies add_comm and mul_add from ArithmeticFromLogic to rearrange the exponent, cancels the $2πi$ multiple with Complex.exp_int_mul_two_pi_mul_I, and finishes with ring and simp.
why it matters
The result completes the core step of MATH-001 by confirming that the discrete 8-tick rotations close into a group, thereby justifying the appearance of $i$ in the Schrödinger equation and in Euler’s formula. It aligns with the T7 eight-tick octave landmark and supplies the algebraic foundation for the sibling constructions of euler_identity and schrodinger_i_from_8tick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.