normalized_state_unit_norm
plain-language theorem explainer
Normalized states in the RS Hilbert space carry unit norm by definition of their structure. Quantum modelers in the Recognition Science framework cite this when confirming that state vectors satisfy the normalization required for Born-rule probabilities. The proof is a one-line term that selects the norm_one field from the NormalizedState record.
Claim. Let $H$ be a separable Hilbert space over the complex numbers equipped with the RS structure. For any normalized state whose vector component is $v$, one has $|v| = 1$.
background
RSHilbertSpace is the class extending SeminormedAddCommGroup, InnerProductSpace over C, CompleteSpace, and SeparableSpace. NormalizedState is the record type containing a vector vec together with the field norm_one asserting that its norm equals 1. The two H definitions from CostAlgebra and FunctionalEquation reparametrize the shifted cost function H(x) = J(x) + 1 that turns the Recognition Composition Law into d'Alembert's equation, but are not invoked here. The declaration sits inside the module that assembles complex Hilbert spaces from the ledger.
proof idea
The term proof is the single projection ψ.norm_one, which extracts the norm_one field supplied by the NormalizedState structure.
why it matters
This supplies the unit-norm axiom required for any probability interpretation inside the quantum sector of Recognition Science. It is a prerequisite for further constructions in ComplexHilbertStructure and aligns with the Hilbert-space emergence from the functional equation. No direct downstream users are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.