quarterTurnEnergy_zero
plain-language theorem explainer
The recognition-Hamiltonian eigenvalue on the zeroth DFT-8 mode is exactly zero: the ground-state energy vanishes. Anyone citing the discrete Schrödinger spectrum, Hermitian Ĥ_RS, or energy nonnegativity on the eight-tick register would quote this. The proof is a one-line simplification of the closed-form eigenvalue formula at mode index 0.
Claim. The recognition-Hamiltonian eigenvalue on the zeroth DFT-8 mode vanishes: $E_0 = 0$, where $E_k = \hbar \cdot \pi k/(4\tau_0)$ with RS-native quanta $\hbar=\varphi^{-5}$ and $\tau_0=1$.
background
This module derives the Schrödinger equation from the Recognition forcing chain. T7 forces the eight-tick carrier Signal8 = Fin 8 → ℂ with one-tick operator acting as cyclic shift; the DFT-8 basis diagonalizes that shift with eigenvalues $\omega_8^k = \exp(-i\pi k/4)$.
Identifying $\omega_8^k$ with the Schrödinger phase factor $\exp(-i E_k \tau_0/\hbar)$ yields the recognition-Hamiltonian spectrum $E_k = \hbar \cdot \pi k/(4\tau_0)$. With RS-native units $\hbar = \varphi^{-5}$ and $\tau_0 = 1$, this is $E_k = \varphi^{-5}\cdot\pi k/4$. The definition quarterTurnEnergy is exactly that closed form on Fin 8.
Sibling facts already record that these eigenvalues are real (Hermitian Ĥ) and nonnegative. The present statement isolates the ground mode $k=0$.
proof idea
One-line tactic proof: unfold quarterTurnEnergy and simplify. Substituting $k=0$ gives a factor $(k.\mathrm{val}:\mathbb{R})=0$ in the numerator, so the whole real expression collapses to $0$ independently of $\hbar$, $\pi$, and $\tau_0$.
why it matters
In the module's five-step derivation, energy nonnegativity and Hermiticity of Ĥ_RS are listed as proved items (table rows 4–5). Vanishing ground-state energy $E_0=0$ is the base case of that spectrum: excited modes ($k\ge 1$) are strictly positive by the companion lemma, while the vacuum mode sits at zero.
This matches the discrete Schrödinger picture on the eight-tick octave forced by T7 ($2^D$ with $D=3$): the cyclic-shift generator has a trivial eigenvalue on the constant DFT mode, read off as zero energy after matching phases to $\exp(-i E_k \tau_0/\hbar)$. Downstream linear superposition and continuum recovery inherit a nonnegative Hermitian spectrum with a true ground state.
No further used-by edges are recorded yet; the lemma closes the ground-state slot in the local energy package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.