sectorProject
plain-language theorem explainer
Canonical linear projector that retains exactly the Fourier modes listed by a structured sector on the 8-tick signal space. Anyone assembling the recognition update (projector-after-shift) or proving that the quarter-turn core is fixed cites this map. Linearity is discharged by two short calc chains that push addition and scalar multiplication through the DFT coefficient map and the finite sum over kept modes.
Claim. Fix a structured sector $S$ with kept mode set $K\subset\mathrm{Fin}\,8$ (all odd modes included, DC excluded). The sector projector $P_S:\mathbb{C}^8\to\mathbb{C}^8$ is the $\mathbb{C}$-linear map $(P_S f)(t)=\sum_{k\in K}\hat f(k)\,\omega_8^{tk}/\sqrt{8}$, where $\hat f(k)$ are the DFT-8 coefficients of $f$ and $\omega_8$ is a primitive 8th root of unity.
background
The ambient space is Signal8, the complex-valued functions on the eight-tick clock (the discrete circle of length $2^3$ forced by the T7 octave). Its Fourier analysis is the unitary DFT-8: coefficients $\hat f(k)$ and matrix entries $\omega_8^{tk}/\sqrt{8}$.
A structured sector packages a finite set $K$ of frequency indices that must contain every odd mode ${1,3,5,7}$ and must exclude the DC mode $k=0$. The odd-mode core is the quarter-turn subspace; a structured sector may enlarge it by selected even non-DC modes.
Upstream, the coefficient map is already known to be $\mathbb{C}$-linear: $\widehat{f+g}=\hat f+\hat g$ and $\widehat{a\cdot f}=a,\hat f$. Those two lemmas are the only analytic input needed to promote the mode-truncation formula into a bundled linear map.
proof idea
The definition supplies toFun as the partial inverse DFT summed only over $K$. The two linearity obligations are pure calc scripts.
For additivity: rewrite $\widehat{f+g}$ by dft_coefficients_add, distribute the product over the summand by ring, then split the Finset sum by Finset.sum_add_distrib.
For homogeneity: rewrite $\widehat{a\bullet f}$ by dft_coefficients_smul, reassociate the scalar by ring, and pull $a$ out of the sum by Finset.mul_sum.
No spectral identities beyond coefficient linearity are used.
why it matters
This projector is the spatial half of the concrete recognition update: recognitionUpdate S = sectorProject S ∘ shift, i.e. cyclic advance of the eight-tick register followed by mode truncation to the sector. Downstream lemmas record the pointwise formula, the on-mode keep-or-kill rule, and the key structural fact that every structured-sector projector acts as the identity on the quarter-turn core.
In the Recognition Science chain the eight-tick clock is the T7 octave; keeping all odd modes guarantees that the quarter-turn generator (the complex structure forced earlier in the foundation) survives every admissible sector. The definition therefore sits between the spectral DFT-8 layer and the dynamical recognition operator that evolves ledger signals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.