omega8_pow_eq_evolution_factor
plain-language theorem explainer
For each DFT-8 mode index k, the cyclic-shift eigenvalue ω₈^k equals the one-tick Schrödinger phase factor exp(-i E_k τ₀/ℏ), with E_k the quarter-turn energy. Anyone deriving the discrete Schrödinger equation from the eight-tick carrier cites this identification. The proof rewrites ω₈^k via exp(k·(-iπ/4)), unfolds E_k, and cancels τ₀/ℏ by field arithmetic.
Claim. For every mode index $k \in \{0,\ldots,7\}$, $$\omega_8^{k} = \exp\!\Bigl(-i\, E_k\, \tau_0 / \hbar\Bigr),$$ where $\omega_8 = \exp(-i\pi/4)$ and the quarter-turn energy is $E_k = \hbar\,\pi k/(4\tau_0)$.
background
The module derives the Schrödinger equation from the Recognition forcing chain. T7 forces the eight-tick period $2^D$ with $D=3$, so the carrier is Signal8 = Fin 8 → ℂ and the one-tick recognition operator acts as cyclic shift. The DFT-8 basis diagonalizes that shift: mode $k$ has eigenvalue $\omega_8^k = \exp(-i\pi k/4)$.
Hamiltonian extraction identifies that eigenvalue with a one-tick Schrödinger phase. The quarter-turn energy is defined so that $E_k = \hbar,\pi k/(4\tau_0)$. In RS-native units one has $\hbar = \varphi^{-5}$ and $\tau_0 = 1$ (the fundamental tick), with both positive by the constant lemmas used here.
This declaration is table entry 2 in the module: the pure algebraic bridge between the geometric root of unity and the integrated evolution factor $\exp(-i E_k \tau_0/\hbar)$.
proof idea
Tactic proof in two blocks. First, expand $\omega_8$ and apply Complex.exp_nat_mul to obtain
$$\omega_8^{k} = \exp\bigl(k\cdot(-i\pi/4)\bigr).$$
Rewrite the goal with that identity, then congr 1 on the exponents. Unfold the quarter-turn energy $E_k = \hbar,\pi k/(4\tau_0)$. Non-vanishing of $\hbar$ and $\tau_0$ in $\mathbb{C}$ follows from the real positivity lemmas by exact_mod_cast. After push_cast, field_simp cancels the factors and matches $-i E_k \tau_0/\hbar$ with $k\cdot(-i\pi/4)$.
why it matters
This is the Hamiltonian-extraction step in the five-step Schrödinger derivation: without $\omega_8^k = \exp(-i E_k \tau_0/\hbar)$, the cyclic-shift spectrum never becomes an energy spectrum. Downstream, discrete_schrodinger_eigenmode rewrites the scaled eigenmode evolution through this identity to get the exact one-tick flow $\psi(\tau_0) = \exp(-i E_k \tau_0/\hbar),\psi(0)$. The same lemma is stored as phase_factor in schrodingerEquationCert.
In the unified forcing chain it is the phase_factor field of t7_t8_to_canonical_schrodinger_bridge_holds, so T7 (eight-tick octave) plus T8 ($D=3$) land on a canonical Schrödinger bridge only after this equality. Framework landmarks: T7 eight-tick period, DFT-8 diagonalization, and RS-native $\hbar=\varphi^{-5}$. No sorry remains; the continuum Taylor step sits later in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.