shift_period_8
plain-language theorem explainer
On the eight-slot complex carrier, the cyclic recognition shift has exact period 8: eight applications recover every signal. Anyone citing the T7 eight-tick octave, the complex-structure certificate, or the T7-to-canonical-carrier bridge needs this identity. The OperatorCore entry is a one-line re-export of the proved Foundation theorem.
Claim. For every signal $f : \mathrm{Fin}\,8 \to \mathbb{C}$, the eighth iterate of the cyclic shift equals $f$: $T^{8}f = f$. Equivalently, the recognition clock on the eight-tick carrier is strictly 8-periodic.
background
The local setting is complex-structure forcing on the canonical recognition carrier. A signal is a map $f : \mathrm{Fin},8 \to \mathbb{C}$ (eight complex amplitudes, one per tick of the recognition clock). The elementary shift $T$ advances the index by one step modulo 8; shiftIter n is its $n$-fold composition.
Upstream, the Foundation theorem states the same identity and proves it from the fact that eight steps of the index map nextIdx return every residue class in $\mathrm{Fin},8$. The module doc frames this as the fundamental periodicity of the recognition clock: $T^{8} = \mathrm{id}$.
In the forcing chain this is the concrete operator realization of T7 (eight-tick octave, period $2^{3}$). The same period later forces a faithful representation whose spectrum contains a non-real eigenvalue, which is why the carrier must be complex rather than real.
proof idea
This OperatorCore declaration is an abbrev that simply names the already-proved Foundation theorem ComplexStructureForcing.shift_period_8. No new argument is given here.
The upstream proof is short: extensionality on the eight indices, unfold the iterated shift to eight applications of the one-step map, then apply the lemma that nextIdx has order 8 on $\mathrm{Fin},8$. The result is $T^{8}f = f$ pointwise.
why it matters
This identity is the operator form of T7's eight-tick octave. It is the periodicity field of the complex-structure certificate (together with the imaginary eigenvalue at mode 2, the real-obstruction $x^{2}+1$, DFT unitarity, and phase-invariant mode cost). Downstream, UnitaryEvolution and Hamiltonian emergence sit in the same module and rely on the same 8-periodic carrier.
In UnifiedForcingChain it is wired into T7_To_CanonicalCarrier_Bridge and the theorems that the bridge holds: T7 supplies the eight-tick equation, and this lemma supplies the matching period for the canonical shift on Signal8 = Fin 8 → ℂ. Without $T^{8} = \mathrm{id}$, the bridge from dimension forcing to the complex carrier would not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.