Signal8
plain-language theorem explainer
Local type alias for the eight-tick analytic signal carrier, identified with the canonical Foundation carrier from complex-structure forcing. Gravity authors cite it as the single-site Hilbert factor inside the macroscopic ledger tensor product. The body is a pure abbreviation with no proof obligations.
Claim. Write $\mathrm{Signal}_8$ for the eight-tick analytic signal carrier type, identified with the canonical carrier forced by complex structure in the Recognition foundation.
background
Track 2.A of Gravity IV upgrades the macroscopic ledger Hilbert carrier from a paper-level conditional claim to a structural Lean theorem. The single-site factor is the eight-tick analytic signal space: the carrier on which the one-tick recognition update (cyclic shift) acts $\mathbb{C}$-linearly, as already established for the single-site ledger superposition.
In Recognition Science the fundamental evolution period is the eight-tick octave (forcing chain T7, period $2^3$). The module builds the multi-site carrier as the finite $\iota$-fold Pi tensor product over $\mathbb{C}$ of these $\mathrm{Signal}_8$ factors, then lifts the recognition update factorwise via the universal property of the tensor product map.
This abbreviation simply re-exports the foundation carrier into the gravity namespace so the macroscopic construction can name the single-site type without a long qualified path.
proof idea
Definitional abbreviation only: the type is definitionally equal to the canonical Signal8 from Foundation.ComplexStructureForcing. No tactics, no lemmas, no obligations.
why it matters
Without a named single-site carrier, the macroscopic ledger
$$\mathrm{MacroscopicLedger}:=\bigotimes_{i\in\iota}^{\mathbb{C}}\mathrm{Signal}_8$$
cannot be stated. Paper IV Theorem 1 (ledger superposition) is already unconditional at one site; Track 2.A needs the same carrier at every tensor factor so that multi-site superpositions remain physical and are preserved by recognition. The eight-tick structure is the T7 octave landmark. Downstream siblings (MacroscopicLedger, MacroscopicShift, cyclic-shift linearity) all consume this alias. The module reports zero sorry and zero RS-internal axioms for the structural upgrade.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.