display_normSq_eq
plain-language theorem explainer
For any finite F_RS[i] amplitude, the squared Hilbert-display norm equals the sum of the native F_RS[i] Born weights. Anyone proving normalization transfer or the finite-Hilbert display headline cites this identity. The proof is a one-line re-export of the corresponding F_RS complex-amplitude lemma.
Claim. Let $\psi$ be a finite amplitude over the scalar carrier $F_{RS}[i]$ with $N+1$ alternatives. Writing $\mathrm{display}(\psi)$ for its image in the finite complex Hilbert display, one has $\|\mathrm{display}(\psi)\|^2 = \sum_{i=0}^{N} w_{\mathrm{native}}(\psi,i)$, where $w_{\mathrm{native}}$ is the native Born weight built from the real and imaginary $F_{RS}[i]$ components.
background
In the Primitive Recognition Calculus, finite complex amplitudes are carried natively by $F_{RS}[i]$ (the finite-description scalar carrier). Ambient $\mathbb{C}$ and finite Hilbert space appear only as displays. An FRSIAmp N is a map from $N+1$ alternatives into that carrier; each component has real and imaginary parts evaluated to reals.
The native Born weight of alternative $i$ is $\mathrm{eval}(\mathrm{re})^2 + \mathrm{eval}(\mathrm{im})^2$. The Hilbert-display squared norm is the usual sum of complex Born weights on the displayed vector. The sibling display map sends a native amplitude into FiniteHilbertDisplay N (a finite complex amplitude vector).
Upstream, FRSComplexAmplitude.display_normSq_eq already states that the displayed complex norm equals the sum of native Born weights, proved by definitional equality (rfl). This module re-states that fact in Hilbert-display vocabulary so the finite-Hilbert bridge can quote a local name.
proof idea
One-line term wrapper: apply FRSComplexAmplitude.display_normSq_eq to $\psi$. No extra algebra. The upstream lemma itself is definitional (rfl), so the identity is pure unfolding of display, normSq, and native bornWeight into the same finite sum.
why it matters
This is the squared-norm half of the finite Hilbert display bridge. Downstream, normalized_iff_display rewrites native normalization as normSq (display ψ) = 1 via this equality; normBridge uses it as the commuting square between native sum-of-Born-weights and display squared norm; and finite_hilbert_display_headline packages it as the first conjunct of the headline that finite Hilbert space is only a display of native $F_{RS}[i]$ amplitudes.
It also feeds the parallel F_RS complex-amplitude headline (frsi_amplitude_headline), which asserts that ambient $\mathbb{C}$ is display-only while Born weights and normalization are preserved. In Recognition terms, this keeps the Born rule and normalization on the native carrier rather than smuggling structure from ambient Hilbert space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.