Hc
plain-language theorem explainer
Complexifies the real symmetric Hamiltonian of a discrete evolution into an N-by-N matrix over ℂ by entrywise cast. Anyone proving Hermiticity of the recognition Hamiltonian, building the skew-Hermitian generator, or stating finite-dimensional Stone generation cites it. The body is a one-line Matrix.of coercion from ℝ to ℂ.
Claim. Given a discrete evolution on an $N$-dimensional register whose Hamiltonian is a real symmetric matrix $H$, the complexified Hamiltonian is the matrix $H_{\mathbb{C}}\in M_N(\mathbb{C})$ with entries $(H_{\mathbb{C}})_{ij}=H_{ij}$ viewed in $\mathbb{C}$.
background
The parent module closes build-spine item HLG-2.1: operator-level Hamiltonian emergence on the finite recognition register $\mathbb{C}^N$. Scalar work in HamiltonianEmergence already shows that the J-cost near equilibrium is quadratic, $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 framed via infinite-dimensional Stone theory. Because the 8-tick register is finite-dimensional, matrix exponentials suffice.
Upstream, a discrete evolution packages a real matrix $H:\mathrm{Fin},N\to\mathrm{Fin},N\to\mathbb{R}$ together with a symmetry proof $H_{ij}=H_{ji}$, and defines a linearized step on deviation vectors. The present definition simply promotes that real $H$ to a complex matrix so that Mathlib's Hermitian, skew-Hermitian, and Matrix.exp API apply.
Notation: $H_{\mathbb{C}}$ is written Hc ev in the development; the generator is then $-i H_{\mathbb{C}}$, and the one-parameter family is $U(t)=\exp(t\cdot(-i H_{\mathbb{C}}))$.
proof idea
Pure definition, not a proof. Construct the matrix via Matrix.of whose $(i,j)$-entry is the real number ev.hamiltonian i j coerced to $\mathbb{C}$. No lemmas are applied; the cast is the entire content. Downstream Hermiticity (Hc_isHermitian) then uses that conjugation fixes real scalars and that the source matrix is symmetric.
why it matters
This is the first concrete operator object in the finite-dimensional Stone-generator spine. It is the self-adjoint $\hat H$ that later theorems package: Hc_isHermitian shows $H_{\mathbb{C}}^\dagger=H_{\mathbb{C}}$; gen sets $\mathrm{gen}=-i H_{\mathbb{C}}$; gen_skewHermitian and the unitary one-parameter group $U(t)=\exp(t\cdot\mathrm{gen})$ follow; step_eq_firstOrder identifies the existing discrete step with the Euler truncation $(1+\mathrm{gen})\psi$; and operator_level_hamiltonian_emergence bundles the whole package into one statement.
Framework role: it turns the operator half of "quantum mechanics is the high-frequency limit of recognition dynamics" into a kernel theorem on $\mathbb{C}^N$, aligned with the T7 eight-tick register, without invoking infinite-dimensional Stone theory. What remains conditional is the modeling identification that the full nonlinear $\hat R$ linearizes to this step at $O(\varepsilon^3)$, plus the $\Delta=8\tau_0/\hbar$ units bridge (same residual as HLG-1.2).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.