operator_level_hamiltonian_emergence
plain-language theorem explainer
On the finite-dimensional recognition register ℂ^N, small-deviation evolution is a unitary one-parameter group generated by a self-adjoint Hamiltonian, and the discrete recognition step is exactly its first-order truncation. Anyone citing the operator-level content of quantum mechanics as the high-frequency limit of recognition dynamics would use this. The proof is a term-mode conjunction packaging six already-proved component lemmas on Hermiticity, skew-Hermiticity, group laws, unitarity, and first-order match.
Claim. For any discrete evolution on $N$ bonds with real symmetric Hamiltonian matrix $H$, write $H_{\mathbb{C}}$ for its complexification, $G=-i H_{\mathbb{C}}$, and $U(t)=\exp(t G)$. Then $H_{\mathbb{C}}$ is Hermitian, $G^\dagger=-G$, $U(0)=I$, $U(s)U(t)=U(s+t)$ for all real $s,t$, every $U(t)$ lies in the unitary group $U(N)$, and the discrete step acts by $\psi\mapsto(I+G)\psi$.
background
The module discharges build-spine item HLG-2.1 (operator-level Hamiltonian emergence). The sibling module HamiltonianEmergence already proves the scalar foundation: near equilibrium the J-cost is quadratic, $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$, and total cost approximates quadratic energy. It left the operator claim $\hat R=\exp(-i\hat H\cdot 8\tau_0/\hbar)$ as a hypothesis, citing Stone's theorem for discrete unitary groups. That framing is unnecessary: the recognition register is finite-dimensional ($\mathbb{C}^N$ for the eight-tick register), so matrix exponentials and Mathlib's finite-dimensional API suffice.
A DiscreteEvolution packages a real symmetric $N\times N$ Hamiltonian. Its complexification $H_{\mathbb{C}}$ is that matrix viewed over $\mathbb{C}$. The generator is $G=-i H_{\mathbb{C}}$. The evolution family is $U(t)=\exp(t G)$. DeviationHilbert is simply $\mathbb{C}^N$ with the standard inner product. The discrete step already defined upstream is the linearized map $\psi\mapsto\psi-i(H_{\mathbb{C}}\psi)$, which this theorem identifies with the first-order truncation $(I+G)\psi$ of the exponential.
proof idea
Pure term-mode packaging: the proof is the six-tuple of already-proved component lemmas
⟨Hc_isHermitian, gen_skewHermitian, U_zero, U_add, U_mem_unitaryGroup, step_eq_firstOrder⟩.
Hermiticity of the complexified Hamiltonian is the standard fact that a real symmetric matrix is self-adjoint over $\mathbb{C}$. Skew-Hermiticity of the generator follows by conjugating the factor $-i$. The identity $U(0)=I$ and the cocycle $U(s)U(t)=U(s+t)$ are the matrix-exponential group laws. Membership in the unitary group uses that a skew-Hermitian generator produces unitary one-parameter orbits. The last conjunct equates the discrete step with the first-order truncation $(I+G)\psi$ of $\exp(G)$.
why it matters
This is the operator-level content of "quantum mechanics is the high-frequency limit of recognition dynamics", stated as a finite-dimensional theorem rather than a placeholder. It closes the gap left by HamiltonianEmergence, which had the scalar quadratic foundation but left $\hat R$'s operator form as a hypothesis citing infinite-dimensional Stone theory. Framework landmarks: the eight-tick octave (T7) fixes the finite register picture that makes the finite-dimensional argument available; the result supplies the self-adjoint generator and unitary group structure that any later identification of recognition dynamics with Schrödinger evolution must use.
Honest residual (from the module doc): the Stone-generator kernel is proved, but identification of the full nonlinear $\hat R$ with this linear step to $O(\varepsilon^3)$ still rests on the proved scalar bound totalJcost_approx_quadratic plus the modeling choice that $\hat R$ linearizes to step. The exact operator $O(\Delta^2)$ exponential Taylor bound and the $\Delta=8\tau_0/\hbar$ calibration remain named residuals (same units bridge as HLG-1.2). No downstream dependents are wired yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.