U
plain-language theorem explainer
Defines the recognition evolution family as the matrix exponential of real time times the skew-Hermitian generator of a finite-dimensional discrete evolution. Anyone citing the operator-level one-parameter group, unitarity, or first-order truncation of the recognition step uses this object. The body is a direct Mathlib exponential of the scaled generator; no proof content.
Claim. Given a discrete evolution $ev$ on an $N$-dimensional register (real symmetric Hamiltonian matrix) and a real parameter $t$, set $U(ev,t) := \exp\bigl(t\,\mathrm{gen}(ev)\bigr)$ as an $N\times N$ complex matrix, where $\mathrm{gen}(ev)=-i H_c(ev)$ is the complexified skew-Hermitian generator. At the calibrated tick $t=8\tau_0/\hbar$ this is the operator-level recognition step.
background
Module HamiltonianEmergenceOperator discharges build-spine HLG-2.1: the finite-dimensional Stone generator for recognition dynamics. The scalar module already shows $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$ and leaves the operator claim $\hat R=\exp(-i\hat H\cdot 8\tau_0/\hbar)$ as a hypothesis citing infinite-dimensional Stone theory. That framing is unnecessary: the eight-tick register is $\mathbb{C}^N$, so everything is matrix exponentials.
A DiscreteEvolution N packages a real symmetric $N\times N$ Hamiltonian. Its complexification $H_c$ is Hermitian; the generator $\mathrm{gen}(ev)=(-i)\cdot H_c(ev)$ is skew-Hermitian (the $-i\hat H$ in the usual Schrödinger picture). The evolution family is then the standard one-parameter group built from that generator.
RS-native units set $\tau_0=1$ tick and $c=1$; the calibrated step uses $t=8\tau_0/\hbar$ with the eight-tick octave from the forcing chain (T7).
proof idea
Pure definition: cast the real time $t$ to $\mathbb{C}$, scale the generator matrix $\mathrm{gen}(ev)$ by that scalar, and apply Mathlib's matrix exponential exp over $\mathbb{C}$. No lemmas are invoked in the body; subsequent theorems (U_zero, U_add, U_unitary, step_eq_firstOrder) prove the group and unitarity properties of this object.
why it matters
This is the central object of HLG-2.1: the operator-level content of "quantum mechanics is the high-frequency limit of recognition dynamics," stated as a finite-dimensional theorem rather than a Stone-theorem placeholder. Downstream siblings establish $U(ev,0)=1$, the additive group law $U(s)U(t)=U(s+t)$, unitarity and membership in the unitary group, and exact match of the linearized discrete step to the first-order truncation of $U(ev,1)$.
It sits under the forcing-chain landmarks T5 (J-cost) and T7 (eight-tick octave): the calibrated recognition step is $U$ at $t=8\tau_0/\hbar$. What remains conditional is identifying the full nonlinear $\hat R$ with this linearization to $O(\varepsilon^3)$, plus the named residuals on the exponential Taylor bound and the units bridge (same as HLG-1.2). Kernel structure (Hermitian generator, unitary group, first-order truncation) is proved with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.