ComplexNormalized
plain-language theorem explainer
Finite complex amplitude vectors on a discrete index set are normalized precisely when the sum of component Born weights equals one. Anyone citing the finite-layer Born rule, norm-preserving maps, or the complex amplitude headline uses this predicate as the standing hypothesis. The body is a one-line definitional equality of the squared norm with unity.
Claim. For $N \in \mathbb{N}$ and $\psi : \{0,\ldots,N\} \to \mathbb{C}$, the vector $\psi$ is normalized when its squared Euclidean norm equals one: $\sum_{i=0}^{N} |\psi(i)|^2 = 1$.
background
In the primitive recognition calculus, a finite complex amplitude is a map from the discrete index set $\mathrm{Fin}(N+1)$ into $\mathbb{C}$. The squared norm of such a vector is the sum, over all indices, of the complex Born weights (each weight is the squared modulus of the corresponding component).
Normalization is the statement that this squared norm equals one. The real-amplitude sibling of the same module uses an analogous predicate; the complex version is the native finite stand-in for a unit vector in a finite-dimensional Hilbert space, before any completion to the display space.
The surrounding module builds the finite complex layer of Recognition Science amplitudes: nonnegativity of Born weights, preservation of the unit-norm condition under norm-preserving maps, and the headline that Hilbert space remains only the display completion.
proof idea
Definitional, not a proved theorem. The predicate is the bare equality of the squared-norm functional with the real number $1$. Unfolding it in a later proof is exactly rewriting by that equality (as in the one-line simpa proofs of the Born-sum and norm-preservation lemmas).
why it matters
This predicate is the standing hypothesis for the finite complex Born rule: under it, the sum of complex Born weights equals one. It is also the invariant preserved by finite complex norm-preserving maps, the native finite analogue of unitary evolution.
Both facts are packaged into the complex finite-amplitude headline, which states nonnegativity of Born weights, the unit sum under normalization, and closure of the normalized class under norm-preserving maps. Downstream, the $F_{RS}[i]$ carrier layer equates its own normalization predicate with this one after display into ambient $\mathbb{C}$, so the finite-description scalar carrier inherits the same unit-norm meaning.
In the Recognition framework the construction keeps Hilbert space as display completion only; the genuine finite layer already carries Born weights and normalization without infinite-dimensional structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.