StoneGeneratorCert
plain-language theorem explainer
Bundled finite-dimensional Stone certificate for any small-deviation discrete Hamiltonian on $\mathbb{C}^N$: complexified $H$ is Hermitian, $\mathrm{gen}=-iH$ is skew-Hermitian, $U(t)=\exp(t\,\mathrm{gen})$ is a unitary one-parameter group, and the discrete step equals the first-order truncation $(1+\mathrm{gen})$. Cited by anyone using operator-level Hamiltonian emergence (HLG-2.1). As a Prop structure it carries no proof body; the companion theorem discharges each field from named lemmas.
Claim. For $N\in\mathbb{N}$ and any discrete evolution $ev$ (real symmetric Hamiltonian on $N$ bonds), the following hold as one proposition: the complexified Hamiltonian $H_c$ is Hermitian; the generator $\mathrm{gen}=-i H_c$ is skew-Hermitian; the evolution $U(t)=\exp(t\,\mathrm{gen})$ satisfies $U(0)=I$ and $U(s)U(t)=U(s+t)$; every $U(t)$ is unitary and lies in the unitary group on $\mathbb{C}^N$; and the discrete step acts by $(I+\mathrm{gen})\psi$ on deviation states.
background
Module setting is operator-level Hamiltonian emergence (build-spine HLG-2.1). Upstream HamiltonianEmergence already shows the scalar fact that the J-cost near equilibrium is quadratic, $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$, and defines a discrete evolution as a real symmetric matrix $H$ on $N$ bonds together with the linearized step on the deviation Hilbert space $\mathbb{C}^N$.
This module complexifies that matrix to $H_c$ (real entries viewed in $\mathbb{C}$), sets $\mathrm{gen}=-i H_c$, and defines the continuous family $U(t)=\exp(t,\mathrm{gen})$. Because the recognition register is finite-dimensional, matrix exponentials replace infinite-dimensional Stone theory; Mathlib supplies the full API.
The certificate packages the operator claims that make $U$ a genuine unitary one-parameter group generated by a self-adjoint Hamiltonian, with the existing discrete step exactly the first-order truncation of $U(1)$.
proof idea
No proof body: this is a Prop-valued structure whose seven fields are the certificate obligations. The companion theorem stoneGeneratorCert builds an instance by assigning each field to a named lemma: Hermitianness of $H_c$, skew-Hermitianness of $\mathrm{gen}$, $U(0)=I$, the Cauchy law $U(s)U(t)=U(s+t)$, unitarity of each $U(t)$ (both products equal $I$), membership in the unitary group, and equality of the discrete step with $(1+\mathrm{gen})\psi$. Each of those lemmas is proved separately from the matrix-exponential API and the real-symmetric origin of $H$.
why it matters
Closes the operator half of "quantum mechanics is the high-frequency limit of recognition dynamics" as a finite-dimensional theorem rather than a placeholder. Downstream, stoneGeneratorCert asserts the certificate for every discrete-evolution Hamiltonian, so any later argument that needs a self-adjoint generator, a unitary group, or the first-order match can cite a single instance.
Framework landmarks: the eight-tick register supplies the finite $N$ (T7), and the residual calibration $\Delta=8\tau_0/\hbar$ is the same units bridge as HLG-1.2. Honest residual (from the doc-comment): identification of the full nonlinear $\hat R$ with this linearization to $O(\varepsilon^3)$, plus the exact operator $O(\Delta^2)$ Taylor bound, remain named open pieces; the Stone kernel itself is proved with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.