neutralRegister
plain-language theorem explainer
The neutral register is the mean-free hyperplane inside the eight-tick complex carrier: signals whose eight samples sum to zero. It is the ambient subspace that must contain the quarter-turn (odd DFT) core of the recognition operator. Downstream forcing bridges cite it to place the operator core inside a DC-free ledger channel. The body is the standard submodule check for a linear constraint.
Claim. Define the neutral register as the $\mathbb{C}$-submodule of eight-tick signals $f:\mathrm{Fin}\,8\to\mathbb{C}$ consisting of those $f$ with $\sum_{t} f(t)=0$ (vanishing total mass / zero DC mode).
background
In the Recognition Operator module the canonical carrier is Signal8, the complex function space on eight ticks forced by the T7 eight-tick octave (period $2^3$). The recognition operator acts by cyclic shift and DFT analysis on this carrier; physical ledger channels are required to be mean-free so that the global DC mode does not carry recognition cost.
The neutral register is exactly that mean-free hyperplane: the set of signals whose sum over the eight ticks vanishes. It is cut out as a $\mathbb{C}$-linear subspace of Signal8, so it inherits the structure needed for spans of DFT modes and for submodule comparisons such as containment of the quarter-turn core.
Local setting: this file builds the analytic 8-tick operator and the legacy ledger compatibility surface. The definition sits upstream of the DFT-mode membership lemmas and of the T7/T8 operator-core bridge certificates in the unified forcing chain.
proof idea
Definitional submodule construction, not a deep theorem. Carrier is the zero-sum set. Zero membership is immediate by simp. Closure under addition rewrites the sum of $f+g$ via pointwise addition and Finset.sum_add_distrib, then adds the two zero hypotheses. Closure under scalar multiplication rewrites the sum of $a\bullet f$ via Finset.mul_sum and multiplies the zero hypothesis by $a$. No external lemmas beyond the standard Pi/Finset simp facts are required.
why it matters
The neutral register is the ambient home of the operator core in the forcing chain. quarterTurnCore_le_neutralRegister places the odd Fourier span inside it; dft8_mode_mem_neutralRegister shows every non-DC DFT mode already lives there. Those facts feed OperatorCore_Forced.quarter_core_neutral and the T7/T8 operator-core bridge, which certify that the quarter-turn core forced by T7 (eight-tick octave) and T8 ($D=3$) sits in a DC-free channel and is propagated by the bare cyclic shift.
Without a named mean-free submodule, the bridge certificates could not state neutrality of the core as a submodule inequality. The definition therefore closes the carrier side of the T7 → canonical carrier → operator core path: eight ticks force Signal8, DFT isolates odd modes, and neutrality keeps recognition off the global phase/DC register.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.