Signal8
plain-language theorem explainer
The eight-tick carrier is the type of complex maps on a discrete cycle of length 8. It is the Hilbert-space stand-in forced by the T7 octave (period 2^3 with D=3) and is the ambient space for the recognition operator and its DFT-8 eigenmodes. Anyone citing the discrete Schrödinger flow or Hamiltonian extraction in this module uses this type. The declaration is a pure type synonym with no proof content.
Claim. Write $\mathrm{Signal}_8$ for the type of maps $\{0,1,\ldots,7\}\to\mathbb{C}$. Equivalently, $\mathrm{Signal}_8=\mathbb{C}^8$ with coordinates indexed by the eight-tick recognition cycle.
background
The module derives the Schrödinger equation $i\hbar\partial_t\psi=\hat H\psi$ from the Recognition Science forcing chain in five kernel-checked steps. Step 1 is the passage from T7 (the eight-tick octave, period $2^D$ with $D=3$) to a finite carrier: complex amplitudes on eight discrete ticks.
The fundamental time quantum is the tick $\tau_0=1$ in RS-native units. One octave is eight ticks. The one-tick recognition update on this carrier is the cyclic shift of the eight slots; that operator is later diagonalized by the DFT-8 basis (step 2), yielding eigenvalues $\omega_8^k=\exp(-i\pi k/4)$.
This abbreviation exists only to keep later signatures readable. It does not encode dynamics; dynamics enter when the cyclic shift and the eigenmode lemmas act on elements of this type.
proof idea
Pure definitional abbreviation: the type is identified with Fin 8 → ℂ. No tactics, no lemmas, no proof obligations. Downstream lemmas treat elements as eight-component complex vectors and apply the spectral cyclic-shift operator componentwise in the DFT-8 basis.
why it matters
This is the first concrete object in the module's five-step derivation: "T7 → Signal8. The 8-tick recognition period $2^D$ ($D=3$) forces the carrier, and the one-tick recognition operator acts as cyclic shift on this carrier." Every subsequent statement in the table (exact eigenmode evolution, $\omega_8^k$ as Schrödinger phase factor, discrete Schrödinger flow, Hermitian nonnegative quarter-turn energies, and linear superposition) is typed over this space.
In the broader framework it is the finite-dimensional stage on which T7 (eight-tick octave) and the complex-structure forcing that selects DFT-8 become operational. Hamiltonian eigenvalues are later read off as $E_k=\hbar\cdot\pi k/(4\tau_0)$ with RS-native $\hbar=\phi^{-5}$ and $\tau_0=1$. Without fixing the carrier, the discrete-to-continuum Schrödinger limit has nowhere to live.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.