bornWeight
plain-language theorem explainer
Born weight of the i-th slot of a finite Hilbert display vector is the squared complex modulus of that entry. Anyone working the finite-amplitude probability layer cites this as the display-side Born weight. The body is a one-line alias of the complex Born weight on maps Fin(N+1)→ℂ.
Claim. For $N\in\mathbb{N}$ and a finite Hilbert display vector $v:\{0,\ldots,N\}\to\mathbb{C}$, the Born weight at index $i$ is $|v(i)|^2=\mathrm{Re}(v(i))^2+\mathrm{Im}(v(i))^2$.
background
The finite Hilbert display carrier is the ambient complex vector on the finite distinction alternatives: maps $\mathrm{Fin}(N+1)\to\mathbb{C}$. The sibling display sends a native $F_{RS}[i]$ amplitude into that carrier, so ordinary complex Hilbert notation can be used without leaving the Recognition stack.
Upstream, the complex Born weight on a finite complex amplitude is defined componentwise as $\mathrm{re}^2+\mathrm{im}^2$. The real finite-amplitude Born weight is simply the square of the real entry. The native $F_{RS}$ Born weight evaluates the two Recognition-carrier components and squares them in the same way.
This module sits in the Primitive Recognition Calculus bridge: it completes the finite display so that Hilbert-style norms and Born weights match the native $F_{RS}[i]$ formulae once the amplitude is displayed.
proof idea
One-line definitional wrapper: the display Born weight is exactly DeltaAmplitude.complexBornWeight applied to the finite Hilbert vector and the index. No extra algebra; the meaning is inherited from the complex squared-modulus formula $\mathrm{re}^2+\mathrm{im}^2$.
why it matters
This is the display-side Born weight used throughout the finite-amplitude probability layer. Downstream it is consumed by nonnegativity lemmas, the sum-to-one identity for normalized amplitudes, and the delta-amplitude headline (nonnegative weights, total probability one, norm-preserving maps keep normalization). Parallel native and FRS complex Born weights, plus the equalities display_bornWeight_eq and display_normSq_eq, route through the same notion so that Hilbert display data and $F_{RS}[i]$ data agree on probabilities.
In the Recognition framework this is the finite, constructive stand-in for the Born rule on a discrete set of distinction alternatives, before continuum Hilbert space is recovered. It does not itself force $\phi$, the eight-tick octave, or $D=3$; those live in the T5–T8 forcing chain. It supplies the probability weights once amplitudes are on the finite display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.