eighth_root_ne_one
plain-language theorem explainer
The complex number exp(2πi/8) is not 1. Anyone proving that the eight eighth roots of unity sum to zero needs this non-degeneracy fact. The proof is a short contradiction: if the root were 1 then its fourth power would force 1 = −1.
Claim. The complex exponential $\exp(2\pi i/8)$ is not equal to $1$.
background
This module banks the Wave C1 R2 exact-shell tick-phase enrichment schema for Gap 2. Exact path classes carry a tick assignment into Fin 8, and the derived phase is $2\pi\cdot\mathrm{tick}/8$. The eight-tick octave (forcing chain T7) supplies the period; the analytic content here is independent equidistribution and root-of-unity cancellation on shells.
The sibling tickRoot is the map sending each residue $p\in\mathrm{Fin},8$ to $\exp(2\pi i,p/8)$. Summing those roots is the algebraic engine of the amplitude bridge: mass-balanced Fin-8 fibers cancel by eighth-root orthogonality, yielding shell amplitude vanishing. Before that sum identity can be proved, one must know the generator is not the trivial root 1.
The local setting is combinatorial guards first (equal fiber cardinalities, mass balance under shellwise-constant class measure), then the complex-analytic bridge. No continuum or measure axioms are flipped here.
proof idea
Proof by contradiction. Assume $\omega:=\exp(2\pi i/8)=1$. Raise both sides to the fourth power and use $\exp(z)^n=\exp(nz)$ to obtain $\omega^4=\exp(\pi i)$. The standard identity $\exp(\pi i)=-1$ then yields $1^4=-1$, i.e. $1=-1$, which is absurd by norm_num. The only algebraic steps are rewriting the exponent by ring and applying Complex.exp_pi_mul_I.
why it matters
Feeds the parent theorem sum_tickRoots_eq_zero (sum of the eight eighth roots vanishes), which is the load-bearing algebraic step of the root-of-unity bridge in this module. That bridge turns mass-balanced tick fibers into ShellAmplitudeVanishes, closing the combinatorial-to-amplitude transport named in the module doc.
Framework landmark: T7 eight-tick octave (period $2^3$). The lemma is the non-degeneracy half of the geometric-sum argument for the cyclotomic filter on shells. It does not itself discharge the still-open TypedResidual_strengthened_tick_balance or the analytic OscillatoryTail for the signature-vertex witness (R4); it only unlocks the finite sum identity used by the per-shell cancellation theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.