complexBornWeight
plain-language theorem explainer
The complex Born weight at a finite alternative is the squared modulus of that component: Re(z)^2 + Im(z)^2. Anyone proving the finite complex Born rule, normalization, or the complex-amplitude headline cites this. It is a bare definition, not a derived identity.
Claim. For a finite complex amplitude vector $\psi:\{0,\ldots,N\}\to\mathbb{C}$ and an index $i$, the complex Born weight is $|\psi(i)|^2=\mathrm{Re}(\psi(i))^2+\mathrm{Im}(\psi(i))^2$.
background
In the primitive recognition calculus, a finite complex amplitude is a map from a discrete set of $N+1$ alternatives into $\mathbb{C}$. The real sibling of this layer already has a Born weight (squared real amplitude). The complex layer needs the matching pointwise weight before one can sum to a total squared norm or state normalization.
The classical Born rule identifies outcome probability with $|\psi|^2$. Here that rule is stated first on a finite index set, before any Hilbert-space completion. Upstream double-slit amplitudes are sums of complex phases whose intensities are the same squared-modulus construction; the golden-integer and action norms nearby are different algebraic norms and are not used in the body of this definition.
Locally the module builds the finite complex stack: pointwise weight, total squared norm, normalization, and norm-preserving maps. Hilbert space is treated later as a display completion of this finite layer.
proof idea
One-line definition. On input $\psi$ and index $i$, return the sum of squares of the real and imaginary parts of the complex value $\psi(i)$. No lemmas are applied.
why it matters
This is the atomic weight that the finite complex Born package rests on. Nonnegativity of each weight, the identity that normalized amplitudes sum weights to one, and the total squared-norm sum are all defined or proved from it. The complex finite-amplitude headline packages those three facts and states that Hilbert space remains only the display completion.
Downstream, the FRS complex-amplitude display proves that this weight agrees with the native finite $F_{RS}[i]$ Born weight (by definitional equality), and the Hilbert-display completion reuses the same formula as its displayed Born weight. In Recognition Science terms it is the finite complex face of the Born rule that the real delta-amplitude layer already had, before continuum display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.