normalized_iff_display
plain-language theorem explainer
Native normalization of a finite F_RS[i] amplitude is equivalent to squared-norm one for its ambient complex display. Anyone citing the F_RS[i] amplitude headline or the finite Hilbert display bridge needs this equivalence. The proof unfolds both normalization predicates and rewrites via the display-norm identity.
Claim. For every $N\in\mathbb{N}$ and every finite amplitude $\psi$ with values in the scalar carrier $F_{RS}[i]$, the native normalization condition $\sum_i w_B(\psi,i)=1$ holds if and only if the displayed complex amplitude has squared norm one: $\|\mathrm{display}(\psi)\|^2=1$.
background
In the Primitive Recognition Calculus, finite complex amplitudes are not primitive objects over $\mathbb{C}$. They are carried by the finite-description scalar field $F_{RS}[i]$. An $F_{RS}[i]$ amplitude of length $N+1$ is a map $\mathrm{Fin}(N+1)\to F_{RS}[i]$-expressions; the ambient complex vector is only a display obtained by evaluating each component.
Native Born weight is computed from the two $F_{RS}$ components of each entry. Native normalization is the statement that those Born weights sum to one over the finite index set. On the display side, ComplexNormalized means the usual complex squared norm equals one.
The linking identity is that the displayed complex squared norm equals the sum of the native Born weights. That identity is definitional once display and Born weight are fixed, and it is the only upstream fact this equivalence needs.
proof idea
Term-mode proof by unfolding. Expand native Normalized (sum of Born weights equals one) and ambient ComplexNormalized (complex squared norm equals one). Rewrite the ambient side with display_normSq_eq, which states that the displayed complex squared norm is definitionally the same sum of native Born weights. The two sides become identical propositions.
why it matters
This is one of the three preservation clauses in the F_RS[i] finite amplitude headline: display preserves real/imaginary carrier membership, Born weights, and normalization. The headline packages nonnegativity of Born weights, the norm identity, this iff, and carrier membership of real and imaginary parts.
Downstream, the finite Hilbert display layer reuses the same pattern: native F_RS[i] normalization is exactly display-Hilbert normalization, feeding the finite Hilbert display headline that finite Hilbert space is only a display of native amplitudes. In the Recognition framework this keeps Born-rule structure on the finite carrier while treating ambient $\mathbb{C}$ as presentation, not ontology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.