sectorProject_eq_id_on_quarterTurnCore
plain-language theorem explainer
Every structured-sector Fourier projector acts as the identity on the quarter-turn core (the C-span of odd DFT modes on the 8-tick signal space). Anyone showing that recognition updates reduce to bare cyclic shift on that core cites this. The proof is span induction: generators are kept by the sector's odd-mode inclusion axiom, then linearity closes add and scalar cases.
Claim. For every structured sector $S$ (kept Fourier modes including all odd indices and excluding DC) and every eight-tick signal $f$ in the quarter-turn core (the $\mathbb{C}$-span of the odd DFT modes), the sector projector satisfies $P_S(f)=f$.
background
Work is on Signal8, complex-valued functions on the eight-tick circle, the discrete carrier of the Recognition operator. The cyclic shift advances the reading index by one tick and is the fundamental discrete time generator.
The quarter-turn core is the $\mathbb{C}$-span of the odd DFT modes ${1,3,5,7}$. A structured sector extends that core by a finite set of kept modes that is required to contain every odd mode and to exclude the DC mode $k=0$. The sector projector is the linear map that retains exactly the Fourier coefficients in the kept set and kills the rest; on a single basis mode it is the identity or zero according as the mode is kept.
The local setting is the analytic 8-tick Recognition operator (Foundation), not the legacy ledger API. The odd-mode inclusion axiom is what forces every such projector to fix the core.
proof idea
Apply Submodule.span_induction to membership of $f$ in the quarter-turn core.
On generators: an odd DFT mode $k$ lies in keepModes by odd_modes_included, so sectorProject_mode returns the mode unchanged.
Zero: the projector is a linear map, hence sends $0$ to $0$.
Sum: map_add plus the two inductive hypotheses.
Scalar: map_smul plus the inductive hypothesis.
No further Fourier analysis is needed once the generators are fixed.
why it matters
This is the identity step that lets the projector-after-shift update collapse to bare cyclic shift on the core. The immediate parent is recognitionUpdate_eq_shift_on_quarterTurnCore, whose doc-comment states that the update "reduces to the bare shift on the quarter-turn core, independently of the chosen sector extension."
In the forcing chain this sits under the eight-tick octave (T7, period $2^3$): the odd modes are exactly the quarter-turn harmonics of that discrete circle. Sector extensions may add even non-DC modes, but the core dynamics stay sector-independent. Without pointwise fixation, recognition updates would mix sector choice into the core evolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.