Pith. sign in
module module high

IndisputableMonolith.Foundation.ComplexStructureForcing

show as:
view Lean formalization →

Module that forces complex structure on the eight-tick recognition carrier. Signals are maps Fin 8 → ℂ; the cyclic shift is diagonalized by the DFT-8 basis, and modes 2 and 6 yield eigenvalues i and −i. Irreducibility of x²+1 over ℝ follows, so ℂ is the natural scalar field. Born-rule forcing, ledger superposition, and amplitude-linear gravity import this carrier.

claimA recognition signal on the eight-tick cycle is a map $s:\{0,\ldots,7\}\to\mathbb{C}$. The cyclic shift has DFT-8 eigenvalues $\omega^k$ with $\omega=e^{-2\pi i/8}$; the mode-2 eigenvalue equals $i$ and the mode-6 eigenvalue equals $-i$. Hence $x^2+1$ has no real root, and the natural scalar field of the recognition state space is $\mathbb{C}$.

background

Recognition Science runs on a discrete eight-tick clock (T7 in the forcing chain): phases $0,\pi/4,\ldots,7\pi/4$. The EightTick module supplies that period-$2^3$ structure; Constants fixes the RS time quantum $\tau_0=1$ tick.

DFT8 is the canonical unitary basis for the cycle. Its primitive root is $\omega=e^{-2\pi i/8}$. A signal is a function from Fin 8 into $\mathbb{C}$; the one-tick update is the cyclic shift on that eight-slot register. The shift is diagonal in the DFT basis, with eigenvalues the successive powers of $\omega$.

The Cost import is ambient infrastructure for later Born-weight comparisons; this module itself is spectral and algebraic, not cost-theoretic.

proof idea

Definition layer first: Signal8 as Fin 8 → ℂ, nextIdx and shift (and its iterates) for the cyclic update, with period-8 lemmas. DFT basis vectors are introduced; eigenvalues of the shift are identified with phase factors $\omega^k$ via the standard DFT eigenrelation.

Two concrete evaluations pin the complex structure: the mode-2 eigenvalue equals $i$, and mode 6 equals $-i$. A short algebraic lemma records that $x^2+1$ has no real root, so the pure-imaginary pair cannot live in a real scalar field. The module is mostly definitions plus these spectral identities; no deep tactic proof is required beyond evaluating roots of unity and the quadratic.

why it matters in Recognition Science

This is the foundation step that makes the recognition carrier a complex Hilbert space rather than a real vector space. LedgerSuperposition (Gravity IV, T1) quotes Signal8 as the complex Hilbert carrier and the cyclic shift as ℂ-linear. BornRuleForcing builds the unique phase-invariant sector measure on the same DFT-8 modes. AmplitudeLinearForced (Gravity Track 2.C) needs substrate ℂ-linearity to upgrade the amplitude-linear gravitational channel from model to theorem. OperatorCore.ComplexStructureForcing and RecognitionOperator re-export or refine the same carrier.

In the forcing chain this sits under T7 (eight-tick octave): once the period is $2^3$, the DFT spectrum necessarily contains $i$, forcing complex structure without an extra postulate.

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)