odd_mode_fourth_eigenvalue
plain-language theorem explainer
On odd Fourier modes of the eight-cycle, the mode eigenvalue raised to the fourth power equals −1 in ℂ. Anyone proving that four one-tick shifts act as −I on the quarter-turn core cites this. The argument is a short power-law rewrite: reduce to ω₈⁴ = −1 and apply that odd powers of −1 are −1.
Claim. Let $\omega_8 = e^{2\pi i/8}$ be the primitive eighth root of unity. For every $k \in \{0,\ldots,7\}$ with $k$ odd, $(\omega_8^k)^4 = -1$ in $\mathbb{C}$.
background
The eight-tick octave is the fundamental evolution period in Recognition Science (forcing chain T7): one full cycle has length $2^3 = 8$. The primitive root $\omega_8 = e^{2\pi i/8} = e^{i\pi/4}$ is the generator of the cyclic DFT on that period; mode $k$ carries eigenvalue $\omega_8^k$ under a one-step cyclic shift.
Odd modes are those with odd index $k \in \mathrm{Fin},8$. The local module builds the recognition operator and its action on eight-channel signals; the quarter-turn core is the span of those odd modes. Upstream, omega8_pow_4 records $\omega_8^4 = -1$, which is the algebraic seed for four-step sign flip.
proof idea
Term-mode rewrite. First convert $(\omega_8^k)^4$ to $\omega_8^{4k}$ via the power-multiplication identities (with a Nat.mul_comm swap so the exponent is $4\cdot k$). Factor as $(\omega_8^4)^k$ and replace $\omega_8^4$ by $-1$ using omega8_pow_4. The remaining claim is $(-1)^k = -1$, which follows from the hypothesis that $k$ is odd (Odd.neg_one_pow), discharged by simpa.
why it matters
This is the modewise eigenvalue fact behind the paper statement $P^4 = -I$ on the quarter-turn core. Downstream, shift_four_eq_neg_on_quarterTurnCore inducts over the span of odd modes and invokes this lemma at each generator: four iterated cyclic shifts send mode $k$ to $(\omega_8^k)^4$ times itself, hence to $-f$.
In the forcing chain this sits under T7 (eight-tick octave) and the complex-structure forcing imported by the module: the sign flip after four ticks is the discrete quarter-turn that distinguishes the odd-mode core from even modes (where the same power is $+1$). Without the odd-mode restriction the identity fails, so the lemma cleanly carves the subspace on which the recognition operator implements a geometric $-I$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.