display_normSq_eq
plain-language theorem explainer
For any finite F_RS[i] amplitude vector, the squared complex norm of its ambient display equals the sum of the native Born weights over the N+1 alternatives. Anyone proving normalization transfer or the F_RS[i] amplitude headline cites this identity. The proof is pure definitional equality (rfl).
Claim. Let $\psi$ be a finite amplitude vector of length $N+1$ with components in the finite-description carrier $F_{RS}[i]$. Writing $\mathrm{display}(\psi)$ for its ambient complex amplitude, one has $\|\mathrm{display}(\psi)\|^2 = \sum_{i=0}^{N} w(\psi,i)$, where $w(\psi,i)$ is the native Born weight $\mathrm{eval}(\mathrm{Re}\,\psi_i)^2 + \mathrm{eval}(\mathrm{Im}\,\psi_i)^2$.
background
In the Primitive Recognition Calculus, finite quantum amplitudes are carried natively by $F_{RS}[i]$ (a finite-description scalar field), not by ambient $\mathbb{C}$. An $F_{RS}[i]$ amplitude of rank $N$ is a map from $\mathrm{Fin}(N+1)$ into pairs of real/imaginary $F_{RS}[i]$ expressions. The display map sends each component through the evaluation homomorphism into $\mathbb{C}$, producing an ordinary finite complex amplitude vector.
The native Born weight at alternative $i$ is the sum of squares of the evaluated real and imaginary parts. On the complex side, the squared norm is the sum of complex Born weights over all alternatives. This lemma asserts that those two global norms coincide after display.
The surrounding module builds the bridge from native $F_{RS}[i]$ amplitudes to ambient complex amplitudes while preserving carrier membership, Born weights, and normalization.
proof idea
One-line rfl. After unfolding displayAmp, the native bornWeight, and DeltaAmplitude.complexNormSq, both sides are definitionally the same finite sum of squared real and imaginary evaluations, so no rewriting or lemmas are required.
why it matters
This identity is the norm half of the display bridge. It is conjoined into frsi_amplitude_headline (the module's main claim that ambient $\mathbb{C}$ is only a display of native $F_{RS}[i]$ amplitudes) and is the rewrite step in normalized_iff_display, which equates native and complex normalization.
Downstream, HilbertDisplayCompletion re-exports it as the Hilbert-display norm identity, feeds it into finite_hilbert_display_headline, and uses it to discharge the commuting square of normBridge (the valid-comparison bridge that observes by squared norm). Without this equality, normalization and Born-rule comparison through the native/display/observable path would not be definitionally aligned.
In the broader Recognition stack this is foundation plumbing rather than a forcing-chain step (T0–T8), but it underwrites the claim that finite Hilbert space is a faithful display of the recognition carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.