ComplexNormPreserving
plain-language theorem explainer
A map on finite complex amplitude vectors is norm-preserving when it leaves the squared ℓ²-norm unchanged for every vector. This is the native finite stand-in for unitary evolution in the Recognition calculus. Anyone citing the complex finite-amplitude headline or normalization stability under evolution will use it. The body is a direct universal quantification equating squared norms before and after the map.
Claim. For $N \in \mathbb{N}$ and a map $U$ sending complex amplitude vectors on $\mathrm{Fin}(N+1)$ to themselves, $U$ is complex-norm-preserving when $\|U\psi\|^2 = \|\psi\|^2$ for every amplitude vector $\psi$, with $\|\cdot\|^2$ the sum of complex Born weights over the finite index set.
background
In the primitive recognition calculus, a complex amplitude vector is a map $\mathrm{Fin}(N+1) \to \mathbb{C}$. Its squared norm is the sum of the complex Born weights at each index; a vector is normalized when that sum equals one.
The real-amplitude side of the same module already has a parallel norm-preservation predicate. Here the complex version is the finite native stand-in for unitary evolution: full Hilbert-space unitarity is treated as a display completion, while the discrete layer only needs maps that keep the squared norm fixed.
Upstream, the squared-norm helper is exactly the sum of complex Born weights, and the RS-native units and recognition evolution family supply the broader operator context in which such maps arise (e.g. discrete evolution exponentials), without being required in the definition itself.
proof idea
Definitional, not a proved theorem. The predicate is the single universal statement that for every finite complex amplitude vector $\psi$, the squared norm of $U\psi$ equals the squared norm of $\psi$. No lemmas or tactics are involved.
why it matters
This predicate is the complex half of the finite-amplitude norm story. Downstream, it is the hypothesis that lets normalization pass through a map: if $U$ is complex-norm-preserving and $\psi$ is complex-normalized, then $U\psi$ is complex-normalized (one-line rewrite of the squared-norm equality).
It is also the third conjunct of the complex finite-amplitude headline: Born weights nonnegative, normalized vectors sum to one, and norm-preserving maps send normalized vectors to normalized vectors. That headline states that complex amplitudes already have a native finite layer, with Hilbert space only the display completion.
In the broader Recognition framework this is the discrete stand-in for unitary evolution on the amplitude side of the recognition calculus, parallel to the real-amplitude norm-preservation predicate in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.