complexBornWeight_nonneg
plain-language theorem explainer
For any finite complex amplitude vector on N+1 alternatives, each component Born weight re²+im² is nonnegative. Anyone building the finite-layer Born calculus or the complex amplitude headline cites this. The proof unfolds the weight and closes by nonnegativity of real and imaginary squares.
Claim. Let $\psi : \mathrm{Fin}(N+1) \to \mathbb{C}$ be a finite complex amplitude vector. For every index $i$, the complex Born weight $|\psi(i)|^2 = \mathrm{Re}(\psi(i))^2 + \mathrm{Im}(\psi(i))^2$ satisfies $0 \le |\psi(i)|^2$.
background
This module develops the finite complex amplitude layer of the primitive recognition calculus: amplitudes live on a discrete set of $N+1$ alternatives before any Hilbert-space completion. A complex amplitude vector is simply a map $\mathrm{Fin}(N+1)\to\mathbb{C}$.
The complex Born weight of alternative $i$ is the ordinary modulus squared of the $i$-th component, written $\mathrm{re}^2+\mathrm{im}^2$. The real sibling of this fact is the nonnegativity of the real Born weight; here the same role is played for complex entries. The squared norm of the whole vector is the sum of these weights, so componentwise nonnegativity is the first arithmetic step toward a normalized probability interpretation.
proof idea
Unfold the definition of the complex Born weight to $\mathrm{re}(\psi_i)^2+\mathrm{im}(\psi_i)^2$. Apply nlinarith with the two elementary facts that squares of real numbers are nonnegative (sq_nonneg on the real and imaginary parts). No further structure on $\psi$ is used.
why it matters
This is the first conjunct of the complex finite-amplitude headline: Born weights are nonnegative, normalized complex amplitudes sum to one, and norm-preserving maps keep normalization. Downstream, complexNormSq_nonneg sums the component weights via Finset.sum_nonneg and needs exactly this lemma. The headline then packages the nonnegativity statement for the finite complex layer, with Hilbert space retained only as the display completion. In the Recognition framework this anchors the Born rule at the discrete amplitude stage rather than postulating it after completion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.