RSHilbertSpace
plain-language theorem explainer
RSHilbertSpace equips a type H with the structure of a separable complex Hilbert space for modeling ledger states in the Recognition Science quantum bridge. Quantum modelers cite it when defining operators such as the area operator on simplicial surfaces. The declaration is a direct class extension of four Mathlib structures with no additional axioms or proof steps required.
Claim. A type $H$ carries the structure of a separable Hilbert space when it is a seminormed additive commutative group, an inner product space over $ℂ$, a complete metric space, and separable in its topology.
background
The Recognition Science quantum bridge models states as vectors in a Hilbert space whose inner product encodes recognition flux derived from the cost functional. Upstream, the shifted cost $H(x) = J(x) + 1 = ½(x + x^{-1})$ reparametrizes the J-cost so that the Recognition Composition Law becomes the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. The module title states the local setting as the Hilbert Space for Recognition Science QM Bridge, where discrete recognition bits on the ledger are represented by operators acting on these states.
proof idea
The declaration is a class definition that extends SeminormedAddCommGroup, InnerProductSpace ℂ, CompleteSpace, and TopologicalSpace.SeparableSpace. No lemmas are invoked and no tactics are used; the structure is assembled directly from the four parent classes.
why it matters
This class is the required interface for every downstream quantum construction, including the AreaOperator structure that measures simplicial flux and the area_quantization theorem asserting eigenvalues are integer multiples of ℓ₀². It thereby grounds the discrete ledger in a standard Hilbert-space setting and inherits the J-uniqueness (T5) through the upstream H reparametrization. The declaration closes the interface needed for the eight-tick octave and D = 3 spatial structure to appear in quantum operators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.