mem_quarterTurnModes
plain-language theorem explainer
For mode indices in the eight-tick cycle, membership in the canonical quarter-turn set equals odd parity. Anyone building or citing the recognition operator's minimal structured sector needs this equivalence. The proof is exhaustive case analysis on Fin 8 discharged by decide.
Claim. For every $k \in \{0,1,\ldots,7\}$, one has $k \in \{1,3,5,7\}$ if and only if $k$ is odd.
background
The Recognition Operator module packages the discrete ledger state on an eight-tick cycle (the T7 octave of period $2^3$). Mode indices live in $\mathrm{Fin},8$. The canonical quarter-turn mode set is the explicit finset ${1,3,5,7}$: the four odd residues.
Odd modes are the minimal structured content retained when one projects the full eight-channel signal down to a quarter-turn sector. Even modes (including the zero mode) are the complementary bulk that the structured-sector construction deliberately drops. The lemma simply equates set membership in that finset with the arithmetic predicate $\mathrm{Odd},k$.
Upstream, the set itself is a plain definition; the surrounding operator infrastructure imports the complex-structure forcing layer and sits under the broader Recognition Composition Law / forcing-chain foundation.
proof idea
Term-mode proof by exhaustive case split: fin_cases k expands the goal into eight concrete membership statements (one per residue of $\mathrm{Fin},8$), and decide closes each Boolean equivalence. No algebraic lemmas are invoked; the claim is pure finite arithmetic.
why it matters
This is the membership bridge used by quarterTurnSector, the paper's minimal structured sector: that definition sets keepModes := quarterTurnModes and discharges odd_modes_included by rewriting through this equivalence (simpa [mem_quarterTurnModes]). Without it, the sector's "keep exactly the odd modes" invariant would be a manual finset fact rather than a parity statement.
In the Recognition framework the eight-tick octave (T7) is forced; quarter-turn structure is the coarsest nontrivial subsector compatible with that period. The lemma therefore sits at the interface between the discrete mode lattice and the structured-sector projections used downstream in the recognition operator. It does not itself force complex structure or dimensions; it only certifies the parity characterization of the mode set those constructions keep.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.