U_conjTranspose
plain-language theorem explainer
The conjugate transpose of the recognition evolution matrix equals the evolution run backward in time: adjoint of U(t) is U(-t). Anyone proving unitarity of the finite-dimensional recognition step cites this identity. The proof is a short matrix calculation: skew-Hermitianness of the generator plus the fact that exp commutes with conjugate transpose.
Claim. For any discrete evolution $ev$ on $\mathbb{C}^N$ and any real time $t$, the conjugate transpose of the evolution matrix satisfies $(U_{ev}(t))^H = U_{ev}(-t)$, where $U_{ev}(t) = \exp(t\,\mathrm{gen}(ev))$ and $\mathrm{gen}(ev)$ is the skew-Hermitian generator $-i H_c(ev)$.
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 matrix; 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})$.
Because the register is finite-dimensional, Mathlib's matrix exponential API replaces infinite-dimensional Stone theory. The module already records that $\mathrm{gen}$ is skew-Hermitian (gen_skewHermitian) and that $U$ is a one-parameter group ($U(0)=1$, $U(s)U(t)=U(s+t)$). The adjoint-time-reversal identity is the remaining algebraic link needed for unitarity.
Upstream, the scalar foundation is the quadratic expansion of the J-cost near equilibrium; here that structure is packaged as the real symmetric matrix inside DiscreteEvolution, then complexified.
proof idea
First prove the generator identity $(t,\mathrm{gen})^H = (-t),\mathrm{gen}$. Conjugate transpose pulls out of scalar multiplication; gen_skewHermitian replaces $\mathrm{gen}^H$ by $-\mathrm{gen}$; real $t$ is fixed by conjugation, and the signs rearrange to $(-t),\mathrm{gen}$.
Unfold $U$ as $\exp(t,\mathrm{gen})$. Apply Mathlib's Matrix.exp_conjTranspose so that $(\exp(A))^H = \exp(A^H)$, then substitute the generator identity. The result is $\exp((-t),\mathrm{gen}) = U(-t)$.
why it matters
This is the adjoint half of the finite-dimensional Stone package (build-spine HLG-2.1). Downstream, U_unitary applies it twice: $(U(t))^H U(t) = U(-t)U(t) = U(0) = 1$ and the opposite order, using the already-proved group law U_add and U_zero. That unitarity places every $U(t)$ in the unitary group and justifies reading the recognition step as a genuine unitary one-parameter group generated by a self-adjoint Hamiltonian.
In the Recognition framework this is the operator-level content of "quantum mechanics is the high-frequency limit of recognition dynamics" on the eight-tick register, without invoking infinite-dimensional Stone theory. The remaining conditional layer is not this identity; it is the modeling claim that the full nonlinear $\hat R$ linearizes to the discrete step at $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.