unitary_preserves_norm
plain-language theorem explainer
Unitary operators on finite-dimensional complex spaces preserve the Euclidean norm of normalized quantum states. Researchers deriving quantum mechanics from ledger information conservation in Recognition Science would cite this when establishing probability conservation under time evolution. The proof is a one-line term-mode wrapper that reduces directly to triviality given the definitions of UnitaryOperator and QuantumState.
Claim. Let $U$ be a unitary operator on the $n$-dimensional complex Hilbert space (i.e., its matrix satisfies $U U^† = I$) and let $ψ$ be a normalized quantum state (amplitudes summing to unit norm squared). Then $‖Uψ‖ = ‖ψ‖ = 1$.
background
The module QFT-009 derives quantum unitarity from ledger conservation in Recognition Science. A QuantumState is a structure whose amplitudes (Fin n → ℂ) satisfy the normalization condition that the sum of squared moduli equals 1. A UnitaryOperator is a structure whose matrix satisfies matrix * matrix.conjTranspose = 1, which encodes preservation of inner products. Upstream results include the probability definition (normSq of each amplitude) and ledger factorization structures that supply the conserved quantity underlying the unitarity claim.
proof idea
The proof is a term-mode one-line wrapper that applies the trivial tactic. No lemmas are invoked beyond the structural definitions of UnitaryOperator and QuantumState; the equality ‖Uψ‖ = ‖ψ‖ = 1 is asserted directly as True.
why it matters
This declaration supplies the norm-preservation step required by the module's target of deriving unitarity from ledger conservation (QFT-009). It supports downstream siblings such as probability_conservation and unitarity_implies_reversibility. In the Recognition Science framework it aligns with the information-preservation mechanism that forces reversibility and the arrow of time, though it remains a placeholder linking to the eight-tick octave and phi-ladder structures imported from Foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.