gen
plain-language theorem explainer
Defines the infinitesimal generator of discrete recognition evolution as gen(ev) = -i Hc(ev), the skew-Hermitian matrix that generates the unitary one-parameter group U(t) = exp(t gen). Anyone working the finite-dimensional Stone package (HLG-2.1) cites this. The body is a one-line scalar multiple of the complexified Hamiltonian.
Claim. For a discrete evolution $ev$ on an $N$-dimensional register, the generator is $\mathrm{gen}(ev) := -i\, H_c(ev)$, where $H_c(ev)$ is the complex matrix obtained by viewing the real symmetric Hamiltonian of $ev$ as an element of $M_N(\mathbb{C})$.
background
The parent module upgrades the scalar Hamiltonian-emergence story to operators on the finite register $\mathbb{C}^N$. DiscreteEvolution N packages a real symmetric matrix (the small-strain Hamiltonian) together with the linearized step that applies $\hat R$ in the quadratic regime.
Hc ev is that real matrix viewed over $\mathbb{C}$. Because it is real-symmetric, it is Hermitian; the module then builds the standard finite-dimensional Stone data around it. The scalar precursor only proved $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$ and left $\hat R=\exp(-i\hat H\Delta)$ as a hypothesis citing infinite-dimensional Stone theory. On $\mathbb{C}^N$ that citation is unnecessary: everything is matrix exponentials.
In textbook QM language, if $\hat R=\exp(-i\hat H\Delta)$, the generator of the one-parameter group is $-i\hat H$. That is exactly this definition.
proof idea
Pure definition: scalar multiplication of the complexified Hamiltonian by $-i$ (written (-Complex.I) • Hc ev). No lemmas, no tactics. Downstream theorems (skew-Hermitian property, unitary group laws, first-order truncation identity) consume this matrix as input.
why it matters
Build-spine item HLG-2.1. This is the operator that turns the Hermitian complexification Hc into the skew-Hermitian generator of a unitary one-parameter group. Sibling results immediately prove (gen)^H = -gen, define U ev t = exp(t · gen ev), establish the group laws U 0 = 1 and U s U t = U(s+t), place every U t in the unitary group, and identify the existing discrete step as the first-order truncation (1 + gen) ψ of U 1.
Together these discharge the operator-level claim that was left as a hypothesis in HamiltonianEmergence: small-deviation recognition dynamics is a genuine unitary flow generated by a self-adjoint $\hat H$, as a finite-dimensional theorem rather than a Mathlib-gap placeholder. What remains conditional is only 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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.