NormPreserving
plain-language theorem explainer
Norm-preserving maps on finite real amplitude vectors are those that leave the squared Euclidean norm unchanged. Anyone working the finite native core of unitary evolution cites this predicate. It is a one-line Prop definition: equality of squared norms before and after the map.
Claim. A map $U$ on finite real amplitude vectors of length $N+1$ is norm-preserving when $\|U\psi\|_2^2 = \|\psi\|_2^2$ for every amplitude vector $\psi$.
background
In the delta-native amplitude calculus, an amplitude vector is a real function on $\mathrm{Fin}(N+1)$. Its squared norm is the sum of squares of the components; Born weights are the individual squared components, and a vector is normalized when that sum equals one.
The module treats finite amplitude data as the native core of recognition dynamics. Full Hilbert-space unitaries appear only after display-completion; here the finite stand-in for unitarity is exact preservation of squared norm under a map $U : \mathrm{Amp},N \to \mathrm{Amp},N$.
Upstream, the same squared-norm construction appears on the finite Hilbert display and in related planar carriers, always as the sum-of-squares (or modulus-squared) quantity that Born weights and normalization read off.
proof idea
Pure definition: the predicate is the universal quantification that squared norm of $U\psi$ equals squared norm of $\psi$ for every finite amplitude vector $\psi$. No lemmas or tactics.
why it matters
This predicate is the finite native core of unitary evolution in Recognition Science. It feeds the lemma that norm-preserving maps send normalized amplitudes to normalized amplitudes, and it is the third conjunct of the delta-amplitude headline: nonnegative Born weights, total probability one on normalized states, and preservation of normalization under norm-preserving maps.
That headline packages the finite Born rule and the finite stand-in for unitarity before any Hilbert completion. Downstream display-completion lifts the same idea to complex finite Hilbert displays; the present definition stays strictly real and finite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.