born_weights_sum_one
plain-language theorem explainer
Normalized finite real amplitudes have Born weights that sum to one: the squared components form a discrete probability distribution. Anyone citing the delta-native Born rule or the amplitude headline theorem needs this identity. The proof is a one-line definitional unfold of normalization, squared norm, and Born weight.
Claim. Let $\psi:\mathrm{Fin}(N+1)\to\mathbb{R}$ be a finite real amplitude with squared norm equal to one. Then $\sum_{i}\psi(i)^{2}=1$.
background
In the primitive recognition calculus, a finite amplitude is a real vector $\psi$ indexed by $\mathrm{Fin}(N+1)$. Its squared norm is the sum of squares of the components, and the Born weight of index $i$ is simply $\psi(i)^{2}$. Normalization means that squared norm equals one.
This sits in the delta-native amplitude layer: finite, real, and combinatorial, before any Hilbert-space completion. The same module also carries a complex amplitude variant and a notion of norm-preserving maps (the finite core of unitary evolution). The identity here is the probability-sum half of the Born package for those finite vectors.
proof idea
One-line term proof via simpa. Unfold Normalized (squared norm equals one), normSq (sum of squares), and bornWeight (component square). The hypothesis is then literally the claimed sum, so no further arithmetic is required.
why it matters
Feeds the middle conjunct of delta_amplitude_headline, the module's packaging theorem: nonnegative Born weights, total probability one under normalization, and preservation of normalization by norm-preserving maps. That headline is the finite, delta-native statement of the Born rule before display-completion to Hilbert space.
In Recognition Science this is bookkeeping for the discrete alternative set on which recognition amplitudes live, not a derivation of the Born rule from the forcing chain. It closes the probability-sum obligation so downstream work can treat normalized finite amplitudes as genuine probability data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.