DiscreteEvolution
plain-language theorem explainer
DiscreteEvolution packages a symmetric real matrix H on Fin N together with the linearized update rule that maps a deviation state ψ in ℂ^N to ψ_i minus i times the action of H on ψ. Researchers deriving emergent quantum dynamics from the recognition operator would cite this structure when passing from the scalar quadratic regime of J to a discrete Schrödinger step. The definition is a direct functional encoding of the first-order map without additional lemmas.
Claim. A symmetric real matrix $H$ on indices $1$ to $N$ defines an evolution operator whose action on a state $ψ ∈ ℂ^N$ is given pointwise by $ψ_i ↦ ψ_i - i ∑_j H_{ij} ψ_j$.
background
In the Recognition Science setting the recognition operator R̂ reduces near equilibrium to the quadratic form J(1 + ε) = ε²/2 + O(ε³). This quadratic term is identified with the kinetic energy of an emergent Hamiltonian. DeviationHilbert N is the complex vector space Fin N → ℂ carrying the standard inner product; it serves as the state space for small ledger deviations. The module HamiltonianEmergence supplies the types needed to state the operator-level emergence claim while the scalar quadratic expansion itself is already proved upstream.
proof idea
The structure is introduced by direct field definitions: hamiltonian as a real-valued symmetric matrix and symmetric as the explicit equality condition. The step function is a one-line wrapper that applies the linear map ψ_i - i ∑j H{ij} ψ_j to each component of the input DeviationHilbert vector.
why it matters
This declaration supplies the data type required by diagonalHamiltonian, which sets H to the identity calibrated from J''(1) = 1, and by the hypothesis H_HamiltonianIsGenerator that asserts the recognition operator generates a self-adjoint Hamiltonian in the small-deviation limit. It realizes the module claim that recognition dynamics in the quadratic regime become equivalent to the discrete Schrödinger update ψ(t + Δt) ≈ (1 - i Ĥ Δt) ψ(t). The full operator emergence remains conditional on discrete Stone-type theorems not yet available in Mathlib.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.