omega_ne_one
plain-language theorem explainer
The eight-tick phase factor ω is not 1, so the recognition cycle is nontrivial. Anyone deriving canonical non-commutativity from the finite Heisenberg–Weyl structure on Z/8Z needs this fact. Proof is a short contradiction: ω = 1 forces ω⁴ = 1, but the exponential definition gives ω⁴ = exp(πi) = −1.
Claim. Let $\omega = \exp(2\pi i/8)$ be the eight-tick phase on the recognition cycle. Then $\omega \neq 1$. Equivalently, if $\omega = 1$ then $\omega^4 = 1$, but $\omega^4 = \exp(\pi i) = -1 \neq 1$.
background
The module develops the eight-tick Weyl relation as the recognition-first root of canonical non-commutativity. On the cycle $\mathrm{ZMod},8$, occupation and cost-rate are realized as the shift and clock operators of the finite Heisenberg–Weyl group. They obey $\mathrm{clock}\circ\mathrm{shift} = \omega\cdot(\mathrm{shift}\circ\mathrm{clock})$ with $\omega$ an eighth root of unity; non-commutativity is therefore cyclic recognition structure rather than an axiom.
Here $\omega$ is defined via the complex exponential so that $\omega^8 = 1$. The fundamental RS time quantum is one tick ($\tau_0 = 1$), and one octave is eight ticks (forcing-chain landmark T7). The continuum limit $[x,p]=i\hbar$ with $\hbar=\varphi^{-5}$ remains open (node D6); this file only treats the finite exact root.
The nontriviality $\omega\neq 1$ is the ring-specific content that makes the braiding genuine: if the phase collapsed to 1, clock and shift would commute.
proof idea
Contradiction. Assume $\omega=1$. Then $\omega^4=1$ by rewriting and ring normalization. Separately expand the definition: $\omega^4=\mathrm{Complex.exp}(\pi\cdot i)$ after rewriting $\omega$ through $\mathrm{Complex.exp_nat_mul}$, casting, and ring. Apply $\mathrm{Complex.exp_pi_mul_I}$ to obtain $\omega^4=-1$. Substitute into the first equality and finish with $\mathrm{norm_num}$.
why it matters
Feeds canonical_noncommutativity, which exhibits an explicit wavefunction on $\mathrm{ZMod},8$ with $\mathrm{clock}(\mathrm{shift},\psi)\neq\mathrm{shift}(\mathrm{clock},\psi)$ by reducing the equality case to this lemma. That parent theorem is the finite exact RS root of $[x,p]\neq 0$; the continuum limit (node D3) is still open.
In the Recognition framework this is the algebraic content that makes the eight-tick Weyl relation a genuine non-commutative structure rather than a disguised commuting pair. It sits under T7 (eight-tick octave, period $2^3$) and under the recognition-first program that derives the canonical commutator instead of postulating it. The module notes that the braiding is ring-generic once $\omega^8=1$ and $\omega\neq 1$ are in hand; this declaration discharges the second half.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.