shift_mem_quarterTurnCore
plain-language theorem explainer
One-tick cyclic shift preserves the quarter-turn core: any 8-sample complex signal in the span of the odd DFT modes stays in that span after a cyclic shift. Analysts of the Recognition operator cite this when reducing projector-after-shift dynamics to bare propagation on the odd sector. The proof is span induction, using that each odd DFT mode is an eigenvector of the shift.
Claim. Let $f$ be an 8-sample complex signal lying in the quarter-turn core (the $\mathbb{C}$-span of the odd discrete Fourier modes on $\mathrm{Fin}\,8$). Then the one-tick cyclic shift of $f$ also lies in the quarter-turn core.
background
In Foundation.RecognitionOperator, the analytic Recognition operator acts on Signal8, the space of complex-valued 8-tick signals forced by the eight-tick octave (T7). The bare one-tick map is the cyclic shift, packaged as the $\mathbb{C}$-linear operator shiftLinear.
The quarter-turn core is defined as the span of the odd DFT modes: $\mathrm{span}_{\mathbb{C}}{m_k : k\in\mathrm{Fin},8,,k\text{ odd}}$. These modes are the natural eigenspace for a quarter-turn phase structure on the 8-cycle; the next result in the file records that four shifts act as $-I$ on this core (the concrete $P^4=-I$ identity used in the paper).
Invariance of this subspace under one-tick propagation is the algebraic prerequisite for treating the odd sector as a closed dynamical component of the Recognition update.
proof idea
Rewrite the goal as membership of shiftLinear f in the core (via the simp lemma equating shiftLinear with cyclic shift). Apply Submodule.span_induction to the hypothesis $f\in\mathrm{quarterTurnCore}$.
On generators: an odd mode $m_k$ is sent by the shift to a scalar multiple of itself (dft8_shift_eigenvector); scalar multiples of span generators stay in the span. Zero is preserved by linearity and the submodule zero law. Sums and scalar multiples are preserved because shiftLinear is linear and the core is a submodule (map_add, map_smul, add_mem, smul_mem).
why it matters
This is the invariance step that lets the Recognition update collapse to bare cyclic shift on the odd sector. The immediate parent is recognitionUpdate_eq_shift_on_quarterTurnCore: once the shifted signal remains in the core, the sector projector acts as the identity, so projector-after-shift equals the bare shift independently of any structured-sector extension.
In the framework this anchors the eight-tick (T7) dynamics of the Recognition operator: the odd-mode span is the concrete carrier of the quarter-turn / $P^4=-I$ structure used in the paper. Without this closedness, sector projections would mix modes under time evolution and the reduction of the update law would fail.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.