Pith. sign in
module module moderate

IndisputableMonolith.Foundation.HamiltonianEmergenceOperator

show as:
view Lean formalization →

Module that complexifies the discrete-evolution Hamiltonian from the Recognition Operator into a Hermitian operator on complex Hilbert space, then builds the skew-Hermitian generator and the unitary one-parameter group it produces. Physicists tracing how RS discrete evolution becomes Schrödinger dynamics would cite it. Definitions and short algebraic lemmas establish Hermiticity, unitarity, and the first-order step expansion.

claimGiven a discrete-evolution Hamiltonian (real symmetric matrix from the Recognition Operator near equilibrium), form its complexification $H_c$, the skew-Hermitian generator $G = -i H_c$, and the unitary group $U(t) = \exp(t G)$. The module records that $H_c$ is Hermitian, $G$ is skew-Hermitian, $U$ is unitary with $U(0)=I$ and $U(s+t)=U(s)U(t)$, and the first-order step matches the discrete evolution.

background

Upstream, Hamiltonian Emergence shows that the quantum Hamiltonian arises as the small-deviation limit of the Recognition Operator $\hat R$. Near equilibrium ($x \approx 1$), the $J$-cost $J(x)=(x+x^{-1})/2-1$ reduces to a quadratic form, yielding a real symmetric matrix ev.hamiltonian on the discrete state space.

This module takes that real matrix and views it as a complex matrix $H_c$. From $H_c$ one builds the skew-Hermitian generator and the continuous unitary group that interpolates the discrete recognition steps. The setting is the Foundation layer: forcing the continuum Schrödinger picture out of the discrete RS evolution without extra postulates.

Sibling objects include the complexified Hamiltonian, Hermiticity and skew-Hermiticity witnesses, the exponential map $U$, and the first-order matching identity between a discrete step and the generator.

proof idea

Definition module with short algebraic lemmas, not a single deep theorem. Complexification is the canonical real-to-complex embedding of the symmetric matrix. Hermiticity of $H_c$ and skew-Hermiticity of the generator follow from symmetry of the real Hamiltonian. The unitary group is the matrix exponential of the generator; identities $U(0)=I$, $U(s+t)=U(s)U(t)$, conjugate-transpose inversion, and membership in the unitary group are standard exponential calculus. The step-equals-first-order lemma expands the discrete recognition step to linear order in the generator.

why it matters in Recognition Science

Closes the passage from discrete Recognition evolution to continuous unitary quantum dynamics inside the Foundation stack. Upstream Hamiltonian Emergence supplies the real symmetric matrix from the $J$-cost quadratic limit; this module promotes it to a Hermitian operator and a unitary group, the objects needed for Schrödinger-picture statements later in the monolith.

No downstream used_by edges are recorded yet, so the module is presently a leaf that packages the operator calculus for any parent that needs continuous-time RS quantum evolution. It sits after the forcing chain landmarks (T5 $J$-uniqueness, equilibrium expansion) and before continuum physics claims that quote a Hamiltonian or a unitary propagator.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (15)