step_eq_firstOrder
plain-language theorem explainer
On the finite-dimensional recognition register, the discrete evolution step equals the first-order Euler truncation of the unitary group: applying (1 + gen) to the state recovers the step exactly. Anyone citing the finite-dimensional Stone generator or the operator-level Hamiltonian emergence certificate needs this identity. The proof is a componentwise matrix calculation: expand mulVec, unwind gen = -i Hc, and finish by ring.
Claim. For any discrete-evolution Hamiltonian $ev$ on the $N$-dimensional recognition register and any small-deviation state $\psi$, the discrete step equals the first-order truncation of the unitary evolution: $\mathrm{step}(ev,\psi) = (I + \mathrm{gen}(ev))\,\psi$, where $\mathrm{gen}(ev) = -i\,\widehat{H}(ev)$ is the skew-Hermitian generator of $U(t) = \exp(t\,\mathrm{gen}(ev))$.
background
This module (build-spine HLG-2.1) upgrades the scalar Hamiltonian-emergence story to operators on the finite register $\mathbb{C}^N$. The scalar layer already shows $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$ near equilibrium; the operator claim is that the recognition tick linearizes to a genuine unitary one-parameter group generated by a self-adjoint $\widehat{H}$.
The complexified small-deviation Hamiltonian $H_c(ev)$ is the real symmetric matrix of $ev$ viewed over $\mathbb{C}$. The generator is $\mathrm{gen}(ev)=-i,H_c(ev)$, and the evolution family is $U(ev,t)=\exp(t,\mathrm{gen}(ev))$. The discrete step already defined upstream is $\mathrm{step}(ev,\psi)=\psi-i,(H_c(ev),\psi)$: the Euler update for one tick.
Because the register is finite-dimensional, no infinite-dimensional Stone theory is required; matrix exponentials and the Mathlib unitary-group API suffice. The RS-native constants $\hbar=\varphi^{-5}$ and $\tau_0=1$ enter only the calibrated tick $t=8\tau_0/\hbar$ for the full recognition step, not this algebraic identity.
proof idea
Pointwise on components via funext. Expand $(I+\mathrm{gen})\psi$ with Matrix.add_mulVec and Matrix.one_mulVec, so the $i$-th entry is $\psi_i+(\mathrm{gen},\psi)_i$.
Unwinding gen and $H_c$ shows $(\mathrm{gen},\psi)i=\sum_j(-i),(H{ij}\psi_j)$; pull the scalar out of the sum. The goal reduces to
$\psi_i-i\sum_j H_{ij}\psi_j=\psi_i+(-i)\sum_j H_{ij}\psi_j$,
which is immediate by ring. No spectral theory or exponential series is used: pure matrix arithmetic matching the upstream definition of step.
why it matters
This is the last algebraic link in the finite-dimensional Stone package: it identifies the existing discrete step with the first-order truncation of $U(ev,1)=\exp(\mathrm{gen}(ev))$. Downstream, stoneGeneratorCert packages it as discrete_step_is_first_order, and operator_level_hamiltonian_emergence quotes the same clause in its one-statement summary (Hermitian $H_c$, skew-Hermitian gen, one-parameter unitary group, and step $=(I+\mathrm{gen})\psi$).
In the Recognition framework this is the operator content of "quantum mechanics is the high-frequency limit of recognition dynamics" on the eight-tick register (T7), without invoking infinite-dimensional Stone. The kernel (Hermitian generator, unitary group, first-order match) is a proved theorem. Residuals remain: full nonlinear $\widehat{R}$ equals this linearization only to $O(\varepsilon^3)$, and the exact $O(\Delta^2)$ Taylor bound plus the $\Delta=8\tau_0/\hbar$ calibration stay named (same units bridge as HLG-1.2).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.