Signal8
plain-language theorem explainer
Local name for the eight-tick complex signal space Fin 8 → ℂ, the Hilbert carrier of ledger configurations in the Gravity IV quantum-channel development. Anyone citing ledger superposition or the recognition update on coherent states uses this type. The body is a pure re-export of the canonical Foundation carrier; no new construction.
Claim. Write $\mathrm{Signal}_8$ for the type of maps $\mathrm{Fin}\,8\to\mathbb{C}$, identified with the canonical eight-tick analytic signal carrier from the complex-structure forcing development.
background
The module Gravity IV anchors two load-bearing results of Gravity from Recognition IV: The Quantum Channel. Theorem 1 (Ledger Superposition) treats the recognition state space as a complex Hilbert carrier on which the one-tick update is $\mathbb{C}$-linear and inner-product preserving, so coherent superpositions of definite ledger configurations are physical and stable under update. Theorem 2 concerns unique linear extension of classical density-to-gravity maps.
In the Recognition forcing chain, T7 fixes the eight-tick octave (period $2^3$). The analytic signal on that discrete clock is a function $\mathrm{Fin},8\to\mathbb{C}$. Foundation.ComplexStructureForcing supplies the canonical such carrier; this module only rebinds it under a short local name so the gravity proofs can speak of ledger states without long qualified paths.
Sibling material in the same file equips the carrier with the canonical Hermitian product and proves that the cyclic one-tick recognition update preserves that product, which is the mathematical content of T1.
proof idea
Definitional abbreviation only: the right-hand side is the existing Foundation.ComplexStructureForcing signal type. No tactics, no lemmas, no new data.
why it matters
Without a named eight-tick complex carrier, the ledger-superposition statement cannot even be typed. The module doc makes $\mathrm{Signal}_8$ the state space for T1: coherent superpositions of ledger configurations live here, and the recognition update must act $\mathbb{C}$-linearly while preserving the canonical inner product. That is the quantum-channel half of Gravity IV; T2 then extends classical cost-gradient maps by free linear extension on the same linear structure.
Framework landmark: T7 (eight-tick octave). The construction reuses Foundation.ComplexStructureForcing, SchrodingerDerivation, and RecognitionOperator and introduces no new RS-internal axioms. Downstream siblings (inner product, preservation under cyclic shift, the packaged LedgerSuperpositionTheorem) are the actual theorems; this abbrev is the shared type they all mention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.