Pith. sign in
module module high

IndisputableMonolith.Foundation.ComplexStructureForcing

show as:
view Lean formalization →

Constructs the 8-tick signal space and shows the cyclic shift forces complex structure: its DFT eigenvalues include ±i, so x²+1 has no real root on the cycle. Cited by anyone deriving Hilbert carriers, Born measure, or amplitude-linear channels from the recognition clock. Argument is spectral: period-8 shift, DFT-8 diagonalization, and explicit phases at modes 2 and 6.

claimA signal on the eight-tick cycle is a map $s:\{0,\ldots,7\}\to\mathbb{C}$. The cyclic shift acts by $(Ss)_k=s_{k+1\bmod 8}$ and has period $8$. In the DFT-8 eigenbasis its eigenvalues are eighth roots of unity; modes $2$ and $6$ give $+i$ and $-i$. Hence $x^2+1$ has no real root compatible with the shift spectrum, so the carrier must be complex.

background

Recognition Science runs on a discrete eight-tick clock (forcing-chain T7): phases $0,\pi/4,\ldots,7\pi/4$. The EightTick import supplies that clock; DFT8 supplies the primitive root $\omega=e^{-2\pi i/8}$ and the unitary eight-point Fourier basis as the canonical mode decomposition of one octave.

This module introduces Signal8 (maps $\mathrm{Fin},8\to\mathbb{C}$), the one-step index advance, and the cyclic shift with its iterates. Periodicity lemmas close the cycle. Diagonalization against the DFT-8 basis yields pure-phase eigenvalues; two of them are exactly $\pm i$.

Constants and Cost sit in the import background (RS tick $\tau_0$, $J$-cost) but the local work is spectral on the octave, not thermodynamic.

proof idea

Definition layer first: Signal8, next-index, shift and shift-iterates, with period-8 lemmas closing the cycle. Then the DFT-8 basis and the eigenvalue map, identified with powers of $\omega_8$ via the phase-exponential lemma. Direct evaluation at modes 2 and 6 produces $+i$ and $-i$. The capstone records that $x^2+1$ has no real root, so a real carrier cannot host the shift spectrum. Overall structure is definitions plus short algebraic/spectral lemmas, not a long tactic development.

why it matters in Recognition Science

LedgerSuperposition takes Signal8 as the complex Hilbert carrier and the cyclic shift as $\mathbb{C}$-linear (Gravity IV, T1). BornRuleForcing builds the unique phase-invariant, additive sector measure on the same DFT-8 modes, tied to the two-branch $\exp(-C)$ rule. AmplitudeLinearForced uses substrate linearity on this complex structure to force the amplitude-linear gravitational channel (Track 2.C). RecognitionOperator and OperatorCore.ComplexStructureForcing import the same carrier. The module bridges T7 (eight-tick octave) to complex amplitudes without assuming $\mathbb{C}$ by modeling choice.

scope and limits

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (35)