bornWeight
plain-language theorem explainer
Native Born weight for one slot of a finite F_RS[i] amplitude: the sum of squares of the evaluated real and imaginary F_RS components. Anyone proving nonnegativity, total probability one, or agreement with the ambient complex display cites this. The body is the direct |z|^2 expansion, not a derived lemma.
Claim. For $N\in\mathbb{N}$, a finite amplitude $\psi$ over $F_{RS}[i]$ (a map from $\mathrm{Fin}(N+1)$ into pairs of $F_{RS}$ expressions), and an index $i$, the Born weight is $\mathrm{eval}(\mathrm{Re}\,\psi_i)^2 + \mathrm{eval}(\mathrm{Im}\,\psi_i)^2\in\mathbb{R}$.
background
In the primitive recognition calculus, finite amplitudes are the native home of Born weights before any Hilbert completion. The sibling type FRSIAmp N is a vector of length $N+1$ whose entries are $F_{RS}[i]$ expressions (each a real/imag pair in the F_RS carrier). Evaluation via the carrier map sends those expressions to ordinary reals.
The real-line precursor in DeltaAmplitude defines Born weight as a plain square $(\psi_i)^2$. The complex and Hilbert-display variants lift that to $|z|^2$. This definition is the F_RS-native complex form: evaluate the two components, then sum squares.
The module sits between the F_RS carrier and the ambient complex amplitude display, so that later theorems can identify native weights with displayed complex Born weights by reflexivity.
proof idea
Pure definitional equation, not a proof. The right-hand side is exactly $\mathrm{eval}(\mathrm{re})^2+\mathrm{eval}(\mathrm{im})^2$ on the $i$-th F_RS expression pair. Downstream nonnegativity unfolds this and applies nonnegativity of squares; the display-agreement theorem is rfl against the ambient complex Born weight.
why it matters
This is the F_RS-side anchor of the Born rule in the recognition calculus. It is consumed by native nonnegativity, by the identity that displayed complex Born weight equals the native formula, by the matching norm-squared identity, and by the F_RS amplitude headline that packages nonnegativity with normalization.
On the DeltaAmplitude side the same name feeds the finite Born-weight sum-to-one theorem and the delta-amplitude headline (nonnegative weights, total probability one for normalized amplitudes, norm-preserving maps keep normalization). Those headlines are the finite native core of unitary evolution before Hilbert completion.
Within Recognition Science this is infrastructure for reading measurement weights off ledger amplitudes rather than postulating the Born rule. It does not itself force $\phi$, the eight-tick octave, or $D=3$; it supplies the probability reading once amplitudes exist.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.