NormalizedState
plain-language theorem explainer
NormalizedState packages a unit vector in an RS Hilbert space. Quantum researchers bridging Recognition Science to QM cite it to enforce normalization when defining states. The declaration is a direct structure definition with a vector field and an explicit norm-equality constraint.
Claim. Let $H$ be a separable Hilbert space over the complex numbers. A normalized state is a vector $v$ in $H$ satisfying $||v|| = 1$.
background
The module sets up a Hilbert space foundation for the Recognition Science quantum mechanics bridge. RSHilbertSpace is the class that equips a type with the structure of a separable Hilbert space over ℂ, extending seminormed additive commutative group, inner product space, complete space, and separable topological space.
proof idea
The declaration is a structure definition. It directly introduces the fields vec for the underlying vector in H and norm_one for the equality ||vec|| = 1. No lemmas or tactics are applied.
why it matters
NormalizedState supplies the basic notion of a quantum state for the Recognition Science QM bridge. It is used by complex_hilbert_from_ledger to assert the unit-norm property, by normalized_state_unit_norm to extract the norm equality, by Hamiltonian to require bounded energy for all normalized states, and by Substrate in the ILG relativity module to define the quantum substrate. It connects to the separable Hilbert space required for unitary evolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.