bornWeight_nonneg
plain-language theorem explainer
Native Born weights on finite F_RS[i] amplitude vectors are nonnegative at every index. Anyone citing the F_RS[i] amplitude headline or comparing native versus displayed complex Born rules needs this. The proof unfolds the sum-of-squares definition and applies nonnegativity of real squares via nlinarith.
Claim. For every $N \in \mathbb{N}$, every finite amplitude vector $\psi$ with values in the $F_{RS}[i]$ carrier, and every index $i \in \{0,\ldots,N\}$, the native Born weight of component $i$ satisfies $0 \le w(\psi,i)$, where $w(\psi,i)$ is the sum of squares of the evaluated real and imaginary carrier parts of $\psi_i$.
background
In the primitive recognition calculus, finite amplitudes are first treated as real vectors (DeltaAmplitude) and then as complex data carried by the finite-description scalar field $F_{RS}[i]$. An FRSIAmp N is a map from $\mathrm{Fin}(N+1)$ into carrier expressions with real and imaginary parts; ambient $\mathbb{C}$ is only a display.
The native Born weight of component $i$ is $\mathrm{eval}(\mathrm{re},\psi_i)^2 + \mathrm{eval}(\mathrm{im},\psi_i)^2$. The parallel real construction in DeltaAmplitude takes $w(\psi,i)=(\psi_i)^2$ and already proves nonnegativity by positivity. Cost-axiom Normalization (cost vanishes at unity) sits upstream in the foundation stack but is not invoked here; the local fact is pure square nonnegativity on the carrier evaluation map.
proof idea
Term-mode proof in two steps. Unfold the native Born-weight definition to the sum of two real squares of carrier evaluations. Feed sq_nonneg on each evaluated real and imaginary part into nlinarith, which closes $0 \le a^2 + b^2$. No induction on $N$ and no appeal to normalization or display agreement.
why it matters
This is the nonnegativity conjunct of frsi_amplitude_headline: finite complex amplitudes live on the $F_{RS}[i]$ carrier, ambient $\mathbb{C}$ is display-only, and the display preserves Born weights and normalization. The same nonnegativity pattern appears in the DeltaAmplitude headline (real finite amplitudes have nonnegative Born weights, normalized ones sum to one, norm-preserving maps keep normalization).
In the Recognition stack this is bookkeeping for Born-rule probability before any continuum Hilbert-space completion: weights must be nonnegative before one can talk about total probability one or unitary preservation. It does not itself force $J$-uniqueness, $\varphi$, the eight-tick octave, or $D=3$; it only keeps the finite-amplitude layer consistent with a probability reading.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.