sectorProject_mode
plain-language theorem explainer
A structured-sector projector acts diagonally on the eight-tick DFT basis: it fixes any kept mode and annihilates every discarded mode. Anyone proving that sector projectors fix the quarter-turn core, or that the recognition update preserves selected Fourier content, cites this. The argument cases on membership in the keep-set and reduces via the Kronecker property of DFT coefficients of pure modes.
Claim. Let $S$ be a structured sector (a keep-set of Fourier indices on the eight-tick circle that includes all odd modes and excludes DC). For each mode index $k\in\{0,\ldots,7\}$, the sector projector applied to the pure DFT mode $e_k$ equals $e_k$ if $k$ is kept by $S$, and equals the zero signal otherwise.
background
Work is on Signal8, complex-valued functions on the discrete eight-tick circle $\mathrm{Fin},8$. The cyclic shift $T$ advances the reading index by one tick and generates discrete time evolution; its Fourier eigenbasis is the family of pure modes $e_k$ (written dft8_mode k). DFT coefficients of a pure mode are Kronecker-normalized: the coefficient of $e_j$ at frequency $k$ is $1$ if $k=j$ and $0$ otherwise.
A structured sector extends the quarter-turn core by a keep-set of non-DC modes that is forced to contain every odd index and to exclude the DC mode $k=0$. The associated sector projector is the linear map that reconstructs a signal from only the kept Fourier coefficients: $(\Pi_S f)(t)=\sum_{k\in S.keep} \hat f(k),e_k(t)$.
The local setting is the recognition operator module: the concrete recognition update is projector-after-shift on this eight-tick register, tying the construction to the T7 eight-tick octave.
proof idea
Pointwise extensionality on the eight ticks, then case on whether $k$ lies in the keep-set.
If $k$ is kept, rewrite the projector via its apply lemma and collapse the keep-sum with Finset.sum_eq_single at index $k$. The surviving term is $1\cdot e_k(t)$ by the mode-coefficient lemma; off-diagonal terms vanish by the same Kronecker identity; the missing-index branch is impossible because $k$ is kept.
If $k$ is not kept, the projector sum runs only over kept indices, each of which differs from $k$, so every summand is zero again by the mode-coefficient lemma, and the whole sum is the zero signal.
why it matters
This is the eigenmode calculus for structured-sector projectors: they are exactly the spectral projections onto the chosen keep-sets in the eight-tick DFT basis. Downstream, sectorProject_eq_id_on_quarterTurnCore uses it to show every such projector fixes the quarter-turn core pointwise (the core is spanned by the odd modes, which every structured sector is forced to keep). That identity is the algebraic reason the recognition update, defined as projector-after-shift, acts as the identity on the forced complex structure rather than shearing it.
In the broader chain this sits under T7 (eight-tick octave, period $2^3$) and the complex-structure forcing that selects the quarter-turn generator. Without diagonal action on modes, the projector-after-shift form of the recognition operator would not cleanly preserve the forced $i$-structure on the core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.