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 the quarter-turn identity P⁴ = −I on the odd-mode core cites this. The argument rewrites the exponent, inserts ω₈⁴ = −1, and uses that odd integers satisfy (−1)^k = −1.
Claim. Let $\omega_8$ be a primitive eighth root of unity. For every $k \in \{0,\ldots,7\}$ with $k$ odd, $(\omega_8^k)^4 = -1$ in $\mathbb{C}$.
background
Recognition Science evolves ledger signals on an eight-tick octave (T7): one full period is eight fundamental ticks τ₀. Spectral analysis of that cycle uses the primitive eighth root ω₈ = exp(2πi/8), so mode k carries multiplier ω₈^k under a one-tick cyclic shift.
Odd modes are those with odd index k ∈ Fin 8. The lemma records the elementary root-of-unity fact that four successive multiplications by ω₈^k send such a mode to its negative. Upstream, omega8_pow_4 supplies ω₈⁴ = −1; the tick constant only fixes the discrete time unit and is not used algebraically here.
Locally this sits in the RecognitionOperator module, which builds the one-tick propagator and its action on the eight-dimensional signal space Signal8.
proof idea
Term-mode rewrite chain. First convert (ω₈^k)⁴ into ω₈^(4k) via the power-multiplication identities (with a Nat.mul_comm flip). Then apply omega8_pow_4 to replace ω₈⁴ by −1, leaving (−1)^k. Finally simpa with the oddness hypothesis discharges (−1)^k = −1 via the standard Odd.neg_one_pow fact.
why it matters
This is the modewise algebraic engine behind the paper's concrete P⁴ = −I statement. Downstream, shift_four_eq_neg_on_quarterTurnCore inducts over the span of odd modes and invokes this lemma on each generator: four cyclic shifts act as −Id on the quarter-turn core.
In the forcing chain the eight-tick octave (T7) is the discrete period forced by the recognition calculus. Establishing that four ticks act as a global sign flip on the odd sector is the spectral content of a half-octave (quarter-turn) evolution, and it feeds the complex-structure and recognition-operator development that sits on top of that octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.