quarterTurnCore_le_neutralRegister
plain-language theorem explainer
The odd discrete Fourier modes on the eight-tick carrier span a subspace inside the mean-free neutral register. Anyone packaging the analytic recognition operator core after the eight-tick forcing step cites this inclusion. The argument is a short span-membership reduction: odd indices cannot be the DC mode, so each generator already lies in the neutral register by the non-DC mode lemma.
Claim. Let the eight-tick carrier be $\mathbb{C}^8$ with the standard DFT basis. The submodule spanned by the odd Fourier modes is contained in the neutral register $\{f:\sum_{t\in\mathbb{Z}/8\mathbb{Z}} f(t)=0\}$.
background
The local setting is the recognition operator on the forced eight-tick carrier (T7). Signals are maps Fin 8 → ℂ. The neutral register is the mean-free subspace: those signals whose sum over the eight ticks vanishes. It is the natural place for pure oscillatory content once the DC (global phase / total charge) mode is removed.
The quarter-turn core is the submodule spanned by the odd DFT modes. Odd modes generate the quarter-period shift structure that later becomes the complex structure and the recognition update on the carrier. Upstream, each non-DC DFT mode is already known to lie in the neutral register: its character sum over the cyclic group is zero.
The module sits under the foundation forcing chain that turns the eight-tick octave and $D=3$ into an analytic operator package.
proof idea
Apply Submodule.span_le and check generators. A generator is a DFT mode indexed by some $k\in\mathrm{Fin},8$ with $k$ odd. The zero index is even, so $k\neq 0$: if $k=0$ then $\mathrm{Odd},0$, contradiction. Invoke dft8_mode_mem_neutralRegister on that nonzero index to place the mode in the neutral register. Hence the whole odd span sits inside.
why it matters
This inclusion is the first field of the operator-core package: operator_core_holds records it as quarter_core_neutral, then pairs it with the quarter-turn commit identity and Hamiltonian preservation on that core. Downstream bridges t7_t8_to_operator_bridge_holds and t7_to_canonical_carrier_bridge_holds use the same core to pass from T7 (eight-tick octave, period $2^3$) and T8 ($D=3$) into the analytic recognition operator. Without the odd span living in the mean-free register, the quarter-turn dynamics would mix charge and could not be a pure phase rotation on the forced carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.