Pith. sign in
module module moderate

IndisputableMonolith.Foundation.SchrodingerDerivation

show as:
view Lean formalization →

Derives discrete Schrödinger evolution on the eight-tick recognition cycle from the DFT-8 eigenbasis. Introduces the complex carrier Signal8, proves the one-tick cyclic shift is ℂ-linear, and matches eigenmode phases to powers of ω₈ with a nonnegative quarter-turn energy. Forcing-chain and ledger-superposition modules import it for the quantum channel. The argument is spectral: exact eigenmode evolution under cyclic shift plus energy identities.

claimOn the eight-tick carrier $\mathbb{C}^8$, the one-tick cyclic shift acts on the $k$-th DFT eigenmode by multiplication by $\omega_8^k$ ($\omega_8 = e^{-2\pi i/8}$), giving a discrete Schrödinger law with nonnegative quarter-turn energy spectrum tied to the RS tick $\tau_0 = 1$.

background

Recognition Science fixes an eight-tick octave (period $2^3$) as the minimal closed recognition cycle. The DFT-8 module supplies the canonical unitary basis: the primitive root $\omega_8 = e^{-2\pi i/8}$ and the associated eight eigenmodes of the cyclic shift on length-8 signals.

This module works in RS-native units where the fundamental time quantum is $\tau_0 = 1$ tick (from Constants). The state space is the complex 8-vector carrier (Signal8). The one-tick update is the cyclic shift; the spectral picture identifies each DFT mode's evolution factor with a power of $\omega_8$.

Quarter-turn energy is the natural nonnegative cost associated to a $\pi/2$ phase step on that lattice, linking the discrete unitary evolution to an energy observable used downstream in the quantum channel.

proof idea

Definition layer first: Signal8 as the $\mathbb{C}^8$ carrier, cyclic shift as the one-tick update, and quarterTurnEnergy as a real nonnegative functional (with zero/positivity lemmas).

Linearity is proved directly: cyclic shift respects scalar multiplication and addition over $\mathbb{C}$. Eigenmode lemmas then show exact evolution: each DFT mode picks up the factor $\omega_8^k$, with a scaled variant and the identity equating $\omega_8$ powers to the evolution factor.

The capstone discrete_schrodinger_eigenmode packages that spectral action as the discrete Schrödinger statement on eigenmodes. No continuous PDE analysis; everything is finite-dimensional unitary dynamics on the eight-tick lattice.

why it matters in Recognition Science

Feeds two load-bearing parents. UnifiedForcingChain imports it inside the T0–T8 inevitability argument from the cost foundation (Recognition Composition Law), where the eight-tick octave (T7) and discrete quantum evolution sit on the forcing spine.

LedgerSuperposition (Gravity IV, Theorem 1) uses Signal8 as the complex Hilbert carrier and the proved $\mathbb{C}$-linearity of cyclic_shift for ledger superposition and the quantum channel. Without this module, the discrete Schrödinger bridge from DFT-8 to gravity's recognition state space is missing.

Landmark tie-in: T7 eight-tick octave and the DFT-8 backbone; the energy lemmas support cost-gradient readings of the same update.

scope and limits

used by (2)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (22)