bornWeight
plain-language theorem explainer
For a finite real amplitude vector on N+1 alternatives, the Born weight of alternative i is the square of that component. Anyone deriving the Born rule from Recognition Science finite amplitudes cites this as the native real weight. The body is a one-line definition: square the real entry.
Claim. Let $\psi : \mathrm{Fin}(N+1) \to \mathbb{R}$ be a finite real amplitude vector. The Born weight of alternative $i$ is $(\psi(i))^2$.
background
In the primitive recognition calculus, a finite real amplitude is a map $\psi$ from $\mathrm{Fin}(N+1)$ into $\mathbb{R}$: one real number per discrete alternative. The module builds the real core of Born-type probabilities before complex and Hilbert-display layers.
The classical Born rule assigns probability proportional to $|\psi_i|^2$. Here the real case collapses to a plain square. Sibling notions include the squared norm (sum of these weights) and normalization (that sum equals one). Upstream complex and Hilbert-display modules reuse the same name for the analogous weight built from two real components or from a displayed complex amplitude.
The local setting is delta-native finite amplitude data: nonnegative weights, unit total mass under normalization, and norm-preserving maps that keep normalized vectors normalized.
proof idea
Pure definition: unfold to $(\psi, i)^2$. No lemmas. Downstream nonnegativity is immediate from positivity on a square; the sum-to-one theorem rewrites normalization as the sum of these weights equaling one.
why it matters
This is the real Born weight that the delta-amplitude headline packages: every weight is nonnegative; normalized amplitudes have total weight one; norm-preserving maps preserve normalization. It is the base case that FRSComplexAmplitude.bornWeight and the Hilbert-display weight refine (sum of squares of real and imaginary F_RS components, or the displayed complex weight).
In the Recognition framework it sits under the primitive recognition calculus that feeds finite unitary structure and double-slit amplitude work. It does not itself force the Born rule from the J-cost or the forcing chain; it supplies the finite real probability atom those layers quote. Parent results include bornWeight_nonneg, born_weights_sum_one, and delta_amplitude_headline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.