shift_period_8
plain-language theorem explainer
Eight applications of the cyclic shift on an 8-tick complex signal return the original signal: T^8 = id. Anyone citing the recognition clock, DFT-8 diagonalization, or the T7 carrier bridge needs this identity. The proof is pointwise: reduce iterated shift to eight index advances and apply the Fin-8 wraparound lemma.
Claim. For every signal $f : \mathrm{Fin}\,8 \to \mathbb{C}$, the eighth iterate of the cyclic shift $T$ satisfies $T^8 f = f$, where $(Tf)(k) = f(k+1 \bmod 8)$.
background
The module Complex Structure Forcing starts from T7: the eight-tick forces a cyclic shift $T$ on the ledger state space with $T^8 = I$. Signals are Signal8, i.e. maps $\mathrm{Fin},8 \to \mathbb{C}$. The shift advances the reading index by one tick: $(Tf)(k) = f(\mathrm{nextIdx},k)$. Iteration is the usual recursive composition of $T$.
The sole nontrivial input is the private lemma that eight successive nextIdx steps fix every $k \in \mathrm{Fin},8$ (proved by fin_cases and decide). That is the discrete clock wraparound on the octave.
Local goal of the module: $T$ has eigenvalues the 8th roots of unity, including $i$ at mode 2, so $T$ cannot be diagonalized over $\mathbb{R}$; complexification is forced. Periodicity $T^8 = \mathrm{id}$ is the first algebraic fact in that chain.
proof idea
Tactic proof, short. Extensionality on the output index $k$. Unfold shiftIter (eight nested compositions), Function.comp_apply, and shift, so the claim becomes $f(\mathrm{nextIdx}^8 k) = f(k)$. Finish by congrArg f applied to nextIdx_8 k, which states that eight index advances return $k$.
why it matters
This is the concrete $T^8 = \mathrm{id}$ of the recognition clock (T7 eight-tick octave). It is the periodicity field of complex_structure_certificate, which packages the full forcing argument: period 8, imaginary eigenvalue $i$, no real root of $x^2+1$, DFT-8 unitarity, and J-cost phase invariance.
Downstream, the Unified Forcing Chain bridge T7_To_CanonicalCarrier_Bridge and its holder theorem cite it as shift_period_8, tying T7's eight-tick equation to the canonical carrier $\mathrm{Fin},8 \to \mathbb{C}$ and the cyclic shift's spectrum. OperatorCore re-exports the same fact. Without period 8 there is no primitive 8th-root spectrum and no forced complex structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.