embed
plain-language theorem explainer
The embed definition converts a SmallDeviationState, consisting of small real deviations on N bonds, into the complex Hilbert space DeviationHilbert by casting each deviation componentwise to ℂ. Researchers modeling the small-deviation limit of the Recognition Operator would cite this map when lifting ledger states to wavefunctions for discrete Schrödinger evolution. It is realized by a direct one-line coercion from the deviations field.
Claim. Let $s$ be a small-deviation state on $N$ bonds, with real components $ε_i$ satisfying $|ε_i| ≤ 1/2$. The embedding $ι(s) ∈ ℂ^N$ is defined by $ι(s)_i = ε_i$.
background
The HamiltonianEmergence module shows that the Recognition Operator reduces to quadratic energy for states near equilibrium, where J(1 + ε) = ε²/2 + O(ε³). SmallDeviationState is the structure holding a map deviations : Fin N → ℝ together with the uniform bound |deviations i| ≤ 1/2. DeviationHilbert is the abbreviation Fin N → ℂ, the space carrying the standard inner product for emergent quantum states.
proof idea
The definition is a one-line wrapper that applies the canonical coercion from ℝ to ℂ componentwise to the deviations field of the input state.
why it matters
This embedding supplies the concrete lift from classical ledger deviations to quantum states and is used by downstream constructions including DomainInstance in RecognitionCategory and CoarseGrain in the classical bridge. It realizes the small-deviation regime in which the quadratic J-cost becomes the generator of unitary evolution, consistent with the module's claim that recognition dynamics approximate discrete Schrödinger evolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.