complex_normalized_of_normPreserving
plain-language theorem explainer
Norm-preserving maps on finite complex amplitude vectors send normalized states to normalized states. Anyone assembling the finite Born layer (before Hilbert completion) cites this. The proof is a two-step rewrite: unfold the unit-norm predicate and apply the preservation hypothesis.
Claim. Let $N\in\mathbb{N}$ and let $U$ map finite complex amplitude vectors $\mathrm{Fin}(N+1)\to\mathbb{C}$ to themselves. If $U$ preserves squared norm ($\|U\psi\|^2=\|\psi\|^2$ for every $\psi$) and $\psi$ is normalized ($\|\psi\|^2=1$), then $U\psi$ is normalized ($\|U\psi\|^2=1$).
background
In the primitive recognition calculus, complex amplitudes live on a finite index set before any Hilbert completion. A finite complex amplitude vector is a map $\psi:\mathrm{Fin}(N+1)\to\mathbb{C}$. Its squared norm is the sum of modulus-squares of the components; the state is normalized when that sum equals one.
Norm preservation is the native finite stand-in for unitary evolution: a map $U$ is norm-preserving when it leaves the squared norm of every amplitude vector unchanged. The module treats Hilbert space as a display completion of this finite layer, not as the primitive carrier of the Born rule.
The real-amplitude sibling already records the same preservation fact; the complex version is the direct analogue needed for the complex headline.
proof idea
Term-mode, essentially a one-line rewrite after unfolding. Unfold the definition of complex normalization (squared norm equals one). Rewrite the goal with the norm-preservation hypothesis applied to $\psi$, which replaces $|U\psi|^2$ by $|\psi|^2$, then rewrite with the hypothesis that $\psi$ itself is normalized. No auxiliary lemmas are required.
why it matters
This is the third conjunct of the complex finite-amplitude headline: Born weights are nonnegative, normalized complex amplitudes sum to one, and norm-preserving finite complex maps preserve normalization. The headline packages the native finite Born layer and keeps Hilbert space as display completion only.
In the Recognition framework the finite layer is primary; unitary evolution on the completed space is a later display. The result is the complex counterpart of the real-amplitude preservation lemma in the same module, and it closes the complex half of the amplitude calculus before any continuum limit is taken.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.