delta_complex_amplitude_headline
plain-language theorem explainer
Finite complex amplitudes on Fin(N+1) already carry a native Born package: component weights |ψ_i|² are nonnegative, sum to one on normalized vectors, and any squared-norm-preserving map sends normalized states to normalized states. Cite this when arguing that the Recognition finite layer needs no Hilbert completion for probability bookkeeping. The proof is a three-conjunct term packaging of the component lemmas.
Claim. For every $N\in\mathbb{N}$ and every finite complex amplitude $\psi:\{0,\ldots,N\}\to\mathbb{C}$: (i) each Born weight $|\psi_i|^2=\mathrm{Re}(\psi_i)^2+\mathrm{Im}(\psi_i)^2$ is nonnegative; (ii) if the squared norm of $\psi$ equals $1$, then $\sum_i |\psi_i|^2=1$; (iii) if $U$ preserves squared norms pointwise, then $U$ sends every normalized amplitude to a normalized amplitude.
background
In the Primitive Recognition Calculus, a finite complex amplitude is a map $\psi:\mathrm{Fin}(N+1)\to\mathbb{C}$. Its component Born weight is the ordinary modulus squared $|\psi_i|^2=\mathrm{Re}^2+\mathrm{Im}^2$, and the squared norm is the sum of those weights. Normalization means squared norm equals one; a map $U$ is norm-preserving when it leaves every squared norm unchanged (the finite native stand-in for unitary evolution).
The real-amplitude sibling module already closed the same three facts for real vectors. This module lifts them to $\mathbb{C}$ without leaving the finite index set. As the doc-comment stresses, Hilbert space is only the display completion: the probability identities live on the finite layer.
Upstream, nonnegativity is elementary ($a^2+b^2\ge 0$), the sum-to-one identity is definitional once normalization is assumed, and preservation of normalization is immediate from norm preservation.
proof idea
Term-mode triple constructor. The first conjunct is exactly complexBornWeight_nonneg (nlinarith on the two squares). The second is complex_born_weights_sum_one, which rewrites normalization as the sum of Born weights and closes by simpa. The third applies complex_normalized_of_normPreserving: if $U$ preserves squared norms and $\psi$ is normalized, then $U\psi$ is normalized. No further arithmetic.
why it matters
This is the complex half of the finite-amplitude headline pair. Downstream it is consumed by strongClosureCertificate in DeltaNativeStrongClosure, which assembles the closed Delta-native theorem surface (real forgetful display, generable carrier, certified analytic protocols, and certified transformers).
In the Recognition framework the claim matters because Born bookkeeping and norm-preserving evolution are required already at the finite native layer; the continuum Hilbert space is not a foundational prerequisite. It sits beside the real headline and feeds the strong-closure certificate that packages the whole Primitive Recognition Calculus surface. No open scaffold remains: the status is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.