shiftIter
plain-language theorem explainer
Recursive n-fold iterate of the cyclic 8-tick shift on ledger signals Fin 8 → ℂ. At n = 0 it is the identity; each successor composes one more advance-by-one-tick. Cited wherever Tⁿ or the period-8 law T⁸ = id is needed (periodicity theorem, complex-structure certificate, T7 carrier/shift bridges). Defined by structural recursion on ℕ.
Claim. Define the $n$-fold iterate $T^n$ of the cyclic shift on signals $f : \mathrm{Fin}\,8 \to \mathbb{C}$ by $T^0 = \mathrm{id}$ and $T^{n+1} = T \circ T^n$, where $(Tf)(k) = f(k+1 \bmod 8)$.
background
The module Complex Structure Forcing shows that the 8-tick shift cannot be diagonalized over ℝ, so complexification is algebraically forced. T7 supplies a cyclic time-evolution operator $T$ on the ledger state space with $T^8 = I$; eigenvalues are the 8th roots of unity, and $\omega^2 = i$ has no real square root.
A signal on the 8-tick cycle is a map $\mathrm{Fin},8 \to \mathbb{C}$. The one-step index advance is $k \mapsto (k+1)\bmod 8$. The shift operator acts by $(Tf)(k) = f(k+1 \bmod 8)$: the discrete generator of recognition-clock evolution.
Iterates $T^n$ package repeated application so that periodicity, spectral claims, and bridge certificates can name $T^8$ and intermediate powers without ad-hoc composition chains.
proof idea
Definition by recursion on $\mathbb{N}$, not a proved theorem. Base case $n = 0$ returns the identity map on signals. Successor case composes the one-step shift with the already-defined $n$-fold iterate. No tactics or lemmas; the body is the standard recursive pattern for operator powers.
why it matters
This is the primitive that makes the 8-tick clock speakable as $T^n$. Downstream, shift_period_8 states $T^8 f = f$ for every signal, proving the fundamental periodicity of the recognition clock. The master ComplexStructureCertificate records that periodicity as its first field, then chains T5–T8 through the imaginary eigenvalue $i$, the obstruction $x^2+1 \neq 0$ on ℝ, DFT-8 unitarity, and J-cost phase invariance.
In the unified forcing chain, the T7→canonical-carrier and T7→canonical-shift bridges name Signal8 and the period-8 law built from these iterates, closing the gap from eight-tick forcing to the complex Hilbert carrier needed for genuine unitarity. Framework landmarks: T7 (eight-tick octave), T8 ($D=3$), and the module thesis that complex structure is forced by cost plus 8-tick, not chosen.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.