for
plain-language theorem explainer
On the finite 8-tick register C^N, the complexified small-deviation Hamiltonian is Hermitian, its generator -iH is skew-Hermitian, and the matrix exponential is a unitary one-parameter group whose first-order truncation recovers the discrete evolution step. Anyone citing operator-level Hamiltonian emergence (HLG-2.1) or the claim that quantum evolution is the high-frequency limit of recognition dynamics would land here. Status is scaffolding: the extracted declaration is a sorry stub with empty proof body.
Claim. For a discrete-evolution Hamiltonian on $\mathbb{C}^N$ (the finite 8-tick recognition register), let $H_c$ be its complexification (real symmetric matrix viewed over $\mathbb{C}$). Then $H_c$ is Hermitian, $G:=-i H_c$ is skew-Hermitian, $U(t):=\exp(t G)$ satisfies $U(0)=I$ and $U(s)U(t)=U(s+t)$, each $U(t)$ is unitary, and the discrete step $\psi\mapsto\psi-i H_c\psi$ equals the first-order truncation $(I+G)\psi$ of $U(1)$.
background
Build-spine item HLG-2.1. The sibling module HamiltonianEmergence already gives the scalar story: near equilibrium the J-cost is quadratic, $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$, so total cost approximates a quadratic energy. The operator claim $R\text{-hat}=\exp(-i H\text{-hat}\cdot 8\tau_0/\hbar)$ was left as a hypothesis, wrongly framed as needing Stone's theorem for discrete unitary groups.
The recognition register is finite-dimensional ($\mathbb{C}^N$), so only matrix exponentials are required. In-module, $H_c$ is the real symmetric discrete Hamiltonian viewed over $\mathbb{C}$; the evolution family is $U(t)=\exp(t\cdot G)$ with $G=-i H_c$. RS-native units enter the calibration residual: $\hbar=\varphi^{-5}$, $\tau_0=1$ tick, and the eight-tick octave fixes the intended step size $\Delta=8\tau_0/\hbar$.
Upstream cost algebra supplies the shifted cost $H(x)=J(x)+1=\frac12(x+x^{-1})$, under which the Recognition Composition Law becomes d'Alembert's equation. That scalar structure is what the operator linearization is meant to lift.
proof idea
Empty proof body: sorry_stub scaffolding. The intended route (visible from sibling names and the module plan) is pure finite-dimensional matrix calculus, not infinite-dimensional Stone theory.
Planned steps: (1) Hermitianness of $H_c$ from real symmetry of ev.hamiltonian; (2) skew-Hermitianness of $G=-i H_c$; (3) one-parameter group laws for $U(t)=\exp(t G)$ via the Mathlib matrix exponential API ($U(0)=I$, $U(s)U(t)=U(s+t)$); (4) unitarity and membership in Matrix.unitaryGroup; (5) exact match of DiscreteEvolution.step with the first-order truncation $(I+G)\psi$ of $U(1)$. None of those steps are discharged in this declaration.
why it matters
This is the operator-level content of "quantum mechanics is the high-frequency limit of recognition dynamics": a self-adjoint generator and a unitary one-parameter group on the 8-tick register, tying T7 (eight-tick octave) to the Hamiltonian picture. The module doc marks the Stone-generator kernel (Hermitian $H_c$, unitary $U(t)$, first-order truncation) as the theorem to prove, while the full nonlinear $R\text{-hat}\approx$ linear step to $O(\varepsilon^3)$ stays conditional on totalJcost_approx_quadratic, the modeling choice that $R\text{-hat}$ linearizes to step, the operator $O(\Delta^2)$ Taylor residual, and the $\Delta=8\tau_0/\hbar$ units bridge (same residual family as HLG-1.2).
Downstream action and Hamiltonian material (conjugate momentum, Hamilton equations, geodesic/Euler–Lagrange structure, action convexity) sits on this generator picture once closed. Until the stub is replaced by the sibling lemmas (Hc Hermitian, gen skew-Hermitian, $U$ group and unitary, step equals first order), HLG-2.1 remains an open spine item rather than a finished finite-dimensional theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.