shift_four_eq_neg_on_quarterTurnCore
plain-language theorem explainer
Four cyclic shifts act as multiplication by −1 on every 8-tick signal in the quarter-turn core (the odd DFT-mode span). Anyone citing the paper identity P⁴ = −I on that core uses this lemma. The proof is submodule span induction: odd modes have fourth eigenvalue −1, and the relation extends by additivity and scalar homogeneity of the iterated shift.
Claim. Let $f$ be an 8-tick complex signal lying in the quarter-turn core (the complex span of the odd discrete-Fourier modes on the eight-tick circle). Then four iterations of the cyclic shift satisfy $P^4 f = -f$.
background
The ambient space is Signal8: complex-valued functions on the eight-tick discrete circle, the analytic home of the Recognition operator in this module. The one-tick map is the cyclic shift; cyclicShiftIter n is its n-fold iterate. DFT modes are eigenvectors of every iterate, with eigenvalues powers of the primitive 8th root of unity.
The quarter-turn core is the subspace spanned by the odd modes. On those modes the fourth power of the mode eigenvalue collapses to −1 (lemma odd_mode_fourth_eigenvalue), which is the spectral seed of the geometric statement P⁴ = −I. The eight-tick setting is the T7 octave of the forcing chain: period 2³ forces the discrete circle on which this shift lives.
Upstream, iterated shift is linear (preserves addition and scalar multiplication) and acts diagonally on each DFT mode. Those three facts, plus the odd-mode eigenvalue identity, are exactly the ingredients fed to the span induction below.
proof idea
Apply submodule span induction on membership in the quarter-turn core.
- Generators: each odd mode m = dft8_mode k satisfies cyclicShiftIter 4 m = (ω₈^k)⁴ • m. The odd-mode fourth-eigenvalue lemma rewrites the scalar as −1, so the claim is −m after a pointwise simp.
- Zero vector: immediate from the definition of the iterated shift.
- Sum: cyclicShiftIter_add moves the operator across +, the inductive hypotheses give −x + −y, and scalar arithmetic rewrites that as −(x+y).
- Scalar multiple: cyclicShiftIter_smul pulls the scalar out; the inductive hypothesis and simp finish −(a • x).
No further spectral input is required once the generators are settled.
why it matters
This is the concrete P⁴ = −I identity named in the paper and recorded in the doc-comment. The sole direct consumer is twoBeat_square_eq_neg_on_quarterTurnCore, which rewrites two successive two-beat steps as four shifts and quotes this lemma in one line: two beats therefore square to −I on the same core.
In the Recognition framework the statement sits inside the analytic 8-tick operator that realises the T7 octave. It supplies the algebraic half of the quarter-turn / complex-structure story imported from ComplexStructureForcing: a linear operator whose fourth power is −Id on the odd sector is precisely a discrete model of multiplication by i (up to the usual two-beat packaging). Downstream structured-sector projectors that fix the core pointwise rely on this sign flip being exact, not approximate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.