Hc_isHermitian
plain-language theorem explainer
Any discrete-evolution Hamiltonian, once complexified entrywise to a matrix over C, is Hermitian. Citation target for anyone building the finite-dimensional Stone generator on the recognition register C^N. The proof is a matrix extensionality check: conjugate transpose reduces to the real symmetry field of DiscreteEvolution.
Claim. Let $N\in\mathbb{N}$ and let $ev$ be a discrete evolution on the $N$-dimensional register, i.e. a real matrix $H$ with $H_{ij}=H_{ji}$ for all indices. Write $H^{\mathbb{C}}$ for the same matrix with entries viewed in $\mathbb{C}$. Then $H^{\mathbb{C}}$ is Hermitian: $(H^{\mathbb{C}})^{\dagger}=H^{\mathbb{C}}$.
background
The parent module upgrades the scalar Hamiltonian-emergence story to operators on the finite recognition register $\mathbb{C}^N$. Scalar work already shows $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$ near equilibrium; the operator claim is that small-deviation recognition evolution is a unitary one-parameter group generated by a self-adjoint $\hat H$, without infinite-dimensional Stone theory.
A DiscreteEvolution N packages a real matrix hamiltonian together with the field symmetric asserting $H_{ij}=H_{ji}$. The complexification $H_c$ is that same matrix with entries cast to $\mathbb{C}$. Hermiticity of $H_c$ is the first kernel fact needed before defining the generator $\mathrm{gen}=-i,H_c$ and the matrix exponential family $U(t)=\exp(t,\mathrm{gen})$.
Upstream, the structure only contributes the real symmetry hypothesis; no cost-functional identities are used at this step.
proof idea
Unfold Hermiticity as equality of the conjugate transpose with the matrix itself. Extensionality on indices $(i,j)$ reduces both sides to scalar entries. Simplification of conjugate-transpose and of the complexification map, plus Complex.conj_ofReal, leaves a real equality. That equality is exactly ev.symmetric j i (symmetry of the real Hamiltonian, indices swapped by the transpose). norm_cast closes the real-to-complex coercion.
why it matters
This is the first bullet of the finite-dimensional Stone package (build-spine HLG-2.1). Downstream, gen_skewHermitian quotes it to prove $(\mathrm{gen})^{\dagger}=-\mathrm{gen}$; stoneGeneratorCert records it as the hamiltonian_hermitian field; and operator_level_hamiltonian_emergence packages Hermiticity, skew-Hermiticity, the one-parameter group laws, unitarity, and first-order truncation of the discrete step into one statement.
In Recognition Science terms it converts the modeling slogan "quantum mechanics is the high-frequency limit of recognition dynamics" into a matrix theorem on the eight-tick register: a real symmetric cost Hessian becomes a genuine self-adjoint $\hat H$. What remains conditional is only the identification of the full nonlinear $\hat R$ with this linear step to $O(\varepsilon^3)$, plus the $\Delta=8\tau_0/\hbar$ units bridge, not the generator algebra itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.