complex_hilbert_from_ledger
plain-language theorem explainer
Recognition Science defines the proposition that every normalized state in an RS Hilbert space has unit norm. Quantum modelers deriving Hilbert structure from the cost ledger would cite this when confirming the norm condition holds by construction. The declaration is a direct definition that restates the norm_one field from NormalizedState.
Claim. In any separable Hilbert space $H$ over $ℂ$ equipped with the RS structure, every normalized state $ψ$ satisfies $‖ψ‖ = 1$.
background
RSHilbertSpace is a class that extends a type H with the structure of a separable Hilbert space over the complex numbers: it includes a seminormed additive commutative group, an inner product space over $ℂ$, completeness, and separability. NormalizedState H is a structure containing a vector vec : H together with the field norm_one : ‖vec‖ = 1. This definition appears in the quantum module that extracts the complex Hilbert structure from the Recognition Science ledger axioms, where the shifted cost function satisfies the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y) derived from the recognition composition law.
proof idea
The declaration is a definition that directly sets the proposition to the universal quantification over RS Hilbert spaces and normalized states. No tactics are applied; the unit norm follows immediately from the norm_one field in the NormalizedState structure.
why it matters
This proposition is invoked by the theorem complex_hilbert_structure, which extracts the unit norm as a stable interface, and by complex_hilbert_implies_unit_norm. It bridges the algebraic cost framework (with J-uniqueness at T5 and the eight-tick octave at T7) to the quantum setting, packaging the norm property as a reusable Prop in the ledger-to-Hilbert derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.