U_add
plain-language theorem explainer
The recognition evolution family is a one-parameter group: matrix product of evolutions at real times s and t equals evolution at s+t. Anyone citing the finite-dimensional Stone generator, unitarity of U, or the operator-level Hamiltonian emergence summary needs this identity. The proof is a short matrix-exponential argument: scaled generators commute, so Mathlib's exp-add-of-commute applies after unfolding U.
Claim. Let $N\in\mathbb{N}$ and let $\mathrm{ev}$ be a discrete evolution on the $N$-dimensional recognition register (a real symmetric Hamiltonian matrix). Write $U(\mathrm{ev},t)=\exp(t\,\mathrm{gen}(\mathrm{ev}))$ for the complex matrix exponential of the skew-Hermitian generator. Then for all real $s,t$, $U(\mathrm{ev},s)\,U(\mathrm{ev},t)=U(\mathrm{ev},s+t)$.
background
This module upgrades the scalar Hamiltonian-emergence story to operators on the finite register $\mathbb{C}^N$. A DiscreteEvolution packages a real symmetric $N\times N$ Hamiltonian; its complexification $H_c$ is Hermitian, and the generator is $\mathrm{gen}=-i H_c$, which is skew-Hermitian.
The evolution family is defined by $U(\mathrm{ev},t)=\exp(t\cdot\mathrm{gen}(\mathrm{ev}))$ as a complex matrix exponential. For the calibrated tick $t=8\tau_0/\hbar$ this is the operator-level recognition step. The module's point is that finite dimension makes Stone's theorem elementary matrix calculus: no infinite-dimensional spectral theory is required.
Upstream, the scalar side already has $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$ and quadratic total-cost approximation. Here the algebraic input is only that multiples of a fixed matrix commute, so the exponential is a genuine one-parameter group.
proof idea
First record that $(s\cdot\mathrm{gen})$ commutes with $(t\cdot\mathrm{gen})$: start from $\mathrm{Commute.refl}$ on the generator and push the real scalars through with smul_left/smul_right.
Unfold $U$ to matrix exponentials. Rewrite the product via Mathlib's Matrix.exp_add_of_commute, which needs exactly that commutativity hypothesis.
The remaining equality of exponents is congr 1 plus add_smul and Complex.ofReal_add, identifying $(s+t)\cdot\mathrm{gen}$ with the sum of the two scaled generators over $\mathbb{C}$.
why it matters
This is the group law half of the finite-dimensional Stone package (build-spine HLG-2.1). It is cited by stoneGeneratorCert as the one_parameter_group field, by the summary theorem operator_level_hamiltonian_emergence (the $\forall s,t$ conjunct), and inside U_unitary, which reduces unitarity to $U(t)^H=U(-t)$ plus this additivity and $U(0)=1$.
Framework-wise it supplies the operator content of "quantum mechanics is the high-frequency limit of recognition dynamics": $R$-hat's small-deviation linearization is a unitary one-parameter group generated by a self-adjoint $H$-hat on the eight-tick register. The eight-tick octave and $\hbar=\varphi^{-5}$ enter only as the intended calibration of the time unit; the algebra here is pure matrix exponential calculus.
What remains conditional is identifying the full nonlinear $R$-hat with this linear step to $O(\varepsilon^3)$, plus the exact $O(\Delta^2)$ Taylor residual and $\Delta=8\tau_0/\hbar$ units bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.