U_unitary
plain-language theorem explainer
For any discrete-evolution Hamiltonian on C^N, the one-parameter family U(t) = exp(t·gen) is unitary: both U(t)^† U(t) and U(t) U(t)^† equal the identity. Anyone citing finite-dimensional Stone structure for recognition dynamics needs this. The proof is a short rewrite chain: adjoint equals time reversal, group law collapses to U(0), and U(0)=1.
Claim. Let $ev$ be a discrete evolution on $\mathbb{C}^N$ (real symmetric Hamiltonian matrix) and let $U(t)=\exp(t\,\mathrm{gen}(ev))$ be its recognition evolution family. Then for every real $t$, $U(t)^\dagger U(t)=I$ and $U(t)U(t)^\dagger=I$.
background
This module upgrades the scalar Hamiltonian-emergence story to operators on the finite recognition register $\mathbb{C}^N$. A DiscreteEvolution packages a real symmetric $N\times N$ Hamiltonian; its complexification $H_c$ is Hermitian, and the generator $\mathrm{gen}=-i H_c$ is skew-Hermitian. The evolution family is the matrix exponential $U(t)=\exp(t,\mathrm{gen})$.
Upstream, the one-parameter group law $U(s)U(t)=U(s+t)$ and the identity $U(0)=I$ are already proved, as is the adjoint identity $(U(t))^\dagger=U(-t)$ (time reversal). Those three facts are exactly what unitarity needs: left and right products with the adjoint become $U(-t)U(t)=U(0)$ and $U(t)U(-t)=U(0)$.
The local setting is build-spine HLG-2.1: finite-dimensional Stone generator structure for recognition dynamics, without infinite-dimensional Stone theory, because the 8-tick register is finite.
proof idea
Term-mode proof by refine on the two conjuncts. Each side is a four-step rewrite:
- Replace the adjoint by time reversal via
U_conjTranspose: $(U(t))^\dagger=U(-t)$. - Apply the group law
U_addto get $U(-t)U(t)=U(-t+t)$ (resp. $U(t)U(-t)=U(t+(-t))$). - Cancel with
neg_add_cancel/add_neg_cancelto reach $U(0)$. - Finish with
U_zero: $U(0)=I$.
No spectral theory or continuous functional calculus is invoked; everything is matrix algebra on $\mathrm{Fin},N$.
why it matters
Unitarity is the missing piece that places $U(t)$ inside the unitary group of $\mathbb{C}^N$. Downstream, U_mem_unitaryGroup is a one-line packaging of the second conjunct into Mathlib's Matrix.unitaryGroup, and stoneGeneratorCert bundles Hermitian $H_c$, skew-Hermitian generator, $U(0)=I$, and the group law into the Stone-generator certificate (unitarity is the companion fact that makes the certificate physically complete).
In the Recognition framework this is the operator-level content of "quantum mechanics is the high-frequency limit of recognition dynamics": the linearized recognition step sits inside a genuine unitary one-parameter group generated by a self-adjoint Hamiltonian. It closes the finite-dimensional half of the old placeholder that cited Stone's theorem for discrete unitary groups. What remains conditional is the nonlinear identification of full $\hat R$ with this linear step to $O(\varepsilon^3)$, plus the $\Delta=8\tau_0/\hbar$ calibration residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.