normSq_nonneg
plain-language theorem explainer
The squared Euclidean norm of any finite real amplitude vector is nonnegative. Anyone building Born weights, ledger probabilities, or gap-energy nonnegativity from real amplitudes cites this. The proof unfolds the sum-of-squares definition and applies nonnegativity of each square under a finite sum.
Claim. For every $N \in \mathbb{N}$ and every real amplitude $\psi : \{0,\ldots,N\} \to \mathbb{R}$, the squared norm satisfies $0 \le \sum_{i=0}^{N} \psi(i)^2$.
background
In the primitive recognition calculus, a finite real amplitude is a map $\psi : \mathrm{Fin}(N+1) \to \mathbb{R}$. Its squared norm is the ordinary $\ell^2$ energy $$\mathrm{normSq}(\psi) := \sum_{i} \psi(i)^2$$ over the finite index set. Born weights are built from these squares (or from the complex analogue), so nonnegativity of the total energy is the first arithmetic fact needed before normalization or probability statements.
The module sits under Foundation.PrimitiveRecognitionCalculus and imports the delta-probability layer. Related displays (finite Hilbert display, bipartite planar carrier, metric quadratic forms) reuse the same squared-norm language; here the carrier is strictly real and finite.
proof idea
One short tactic proof. Unfold the definition of squared norm to a universe sum of squares. Apply Finset.sum_nonneg, reducing to pointwise nonnegativity of each summand, then close with sq_nonneg on $\psi(i)$. No induction and no special structure of $N$ beyond finiteness of the index set.
why it matters
This is the real-amplitude base lemma for nonnegativity in the Born pipeline. Downstream it supports born_rule_consistent (Born rule consistency via nonnegativity of squared norm), prob_nonneg on the quantum ledger (probabilities are nonnegative), and the forcing identity that matches complex squared norm to $|z|^2$. Gap-weight material also needs nonnegative mode energies (phiDFTAmplitude_nonneg, diffEnergy8_nonneg); the same square-sum pattern appears there.
In Recognition Science the Born rule is not postulated but forced from ledger structure. A nonnegative squared amplitude is the minimal arithmetic gate before one can speak of normalized Born weights summing to one, which this module also records as a sibling fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.