quarterTurnModes
plain-language theorem explainer
The canonical quarter-turn mode set on the eight-tick cycle is the four odd indices {1,3,5,7}. Anyone building structured sectors of the recognition operator cites this set as the keep-list for odd modes. It is a bare Finset literal, not a derived theorem.
Claim. The canonical quarter-turn mode index set is the finite set $\{1,3,5,7\}$ inside $\mathrm{Fin}\,8 \cong \{0,\ldots,7\}$.
background
Recognition Science forces an eight-tick octave (forcing chain T7): discrete time and mode labels live on a cycle of length $2^3 = 8$. Mode indices are therefore elements of $\mathrm{Fin},8$.
In the recognition-operator module, a structured sector is specified by which of those eight Fourier-like modes are retained. The paper's minimal structured choice keeps exactly the odd indices. Those odds are the quarter-turn modes: advancing by one tick multiplies the phase by a primitive fourth root relative to the full eight-cycle.
Sibling ledger state fields (channels, global phase, active bonds) sit on the same eight-slot scaffolding; this definition only names the odd-mode subset used downstream.
proof idea
Pure definition: the Finset is introduced by the literal enumerator ${1,3,5,7}$. No lemmas are applied. The companion membership lemma later proves, by exhaustive fin_cases and decide, that membership is exactly odd parity of the underlying Nat value.
why it matters
This set is the keep-list for quarterTurnSector, the minimal structured sector used in the paper (keep exactly the odd modes, exclude the DC mode). The membership characterization mem_quarterTurnModes rewrites $k \in$ this set as $\mathrm{Odd},k.\mathrm{val}$, so later proofs can reason in parity language rather than set literals.
Framework landmark: T7 eight-tick octave. Restricting to odd modes is the discrete analogue of a quarter-period sector on the forced period-$8$ cycle; it is the smallest nontrivial mode filter compatible with that octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.