stoneGeneratorCert

The parent module HamiltonianEmergence establishes the scalar foundation: near equilibrium the J-cost is quadratic, $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$, so total cost approximates quadratic energy. It left the operator claim $\hat R=\exp(-i\hat H\cdot 8\tau_0/\hbar)$ as a hypothesis, citing infinite-dimensional Stone theory. That framing is unnecessary: the recognition register is finite-dimensional ($\mathbb{C}^N$ for the eight-tick register), so everything reduces to matrix exponentials already in Mathlib.

A DiscreteEvolution N is a real symmetric $N\times N$ Hamiltonian together with the linearized step $\psi\mapsto\psi-i(H_c\psi)$. The complexified matrix $H_c$ is the real symmetric matrix viewed over $\mathbb{C}$; the generator is $\mathrm{gen}=-i H_c$; the continuous family is $U(t)=\exp(t,\mathrm{gen})$. The certificate structure packages Hermitianness of $H_c$, skew-Hermitianness of $\mathrm{gen}$, the one-parameter group laws, unitarity, and the identity that the discrete step is exactly the first-order truncation $(I+\mathrm{gen})\psi$.

This sits at build-spine HLG-2.1: operator-level content of "quantum mechanics is the high-frequency limit of recognition dynamics," proved outright on $\mathbb{C}^N$ rather than left as a placeholder.

Term-mode structure constructor: each field of StoneGeneratorCert is filled by an already-proved sibling lemma applied to the same ev.

• hamiltonian_hermitian from Hc_isHermitian (real symmetric matrix is self-adjoint over $\mathbb{C}$).
• generator_skewHermitian from gen_skewHermitian (conj-transpose of $-i H_c$ equals its negative).
• evolution_id / one_parameter_group from U_zero and U_add (matrix exponential group laws).
• evolution_unitary / evolution_mem_unitary from U_unitary and U_mem_unitaryGroup.
• discrete_step_is_first_order from step_eq_firstOrder (step equals $(I+\mathrm{gen})\psi$).

No new algebra; pure packaging of the seven component theorems into the certificate Prop.

Closes the operator half of Hamiltonian emergence that HamiltonianEmergence left open. The scalar quadratic approximation of J near identity was already proved; the missing piece was that the linearized recognition step sits inside a genuine unitary one-parameter group generated by a self-adjoint operator. On the finite eight-tick register this is a theorem, not an appeal to infinite-dimensional Stone theory.

Framework role: supports the claim that quantum evolution is the high-frequency limit of recognition dynamics (HLG-2.1). Ties to the eight-tick octave (T7) via the finite register dimension, and to the units bridge $\Delta=8\tau_0/\hbar$ shared with HLG-1.2. The kernel structure (Hermitian generator, unitary group, first-order truncation) is unconditional; what remains conditional is identifying the full nonlinear $\hat R$ with this linear step to $O(\varepsilon^3)$, plus the exact operator Taylor residual and the $\Delta$ calibration.

No downstream users yet (used_by empty); this is the export surface for later modules that need a single named certificate rather than seven separate lemmas.