U_zero
plain-language theorem explainer
At time zero the recognition evolution family is the identity matrix: U(ev,0)=I on C^N. Cited by anyone assembling the finite-dimensional Stone generator or the unitary one-parameter group. The proof unfolds the matrix exponential and applies exp(0)=1 after the zero scalar multiple collapses.
Claim. For every discrete evolution $ev$ on the $N$-dimensional recognition register, the evolution family satisfies $U(ev,0)=I$, where $U(ev,t)=\exp(t\cdot\mathrm{gen}(ev))$ and $\mathrm{gen}(ev)=-i\,H_c(ev)$.
background
This module upgrades the scalar Hamiltonian-emergence story to operators on the finite register $\mathbb{C}^N$ (build-spine HLG-2.1). The scalar layer already shows $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$ near equilibrium; the operator claim is that small-deviation recognition dynamics is a genuine unitary one-parameter group generated by a self-adjoint Hamiltonian, with no infinite-dimensional Stone theory required.
A DiscreteEvolution N packages a real symmetric $N\times N$ Hamiltonian matrix. Its complexification $H_c$ is Hermitian, and the generator is $\mathrm{gen}(ev)=-i,H_c(ev)$ (skew-Hermitian). The evolution family is the matrix exponential
$U(ev,t)=\exp(t\cdot\mathrm{gen}(ev))$.
At the calibrated tick $t=8\tau_0/\hbar$ this is the operator-level recognition step. The present lemma is the identity endpoint of that family.
proof idea
One short tactic proof. Unfold the definition $U(ev,t)=\exp((t:\mathbb{C})\bullet\mathrm{gen}(ev))$. Rewrite $0:\mathbb{R}$ to $0:\mathbb{C}$, so the scalar multiple is the zero matrix; then exp_zero gives $\exp(0)=I$. No structural facts about $ev$ are used beyond the type of gen.
why it matters
Identity at $t=0$ is the first half of the one-parameter group law required for finite-dimensional Stone structure. Downstream, stoneGeneratorCert records it as evolution_id; operator_level_hamiltonian_emergence packages it into the one-statement summary that $U(ev,t)=\exp(t\cdot(-i\hat H))$ is a unitary group generated by self-adjoint $\hat H$ with discrete step equal to the first-order truncation. U_unitary also rewrites through $U_zero$ after conjugating and cancelling $t+(-t)$.
In the Recognition framework this closes the operator half of "quantum mechanics is the high-frequency limit of recognition dynamics" on the eight-tick register, turning a former hypothesis (Stone for discrete unitary groups) into a kernel theorem. Residual conditionality sits only in the nonlinear $O(\varepsilon^3)$ identification of full $\hat R$ with the linear step and the $\Delta=8\tau_0/\hbar$ units bridge, not in this identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.