shiftIter
plain-language theorem explainer
Re-export of the n-fold iterate of the cyclic tick-shift on eight-component complex signals. Anyone proving 8-tick periodicity, DFT mode structure, or the T7 carrier/shift bridges cites this operator. The body is a pure alias to the recursive definition (identity at 0, compose with one shift at successor).
Claim. Write $T^{(n)}$ for the $n$-fold composition of the cyclic advance-by-one operator $T$ on signals $f:\mathrm{Fin}\,8\to\mathbb{C}$. Then $T^{(0)}=\mathrm{id}$ and $T^{(n+1)}=T\circ T^{(n)}$.
background
In the complex-structure forcing module, a recognition signal is an eight-slot complex vector Signal8 = Fin 8 → ℂ, the discrete carrier forced by the eight-tick clock (T7). The elementary advance is the cyclic shift $T$ that sends each slot to the next index modulo 8.
shiftIter packages the powers of that shift: zero applications leave the signal alone; each successor composes one more $T$. This is the standard free monoid action of $\mathbb{N}$ on the signal space generated by a single generator $T$.
The local setting is OperatorCore's thin re-export layer over Foundation.ComplexStructureForcing, so downstream certificates can name the iterate without importing the full forcing file.
proof idea
Definitional alias only. The underlying recursive equation is pattern-matched on the natural number: base case identity, inductive step post-compose the single-tick shift. No tactics or lemmas are invoked at this declaration.
why it matters
Periodicity of the recognition clock is stated as $T^{(8)}=\mathrm{id}$ (shift_period_8), which is field periodicity of the master ComplexStructureCertificate. That certificate packages the full chain: J-uniqueness (T5), $\varphi$ (T6), eight-tick and $D=3$ (T7, T8), then $T^8=I$, the mode-2 eigenvalue $\mathrm{i}$, and DFT unitarity.
Unified forcing bridges T7_To_CanonicalCarrier_Bridge and T7_To_CanonicalShift_Bridge name this iterate when they pin the canonical carrier $\mathrm{Fin},8\to\mathbb{C}$ and the cyclic advance against the Spectral layer. Without a named $n$-fold shift, the period-8 law and the spectrum arguments have no operator to quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.