RecognitionOperator
plain-language theorem explainer
Packages a structured sector (selected non-DC modes on the eight-tick circle, always keeping all odd modes) as the public record for projector-then-shift one-tick evolution on complex 8-signals. Foundation and bridge authors cite it when the analytic 8-tick operator must present a stable operator API. It is a bare structure definition: one field, no proof obligations.
Claim. A recognition operator is a record whose sole data is a structured sector: a finite subset $S \subseteq \{0,\ldots,7\}$ of Fourier modes on the eight-tick circle such that every odd index lies in $S$ and the DC mode $0$ does not.
background
The ambient setting is the analytic eight-tick operator on Signal8, the space of complex-valued functions on $\mathbb{Z}/8\mathbb{Z}$ forced in ComplexStructureForcing. Discrete time is generated by the cyclic shift $T$, $(Tf)(k)=f(k+1 \bmod 8)$, advancing one fundamental tick $\tau_0=1$. The eight phases are $k\pi/4$ for $k=0,\ldots,7$, matching the T7 octave period $2^3$.
A structured sector extends the quarter-turn (odd-mode) core by a chosen set of keep-modes: every odd $k$ must be retained, and the DC mode $0$ is forbidden. That selection is the only payload of the operator record. Older ledger bridges still expect fields such as time, Z-patterns, and recognition cost; this module keeps a thin compatibility surface while the canonical object is the mode-selected 8-signal propagator.
proof idea
No proof. The declaration is a structure with a single field sector : StructuredSector. Inhabitation reduces to supplying a Finset of modes in Fin 8 that contains all odd indices and excludes 0; the two Prop fields of StructuredSector are the only obligations.
why it matters
Gives the public Foundation handle for one-tick projector-followed-by-shift update on the forced complex 8-signal, tying the operator API to the eight-tick octave (T7) and to ComplexStructureForcing's shift generator. Downstream used-by edges are empty in the current graph, so the record is presently a stable export surface rather than an intermediate lemma. It separates mode policy (which non-DC modes survive) from the dynamics (shift), so bridges can swap sectors without reopening the forcing chain. Lands in the same layer as the bare Signal8 propagator and the legacy ledger compatibility shim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.