complex_born_weights_sum_one
plain-language theorem explainer
Normalized finite complex amplitude vectors have Born weights that sum to one. Anyone citing the finite complex Born rule or the complex-amplitude headline needs this identity. The proof is a one-line unfolding: normalization is defined as the squared-norm sum equaling one, and that sum is exactly the sum of the component Born weights.
Claim. Let $N\in\mathbb{N}$ and let $\psi:\mathrm{Fin}(N+1)\to\mathbb{C}$ be a finite complex amplitude vector. If $\psi$ is normalized in the sense that its squared norm equals $1$, then $\sum_{i}\bigl((\mathrm{Re}\,\psi_i)^2+(\mathrm{Im}\,\psi_i)^2\bigr)=1$.
background
In the primitive recognition calculus, a finite complex amplitude is a map $\psi:\mathrm{Fin}(N+1)\to\mathbb{C}$. The complex Born weight of slot $i$ is the ordinary modulus squared $|\psi_i|^2=(\mathrm{Re},\psi_i)^2+(\mathrm{Im},\psi_i)^2$. The squared norm of $\psi$ is the sum of those weights over all $N+1$ slots.
Normalization means that squared norm equals one. The real (non-complex) sibling of this module already records the same sum-to-one fact for real amplitudes; the complex layer mirrors that structure so that Born probabilities remain a probability measure on a finite alternative set.
The module sits under Foundation.PrimitiveRecognitionCalculus and imports the real DeltaProbability layer. Hilbert space is treated only as the display completion; the native finite layer is what this theorem addresses.
proof idea
One-line definitional reduction. Unfold ComplexNormalized to complexNormSq $\psi=1$, then unfold complexNormSq to the Finset sum of complexBornWeight $\psi,i$. The hypothesis is then definitionally the goal; simpa closes it.
why it matters
Feeds the complex finite-amplitude headline theorem, which packages three facts: Born weights are nonnegative, normalized complex amplitudes have weights summing to one, and norm-preserving maps send normalized vectors to normalized vectors. The headline states that complex amplitudes already have a native finite layer and that Hilbert space remains only the display completion.
In Recognition Science this is the finite Born-rule bookkeeping step for complex amplitudes: once normalization is imposed, the component weights form a probability distribution on the finite alternative set. It parallels the real born_weights_sum_one sibling and is the complex half of the amplitude calculus that later interfaces with the forcing chain's discrete structure (eight-tick octave, finite alternatives). No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.