bornWeight_nonneg
plain-language theorem explainer
Born weights on a finite real amplitude vector are nonnegative: each coordinate weight is a square. Anyone assembling the delta-native amplitude headline or the F_RS complex amplitude package cites this. The proof unfolds the weight definition and closes by positivity of squares.
Claim. For every natural number $N$, every real amplitude vector $\psi : \mathrm{Fin}(N+1)\to\mathbb{R}$, and every index $i$, the Born weight $(\psi_i)^2$ satisfies $0\le(\psi_i)^2$.
background
In the delta-native amplitude layer, a finite real amplitude is simply a map $\psi:\mathrm{Fin}(N+1)\to\mathbb{R}$. The Born weight of alternative $i$ is defined by squaring the coordinate: $\mathrm{bornWeight}(\psi,i)=(\psi_i)^2$. This is the real, finite precursor of the usual Born rule before complex structure or Hilbert completion is introduced.
The sibling complex and F_RS packages reuse the same nonnegativity pattern: native F_RS Born weights are sums of two evaluated squares, and the Hilbert-display weight routes through the complex Born weight. The present lemma is the real base case of that chain.
Local setting is Primitive Recognition Calculus: finite alternatives, squared amplitudes as probabilities once normalized, and norm-preserving maps that keep the unit sphere.
proof idea
One-line tactic proof. Unfold the definition of Born weight to expose $(\psi_i)^2$, then apply Mathlib's positivity tactic, which discharges nonnegativity of a real square. No intermediate lemmas are required beyond the definition and the standard square-nonnegativity fact baked into positivity.
why it matters
This is the first conjunct of the delta-amplitude headline: finite amplitude data has nonnegative Born weights; normalized amplitudes sum to probability one; norm-preserving maps preserve normalization. Downstream, the F_RS complex amplitude headline and its own bornWeight_nonneg mirror the same inequality for carrier-evaluated real and imaginary parts, so the real case anchors the display story that ambient $\mathbb{C}$ is only a display of finite F_RS data.
In the Recognition framework this is scaffolding for Born-rule probability on finite recognition alternatives, not yet the full continuum Hilbert space. It feeds the primitive calculus that later connects to eight-tick structure and ladder masses only indirectly, by guaranteeing that finite recognition weights are legitimate nonnegative measures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.