complexNormSq
plain-language theorem explainer
Defines the squared Euclidean norm of a finite complex amplitude on N+1 alternatives as the sum of per-component Born weights |ψ_i|². Anyone working with finite Born normalization, unitary-style maps, or the F_RS[i] display bridge cites it. The body is a direct Finset sum of the componentwise complex Born weights.
Claim. For $N \in \mathbb{N}$ and a complex amplitude vector $\psi : \mathrm{Fin}(N+1) \to \mathbb{C}$, the squared norm is $\|\psi\|^2 := \sum_{i} \bigl(\mathrm{Re}(\psi_i)^2 + \mathrm{Im}(\psi_i)^2\bigr) \in \mathbb{R}$.
background
In the primitive recognition calculus, a finite complex amplitude is a map $\psi : \mathrm{Fin}(N+1) \to \mathbb{C}$. The componentwise complex Born weight is the ordinary modulus squared $|\psi_i|^2 = \mathrm{Re}(\psi_i)^2 + \mathrm{Im}(\psi_i)^2$.
This module builds the finite native stand-in for Hilbert-space structure used by Recognition Science: normalization means total squared norm one, and norm-preserving maps are the finite analogue of unitary evolution. The real (non-complex) sibling already has an analogous squared-norm sum; the complex version is the display-side counterpart used when ambient $\mathbb{C}$ is only a presentation layer.
Upstream, complexBornWeight supplies each summand. Downstream display bridges equate this sum to the native finite $F_{RS}[i]$ Born-weight total, so the complex squared norm is the bookkeeping object that makes normalization statements transport between carrier and display.
proof idea
Definitional, not a proof. Unfold to a single Finset sum: over all $i : \mathrm{Fin}(N+1)$, add the complex Born weight of $\psi$ at $i$. No lemmas are applied; noncomputability is inherited from real arithmetic on complex components.
why it matters
This is the scalar that ComplexNormalized equates to one and that ComplexNormPreserving requires to be invariant. The theorem complex_born_weights_sum_one is literally a simp rewrite of normalization through this definition; complexNormSq_nonneg is the corresponding nonnegativity fact.
It is the display-side norm in the F_RS[i] amplitude headline: display_normSq_eq states that the complex squared norm of the displayed amplitude equals the sum of native born weights, and frsi_amplitude_headline packages that agreement with normalization transport. HilbertDisplayCompletion also reuses it as its normSq.
In framework terms it is bookkeeping for finite Born structure on the recognition side of quantum display, not a forcing-chain (T0–T8) step. It lets later results talk about unitarity-style maps and normalized states without committing to infinite-dimensional Hilbert space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.