display_bornWeight_eq
plain-language theorem explainer
On the finite Hilbert display of an F_RS[i] amplitude, the Born weight at each index equals the native F_RS[i] Born weight. Anyone citing the finite-Hilbert-display bridge or the headline that Hilbert space is only a display of native amplitudes needs this equality. The proof is a one-line term that reuses the complex-amplitude display identity.
Claim. For every finite $N$, every $F_{RS}[i]$-amplitude $\psi$ on $N+1$ alternatives, and every index $i$, the Born weight of the Hilbert display of $\psi$ at $i$ equals the native $F_{RS}[i]$ Born weight of $\psi$ at $i$: $w_{\mathrm{Hilb}}(\mathrm{display}(\psi), i) = w_{F_{RS}}(\psi, i)$.
background
In the Primitive Recognition Calculus, finite amplitudes live natively over the carrier $F_{RS}[i]$. An FRSIAmp N is a map from $N+1$ alternatives into that carrier (real and imaginary $F_{RS}$ components). The native Born weight at index $i$ is the sum of squares of the evaluated real and imaginary parts.
The Hilbert display embeds such an amplitude into an ambient finite complex vector (FiniteHilbertDisplay), via the complex display map. Born weight on that display is the ordinary complex Born weight (squared modulus of the complex component).
Upstream, the complex-amplitude layer already proves that displayed complex Born weight agrees with the native $F_{RS}[i]$ formula (by definitional equality). This module packages that fact at the Hilbert-display interface so later bridge theorems can quote a single local name.
proof idea
One-line term wrapper. The local display is definitionally displayAmp, and the local Hilbert bornWeight is definitionally the complex Born weight on that display. The proof therefore applies the upstream identity FRSComplexAmplitude.display_bornWeight_eq, which itself is rfl against the native formula $w_i = \mathrm{eval}(\mathrm{re})^2 + \mathrm{eval}(\mathrm{im})^2$.
why it matters
This equality is one of the two component identities in finite_hilbert_display_headline: finite Hilbert space is only a display of native $F_{RS}[i]$ amplitudes, and the bridge preserves Born weights, squared norm, and normalization. Without pointwise Born-weight agreement, comparison-by-norm through the native/display/observable bridge would not be valid.
In the Recognition framework this sits in the foundation layer that reconstructs ordinary quantum display structure from the recognition calculus, rather than taking Hilbert space as primitive. It does not itself force dimension, the eight-tick octave, or the $J$-cost uniqueness chain (T5–T8); it only closes the Born-weight half of the finite display bridge used by the headline theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.