Pith. sign in
module module moderate

IndisputableMonolith.Foundation.OperatorCore.ComplexStructureForcing

show as:
view Lean formalization →

Authoritative OperatorCore alias of the 8-tick complex carrier developed in Foundation.ComplexStructureForcing. It packages the cyclic shift on eight-slot ledger signals, its DFT eigenbasis, and the complex J-cost on modes so downstream OperatorCore material can cite one stable import. The mathematical content is the forcing argument that the period-8 shift is not diagonalizable over the reals, so complex structure is algebraically required rather than optional.

claimModule alias for the eight-tick complex carrier: the cyclic shift $T$ on $\mathbb{R}^8$ (or $\mathbb{C}^8$) ledger signals, its iterates and period-$8$ law, the DFT/IDFT eigenbasis with eigenvalues $\lambda_k$, the mode inner product, the complexified cost $J_{\mathbb{C}}$, total mode cost, and unitary evolution generated by the shift.

background

Recognition Science fixes an eight-tick octave (forcing step T7): ledger updates close after period $2^3$. The natural linear model is a cyclic shift operator $T$ on an eight-component signal space (siblings: Signal8, nextIdx, shift, shiftIter, shift_period_8).

The upstream module states the core claim: that shift cannot be diagonalized over $\mathbb{R}$, so complexification is forced. Over $\mathbb{C}$ one obtains a DFT eigenbasis (dft8, idft8, eigenvalue) with a Hermitian inner product (inner8). Costs lift via a complex J-cost (JcostC) and a total mode cost; unitary evolution packages the shift as a discrete unitary dynamics on the carrier.

This OperatorCore file is the authoritative IM import path for that carrier, not a second independent development.

proof idea

This is a module alias (re-export / authoritative path) for Foundation.ComplexStructureForcing, not a standalone proof corpus. The mathematical argument lives upstream: start from the period-8 cyclic shift on the eight-tick ledger, show real diagonalization fails, pass to the complex DFT eigenbasis, then define mode costs and unitary evolution in that basis. Local siblings name those objects; proofs are inherited from the imported module.

why it matters in Recognition Science

OperatorCore needs a single stable handle on the complex eight-tick carrier before building higher operators, spectra, or evolution claims. The module sits on the T7 eight-tick landmark and on the upstream forcing line that complex structure is required because the real shift is non-diagonalizable. No downstream used_by edges are recorded here; the value is infrastructural: later OperatorCore and foundation results can import this path for Signal8, DFT modes, JcostC, and UnitaryEvolution without forking the carrier definition. It does not itself close T5–T8; it packages the complex stage those steps presuppose.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (17)