omega_pow_eight
plain-language theorem explainer
The eight-tick phase factor satisfies ω⁸ = 1, so the discrete recognition cycle on ℤ/8ℤ closes. Anyone citing the finite Heisenberg–Weyl (shift/clock) presentation of occupation vs cost-rate needs this identity for the wraparound slot. The proof unfolds ω as a complex exponential, multiplies the exponent by 8, and applies exp(2πi) = 1.
Claim. Let $\omega := \exp(2\pi i / 8) \in \mathbb{C}$. Then $\omega^8 = 1$. Equivalently, $\omega^8 = \exp(2\pi i) = 1$.
background
In the recognition-first quantum module, the eight-tick cycle is the finite group $\mathbb{Z}/8\mathbb{Z}$. Occupation and cost-rate are realized as the shift and clock operators of the finite Heisenberg–Weyl group on functions $\mathbb{Z}/8\mathbb{Z} \to \mathbb{C}$. Their braiding phase is a fixed complex number $\omega$, defined as the standard eighth root of unity via the complex exponential.
The module derives the Weyl relation $\mathrm{clock}\circ\mathrm{shift} = \omega,(\mathrm{shift}\circ\mathrm{clock})$ rather than postulating $[x,p]=i\hbar$. The only ring-specific content of that braiding is $\omega^8=1$ together with $\omega\neq 1$. This lemma is the closure half of that pair: raising the phase through a full eight-tick period returns the identity scalar.
Framework landmark T7 forces the eight-tick octave (period $2^3$); here that period appears concretely as the order of $\omega$ in $\mathbb{C}^\times$.
proof idea
Tactic proof in two steps. First establish $\omega^8 = \exp(2\pi i)$: unfold the definition of $\omega$, rewrite with $\mathrm{Complex.exp_nat_mul}$ so the factor 8 enters the exponent, then congr/push_cast/ring to identify the exponent with $2\pi i$. Second, rewrite by that equality and apply the Mathlib fact $\mathrm{Complex.exp_two_pi_mul_I}$, i.e. $\exp(2\pi i)=1$.
why it matters
Parent theorem eightTick_weyl (the eight-tick Weyl relation) uses this identity on the single wraparound case $k=0$: the exponent reconciliation $\omega^{k.\mathrm{val}} = \omega^{(k-1).\mathrm{val}+1}$ is a finite $\mathrm{ZMod},8$ fact, and when $k=0$ one needs $\omega^0 = \omega^8$, which this lemma supplies.
That Weyl relation is the recognition root of canonical non-commutativity: occupation and cost-rate fail to commute by exactly the eight-tick phase $\omega$. In the RS forcing chain this sits under T7 (eight-tick octave). The continuum limit $[x,p]=i\hbar$ and the magnitude $\hbar=\varphi^{-5}$ remain open (node D6); this lemma only closes the discrete cyclic algebra.
Together with the sibling $\omega\neq 1$, it makes the non-commutativity genuine rather than a trivial central phase.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.