U_mem_unitaryGroup
plain-language theorem explainer
For any discrete evolution on the finite recognition register C^N and any real time t, the matrix-exponential evolution U(t)=exp(t·gen) lies in the unitary group U(N). Cite this when assembling the operator-level Stone generator package or the one-statement Hamiltonian-emergence theorem. The proof is a two-line rewrite: unpack Mathlib's unitary-group membership and apply the already-proved unitarity identities for U.
Claim. For every discrete evolution $ev$ on $\mathbb{C}^N$ (given by a real symmetric Hamiltonian matrix) and every real time $t$, the evolution operator $U(ev,t):=\exp(t\cdot\mathrm{gen}(ev))$ belongs to the unitary group $\mathrm{U}(N,\mathbb{C})$.
background
The module supplies the finite-dimensional Stone generator that HamiltonianEmergence left open. Scalar work already shows the J-cost near equilibrium is quadratic, $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$, but the operator claim that the recognition step is a unitary one-parameter group generated by a self-adjoint Hamiltonian was only a hypothesis, framed as needing infinite-dimensional Stone theory. On the finite 8-tick register $\mathbb{C}^N$ that framing is unnecessary: everything is matrix exponentials with full Mathlib support.
A DiscreteEvolution packages a real symmetric $N\times N$ Hamiltonian. Its complexification $H_c$ is Hermitian, so the generator $\mathrm{gen}=-i H_c$ is skew-Hermitian. The evolution family is the matrix exponential $U(ev,t)=\exp(t\cdot\mathrm{gen})$. Upstream, unitarity of each $U(t)$ is already recorded as the pair of identities $U(t)^\dagger U(t)=1$ and $U(t)U(t)^\dagger=1$. Mathlib's unitary group is the subtype of matrices satisfying those identities under the star operation (conjugate transpose over $\mathbb{C}$).
proof idea
Short tactic proof, not a wrapper of a single named lemma. Rewrite membership with Matrix.mem_unitaryGroup_iff and identify star with conjugate transpose via Matrix.star_eq_conjTranspose. The goal collapses to the second conjunct of the already-proved unitarity statement for $U(ev,t)$, which supplies both $U^\dagger U=1$ and $UU^\dagger=1$. Close by exact.
why it matters
This is one of the five conjuncts in operator_level_hamiltonian_emergence, the one-statement summary of build-spine HLG-2.1: every $U(ev,t)$ lies in the unitary group on $\mathbb{C}^N$. It also feeds stoneGeneratorCert, which bundles Hermitian Hamiltonian, skew-Hermitian generator, identity at zero, the one-parameter group law, and unitary-group membership into a single certificate.
In Recognition Science 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. The eight-tick octave (T7) fixes the register setting; the residual open pieces are the nonlinear $\hat R$ identification to $O(\varepsilon^3)$ and the $\Delta=8\tau_0/\hbar$ calibration, not this membership fact. Lean status remains 0 sorry and 0 new axiom for the kernel structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.