Observable
plain-language theorem explainer
The Observable structure defines a self-adjoint bounded linear operator on an RS Hilbert space to support the quantum bridge in Recognition Science. Researchers linking cost algebra to measurement would cite this when formalizing observables that distinguish states. The definition encodes the self-adjointness condition directly through the inner product axiom.
Claim. Let $H$ be a type equipped with the RS Hilbert space structure. An observable on $H$ consists of a bounded linear operator $A : H → H$ over the complex numbers such that $⟨A x, y⟩_ℂ = ⟨x, A y⟩_ℂ$ for all $x, y ∈ H$.
background
RSHilbertSpace is a class that extends SeminormedAddCommGroup, InnerProductSpace over ℂ, CompleteSpace, and SeparableSpace, supplying the inner product used in the self-adjoint condition. The module establishes observable algebra for the Recognition Science QM bridge. Upstream results include the shifted cost H from CostAlgebra, which satisfies the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y), and the simpler value-based observable structure in RecognitionForcing.
proof idea
This is a structure definition that directly specifies the operator field and the self-adjoint predicate. It relies on the RSHilbertSpace type class instance and the Mathlib bounded linear operator type without further lemmas or tactics.
why it matters
This structure supplies the quantum observable type required by recognition_forcing_complete and recognition_is_cost_structure in Foundation.RecognitionForcing. It fills the QM bridge step that connects cost structures to state-distinguishing observables, supporting the master theorem on recognition forcing. Downstream uses appear in astrophysics observability limits and constant falsifiers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.