quarterTurnCore
plain-language theorem explainer
The quarter-turn core is the complex linear span of the four odd DFT modes on the eight-tick signal space. Anyone working the RecognitionOperator or the forced operator-core step cites it as the minimal invariant subspace where four cyclic shifts act as minus identity. The definition is a direct span construction from the odd columns of the length-8 DFT matrix.
Claim. Define the quarter-turn core as the $\mathbb{C}$-submodule of eight-tick signals spanned by $\{ e_k : k \in \{0,\ldots,7\},\; k\ \mathrm{odd}\}$, where $e_k$ is the $k$-th discrete Fourier mode on $\mathbb{C}^8$.
background
The ambient space is Signal8, the complex eight-tick register forced by the complex-structure package: functions Fin 8 → ℂ carrying the cyclic one-tick shift. The DFT basis vectors dft8_mode k are the columns of the length-8 DFT matrix; each is an eigenvector of the cyclic shift with eigenvalue a power of a primitive eighth root of unity.
Odd modes ($k = 1,3,5,7$) are precisely those whose fourth-power eigenvalue is $-1$. Their span is therefore the natural home of the quarter-turn relation $P^4 = -I$ used throughout the Recognition Operator development. The module sits in the Foundation layer that builds the analytic eight-tick operator after the complex-structure forcing import.
Upstream, the DFT mode definition supplies the generators; the eight-tick period itself is the T7 landmark of the forcing chain (period $2^3$).
proof idea
Pure definition: the submodule is the complex span of the set of all dft8_mode k for which k.val is odd. No proof obligations beyond the span constructor.
why it matters
This subspace is the operator core that later theorems pin down. Downstream, shift_four_eq_neg_on_quarterTurnCore records the concrete $P^4 = -I$ identity used in the paper; shift_mem_quarterTurnCore shows one-tick invariance; sectorProject_eq_id_on_quarterTurnCore and recognitionUpdate_eq_shift_on_quarterTurnCore show that every structured-sector projector fixes the core and that the projector-after-shift update collapses to bare cyclic shift on it. The inclusion quarterTurnCore_le_neutralRegister places the core inside the neutral register, and OperatorCore_Forced in the UnifiedForcingChain cites it when forcing the recognition operator core. Framework landmark: T7 eight-tick octave, with the odd-mode quarter-turn supplying the complex structure that pairs with D = 3 spatial forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.