normalized_of_normPreserving
plain-language theorem explainer
Norm-preserving maps on finite real amplitude vectors send normalized states to normalized states. Anyone citing the delta-native amplitude headline uses this as the third conjunct: unitary-style evolution keeps total Born mass one. The proof is a two-step rewrite: unfold normalization and apply exact norm-square preservation.
Claim. Let $N\in\mathbb{N}$ and let $U$ be a map on finite real amplitude vectors $\mathrm{Amp}_N=\mathrm{Fin}(N+1)\to\mathbb{R}$. If $U$ preserves squared norm exactly ($\|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
This module develops a finite, delta-native amplitude calculus before any Hilbert-space completion. An amplitude is a real vector on $\mathrm{Fin}(N+1)$; its squared norm is the sum of squares of components, and the Born weight at index $i$ is that component squared. Normalization means squared norm equals one, so the Born weights of a normalized amplitude sum to one (proved separately in the same file).
Norm-preservation is the finite native core of unitary evolution: a map $U$ is norm-preserving when it leaves squared norm invariant for every amplitude. The doc-comment states that Hilbert-space unitaries are the display-completion of this finite condition. The local setting is Primitive Recognition Calculus: amplitudes and probabilities built from discrete recognition data, not from an a-priori $L^2$ space.
Upstream scaffolding includes RS-native units and discrete evolution operators elsewhere in Foundation; those supply the broader story of recognition steps, but this lemma only needs the two local predicates on $\mathrm{Amp}_N$.
proof idea
Term-mode proof by unfolding and rewriting. Unfold the definition of Normalized on the goal, obtaining $\mathrm{normSq}(U\psi)=1$. Rewrite with the norm-preservation hypothesis at $\psi$, replacing $\mathrm{normSq}(U\psi)$ by $\mathrm{normSq},\psi$. Rewrite with the normalization hypothesis on $\psi$, which supplies $\mathrm{normSq},\psi=1$. No external lemmas are required beyond the two predicate definitions.
why it matters
This is the third arm of the delta-amplitude headline theorem in the same module: nonnegative Born weights, total probability one for normalized amplitudes, and preservation of normalization under norm-preserving maps. The headline packages the finite Born rule and the statement that finite unitary-style maps keep probability normalized.
In the Recognition framework this is the discrete precursor to unitary evolution of recognition amplitudes: before Clifford bridges, eight-tick structure, or Hamiltonian emergence operators are invoked, one needs a clean finite fact that exact norm preservation implies normalized states stay normalized. Downstream only the headline cites it directly; the headline is the citation surface for later probability and evolution arguments in Primitive Recognition Calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.