complex_hilbert_structure
plain-language theorem explainer
The theorem asserts that every normalized state in an RSHilbertSpace has unit vector norm, extracted directly from the ledger definition. Quantum modelers working from the Recognition Science cost functional would cite this when confirming Hilbert axioms follow from the J-equation. The proof is a one-line term wrapper that applies the norm_one field of NormalizedState.
Claim. In any RSHilbertSpace $H$, every normalized state satisfies $||ψ.vec|| = 1$.
background
Recognition Science starts from the J-cost functional equation and its reparametrization $H(x) = J(x) + 1 = ½(x + x^{-1})$, which converts the Recognition Composition Law into the d'Alembert equation. The quantum module imports HilbertSpace and defines complex_hilbert_from_ledger as the Prop that every RSHilbertSpace instance yields only unit-norm normalized states. The upstream for structure from UniversalForcingSelfReference supplies the meta-realization axioms that underwrite this extraction.
proof idea
Term-mode proof. The single line introduces the space H, its RSHilbertSpace instance, and the state ψ, then applies exact to the norm_one field of NormalizedState.
why it matters
This result supplies the unit-norm axiom required to treat the ledger-derived structure as a complex Hilbert space inside the Recognition framework. It sits after the forcing chain (T5 J-uniqueness through T8 D=3) and the RCL, closing the step from cost algebra to quantum states. No downstream theorems are recorded, leaving open how the phi-ladder and Berry threshold appear in this Hilbert setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.