complexNormSq_nonneg
plain-language theorem explainer
The squared Euclidean norm of any finite complex amplitude vector is nonnegative. Discrete Born-rule and normalization arguments in the primitive recognition calculus cite this fact. The proof unfolds the sum definition and applies nonnegativity of each complex Born weight.
Claim. For every $N\in\mathbb{N}$ and every complex amplitude vector $\psi:\{0,\ldots,N\}\to\mathbb{C}$, writing $\|\psi\|^2:=\sum_i\bigl((\mathrm{Re}\,\psi_i)^2+(\mathrm{Im}\,\psi_i)^2\bigr)$, one has $0\le\|\psi\|^2$.
background
In the DeltaAmplitude layer of Primitive Recognition Calculus, a finite complex amplitude is a map $\psi:\mathrm{Fin}(N+1)\to\mathbb{C}$. The complex Born weight at site $i$ is the ordinary modulus squared $(\mathrm{Re},\psi_i)^2+(\mathrm{Im},\psi_i)^2$, already known to be nonnegative. The squared norm is the sum of those weights over the finite index set.
The module sits next to the real-amplitude development (normSq, bornWeight, Normalized) and imports the DeltaProbability layer. The local goal is to equip discrete complex amplitudes with the same nonnegativity and normalization toolkit used for real ones, so that later recognition statements can treat complex phases without leaving the finite setting.
proof idea
Term-mode proof: unfold the definition of the squared norm (a Finset sum of complex Born weights), then apply Finset.sum_nonneg, feeding the already-proved pointwise lemma that each complex Born weight is nonnegative. No further arithmetic is required.
why it matters
Nonnegativity of the complex squared norm is the first structural fact needed before one can define normalized complex amplitudes or state a complex Born rule in the recognition calculus. It parallels the real-side lemma normSq_nonneg and underwrites any later claim that a complex amplitude can be rescaled to unit norm when it is nonzero.
No downstream consumers are wired yet in the graph, so the lemma is presently a local foundation brick rather than a cited step in T0–T8 or the RCL chain. It keeps the complex branch of DeltaAmplitude on the same footing as the real branch before phase-sensitive recognition identities are stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.