finite_hilbert_display_headline
plain-language theorem explainer
Finite Hilbert space is only a display of native F_RS[i] amplitudes: squared norm, Born weights, and normalization all transport exactly, and norm comparison is valid precisely when the native Born-weight totals agree. Anyone citing the finite-display bridge or the Delta-native strong-closure certificate needs this package. The proof is a four-conjunct term that assembles already-proved display equalities and the native comparison lemma for the norm bridge.
Claim. For every $N\in\mathbb{N}$ and every native finite amplitude $\psi$ with $N+1$ slots: (i) $\|\mathrm{display}(\psi)\|^2$ equals the sum of the native Born weights of $\psi$; (ii) each displayed Born weight equals the corresponding native Born weight; (iii) $\psi$ is normalized if and only if $\|\mathrm{display}(\psi)\|^2=1$; (iv) two amplitudes are validly comparable under the norm bridge if and only if their native Born-weight totals coincide.
background
In the Primitive Recognition Calculus, finite amplitudes live natively as F_RS[i]-valued data (real and imaginary F_RS components per slot). The native Born weight of slot $i$ is the sum of squares of the evaluated real and imaginary parts; the native squared norm is the sum of those weights over $\mathrm{Fin}(N+1)$. Normalization means that squared norm equals one.
A display map sends each native amplitude to an ordinary complex finite vector (the Hilbert-space picture). Upstream lemmas already record that the displayed complex squared norm equals the sum of native Born weights, and that each displayed Born weight equals the native formula (both by definitional reduction). A separate norm bridge is the comparison channel that asks whether two amplitudes have equal total weight.
This module packages those facts into a single headline: finite Hilbert space is a faithful display of the native finite F_RS calculus for norm, Born weights, normalization, and norm-based comparison.
proof idea
Term-mode four-conjunct package. The first conjunct is display_normSq_eq (displayed squared norm equals the sum of native Born weights). The second is display_bornWeight_eq (componentwise Born-weight agreement). The third is the local normalized_iff_display bridge between native normalization and displayed unit norm. The fourth applies ValidComparison.validComparison_iff_native at the norm bridge, reducing valid comparison of two amplitudes to equality of their native Born-weight totals. No new algebra is performed here.
why it matters
This is the finite-Hilbert display headline for the Primitive Recognition Calculus: it states that ordinary finite Hilbert space is only a presentation layer over native F_RS[i] amplitudes, with Born weights, squared norm, normalization, and norm comparison preserved exactly. Downstream it is consumed by strongClosureCertificate in Delta-native strong closure, which assembles the closed Delta-native theorem surface (real forgetful display, generable carrier, certified analytic protocols, and related entries). In framework terms it supports the claim that quantum-looking finite amplitudes and Born weights arise as displays of recognition-native data rather than as primitive Hilbert structure. It does not itself force dimension, the eight-tick octave, or the J-cost uniqueness chain; those live upstream in the forcing chain (T5–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.