DeviationHilbert
DeviationHilbert defines the complex vector space of functions from Fin N to ℂ for an N-bond system. Researchers deriving emergent Hamiltonians from the Recognition Operator cite it as the state space in which small real deviations become vectors for discrete Schrödinger evolution. The declaration is a direct type abbreviation with no proof obligations or lemmas.
claimFor each natural number $N$, the space of $N$-bond deviations is the vector space of all functions from the finite set of $N$ indices to the complex numbers, equipped with the standard Hermitian inner product.
background
The module shows that the Recognition Operator reduces to a quadratic form near equilibrium, with $J(1 + ε) = ε²/2 + O(ε³)$ proved via quadratic_emergence. SmallDeviationState parameterizes nearby states by real deviations ε, and the embedding maps them into the complex space. DeviationHilbert supplies the codomain for that embedding and the domain for the discrete evolution operator. The module states that this quadratic form is the kinetic energy of the emergent Hamiltonian, turning the eight-tick recognition dynamics into the approximation ψ(t + Δt) ≈ (1 - iĤΔt)ψ(t).
proof idea
This is a type abbreviation that directly sets the deviation space equal to Fin N → ℂ. No lemmas or tactics are invoked; the definition serves only as the target type for embed and the source type for DiscreteEvolution.step.
why it matters in Recognition Science
The type is required by DiscreteEvolution, whose structure carries a symmetric real Hamiltonian matrix and whose step applies the linearized recognition map in the quadratic regime. It is also the codomain of embed, whose norm-squared equals twice the quadratic energy. In the Recognition framework it supplies the Hilbert-space setting for the emergence claim that Ĥ is generated by the Recognition Operator in the small-strain limit, closing the scalar foundation already proved in quadratic_emergence while leaving the full Stone-theorem step for later infrastructure.
scope and limits
- Does not define or prove any inner-product properties on the space.
- Does not connect the space directly to the J-cost function or the phi-ladder.
- Does not address the continuum limit or the case of infinite N.
- Does not prove self-adjointness or unitarity of any operator on the space.
formal statement (Lean)
103abbrev DeviationHilbert (N : ℕ) := Fin N → ℂ
proof body
Definition body.
104
105/-- Embed real deviations into the complex Hilbert space. -/