normalized_state_unit_norm
plain-language theorem explainer
Any vector packaged inside a NormalizedState over an RS Hilbert space has Euclidean norm exactly one. Quantum modelers in the Recognition Science setting cite the result to confirm that states pulled from the ledger satisfy the unit-norm axiom before further constructions. The proof is a direct one-line field projection from the structure definition.
Claim. Let $H$ be a separable Hilbert space over the complex numbers obeying the RS Hilbert space axioms. For any normalized state structure whose vector field is denoted $v$ and whose norm field asserts that the norm of $v$ equals one, the equality holds: the norm of $v$ is one.
background
RSHilbertSpace is the type class that equips a space with the structure of a separable Hilbert space over ℂ: it extends SeminormedAddCommGroup, InnerProductSpace ℂ, CompleteSpace, and SeparableSpace. NormalizedState is the structure that bundles a vector vec : H together with an explicit proof norm_one : ‖vec‖ = 1. The two H reparametrizations (H(x) = J(x) + 1 from CostAlgebra and the functional-equation version) appear among the module dependencies but are not invoked by this declaration.
proof idea
The proof is the one-line term ψ.norm_one, which directly extracts the norm_one field supplied by the NormalizedState structure.
why it matters
The declaration supplies the unit-norm guarantee required by any subsequent quantum construction that begins from ledger-derived states. It sits inside the ComplexHilbertStructure module whose sibling complex_hilbert_from_ledger builds the full Hilbert-space representation; the result therefore closes the normalization step before those constructions are attempted. No downstream uses are recorded yet, leaving open whether the same norm property will be re-derived from the cost functional H or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.