sectorProject_apply
plain-language theorem explainer
Pointwise evaluation of the structured-sector Fourier projector equals the partial inverse DFT over the sector's kept modes. Anyone working with 8-tick mode filtering or sector projections cites this as the simp normal form. The proof is pure definitional equality (rfl).
Claim. For any structured sector $S$ (a finite set of kept Fourier modes on $\mathrm{Fin}\,8$ that includes all odd modes and excludes DC), any 8-tick complex signal $f$, and any tick $t\in\mathrm{Fin}\,8$, the projected signal at $t$ equals $\sum_{k\in S.\mathrm{keep}} \hat f(k)\,\omega^{tk}$, where $\hat f$ are the length-8 DFT coefficients and $\omega$ is the DFT8 kernel entry.
background
The ambient setting is the analytic 8-tick recognition operator on Signal8 (complex-valued functions on $\mathrm{Fin},8$), the discrete circle of the eight-tick octave forced at T7. The DFT8 basis diagonalizes tick-periodic evolution; coefficients and kernel entries are the standard unitary DFT data on eight points.
A structured sector packages a mode set that always keeps the four odd (quarter-turn) modes and never the DC mode, optionally adding further non-DC even modes. The sector projector is the linear map that retains exactly those Fourier components and zeros the rest: it is defined by summing $\hat f(k),\mathrm{dft8_entry}(t,k)$ over the kept index set.
Upstream, that map is already introduced as a $\mathbb{C}$-linear endomorphism of Signal8; the present lemma simply exposes its pointwise formula for rewriting.
proof idea
One-line term proof by rfl. The right-hand side is literally the toFun clause in the definition of the sector projector, so application at $(f,t)$ is definitionally that partial inverse-DFT sum. Marked @[simp] so later mode-by-mode arguments reduce automatically.
why it matters
Feeds the sibling lemma that a pure DFT basis mode is either fixed or sent to zero according as its index lies in the kept set; that lemma rewrites via this simp rule, then collapses the Finset sum to a single term. Together they justify treating structured sectors as sharp Fourier cutoffs on the eight-tick circle.
In the Recognition framework this sits inside the analytic recognition operator that realises the T7 eight-tick octave: sector projections isolate the quarter-turn core (odd modes) plus optional even harmonics while killing DC, which is the discrete counterpart of stripping the mean before reading recognition cost. No open scaffold is involved; the claim is fully proved and only packages definitional content for downstream mode calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.