StructuredSector
plain-language theorem explainer
A structured sector is a subset of the eight Fourier modes on the tick circle that must contain every odd mode and must exclude the DC mode. It packages the admissible mode supports for the recognition projector and update. Anyone citing the quarter-turn sector, sector projection, or recognition operator uses this record. The declaration is a pure structure: two forced membership axioms and a free Finset of kept modes.
Claim. A structured sector is a finite set $K \subseteq \{0,\ldots,7\}$ of Fourier mode indices such that every odd index lies in $K$ and the DC mode $0$ does not: if $k$ is odd then $k \in K$, and $0 \notin K$. Even non-DC modes may be added freely.
background
The ambient setting is the eight-tick signal space (period $2^3$), the discrete circle underlying the Recognition Operator module. Signals are complex functions on eight ticks; their DFT has modes indexed by $\mathrm{Fin},8$. Mode $0$ is the DC (mean) component. The odd modes ${1,3,5,7}$ form the quarter-turn core used throughout the paper's minimal dynamics.
A structured sector extends that core by naming which modes the projector keeps. The only hard constraints are: all odd modes stay in, and DC stays out. Optional even modes ${2,4,6}$ may be included when a larger sector is wanted. Downstream, the sector projector sums only the kept DFT coefficients, and the recognition update is that projector after a cyclic shift.
Sibling data in the module (ledger state, bonds, channels, global phase) sit beside this Fourier-side packaging; the sector itself is purely a mode-support record.
proof idea
No proof body: this is a structure definition. Three fields fix the meaning. keepModes is an arbitrary finite subset of the eight mode indices. The first axiom requires every odd index to belong to that set (so the quarter-turn core is never dropped). The second axiom forbids mode $0$ from the set (DC is never kept). Instantiations such as the minimal quarter-turn sector discharge both axioms by taking exactly ${1,3,5,7}$.
why it matters
This record is the sector parameter of the public Recognition Operator and of the concrete recognition update (projector after shift). The minimal instance is the quarter-turn sector, which keeps exactly the odd modes. Sector projection and the lemmas that it acts as the identity on the quarter-turn core are typed over an arbitrary structured sector, so the same identities hold for any allowed extension.
In the framework this sits on the eight-tick octave (forcing chain T7): mode support is chosen inside the forced period-$8$ discrete circle, never by free continuum Fourier analysis. The DC-exclusion and odd-mode-inclusion axioms encode the paper's choice that the recognition dynamics live on the quarter-turn core and may only enlarge by non-DC even modes. Parent consumers include the bundled operator evolve map and the reduction of projector-after-shift to bare shift on the core, independent of how far the sector is extended.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.