normalized_iff_display
plain-language theorem explainer
Native F_RS[i] amplitude normalization is equivalent to unit squared norm of the finite Hilbert display of that amplitude. Anyone citing the finite Hilbert display bridge or the F_RS[i] amplitude headline uses this equivalence. The proof rewrites by the display-norm identity and closes by definitional equality of the two normalization predicates.
Claim. For any $N\in\mathbb{N}$ and any finite $F_{RS}[i]$ amplitude $\psi$ on $N+1$ alternatives, $\psi$ is normalized (native squared norm equals $1$) if and only if the squared Hilbert norm of its display equals $1$.
background
In the primitive recognition calculus, finite amplitudes live natively over the scalar carrier $F_{RS}[i]$ (finite-description complex-like expressions), not over ambient $\mathbb{C}$. An $F_{RS}[i]$ amplitude $\psi$ is a map from $N+1$ alternatives into that carrier. Native normalization means the sum of Born weights equals one (equivalently, the native squared-norm formula equals one).
The Hilbert display sends each such $\psi$ to an ordinary finite complex amplitude vector. Squared norm on the display side is the usual sum of modulus-squared components. Upstream, display_normSq_eq records that this displayed complex squared norm equals the sum of native Born weights of $\psi$. The module frames finite Hilbert space as a display of native $F_{RS}[i]$ amplitudes, with squared norm as the observable protocol for valid comparison.
proof idea
Short rewrite proof. Apply the upstream identity that the squared norm of the display equals the native Born-weight sum (hence the native norm formula). After that rewrite, both sides of the biconditional are definitionally the same predicate (native Normalized versus normSq(display ψ) = 1), so rfl closes.
why it matters
This is the normalization leg of the finite Hilbert display bridge: native unit norm iff displayed unit norm. It is cited by the finite Hilbert display headline, which packages preservation of Born weights, squared norm, and normalization together with valid comparison through the native/display/observable bridge. It also aligns with the parallel normalization clause in the F_RS[i] amplitude headline (display preserves real/imaginary carrier membership, Born weights, and normalization; ambient $\mathbb{C}$ is display only).
In the Recognition framework this keeps quantum-style finite amplitudes on the finite-description carrier while recovering ordinary Hilbert normalization as a faithful display, rather than as ontology. It does not itself force dimension, $\phi$, or the eight-tick structure; those sit earlier in the forcing chain. It closes a local scaffolding point: normalization is not an extra axiom on the display side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.