normSq
plain-language theorem explainer
Squared Euclidean norm of a finite complex Hilbert display vector: sum of pointwise Born weights over the N+1 distinction slots. Cited wherever Born normalization, eight-tick DFT mode energies, or gap-weight projections need a real scalar from a display vector. Definition is a one-line alias of the complex-amplitude squared-norm.
Claim. For $N\in\mathbb{N}$ and $v:\{0,\ldots,N\}\to\mathbb{C}$, the squared norm is $\|v\|^2:=\sum_{i=0}^{N}|v_i|^2$ (equivalently, the sum of the pointwise complex Born weights of $v$).
background
The finite Hilbert display is the ambient carrier $\mathrm{Fin}(N+1)\to\mathbb{C}$: a complex vector indexed by the finite set of distinction alternatives. It is the display image of an $F_{RS}[i]$ complex amplitude under the module's display map, so the same vector can be read either as a recognition amplitude or as a plain Hilbert vector.
Upstream, complexNormSq on a complex amplitude is defined as the sum over all slots of the complex Born weight (modulus squared of each component). The real-amplitude sibling sums ordinary squares. Both live in the primitive recognition calculus that builds finite amplitudes before the Hilbert completion step.
This module sits in Foundation.PrimitiveRecognitionCalculus and packages the display completion: once amplitudes are shown as Hilbert vectors, norms, Born weights, and normalization predicates are stated uniformly on that carrier.
proof idea
One-line definitional wrapper: the squared norm of a finite Hilbert display vector is exactly the upstream complex-amplitude squared norm applied to the same function. No extra algebra; the types coincide because the display carrier is definitionally $\mathrm{Fin}(N+1)\to\mathbb{C}$.
why it matters
Gives the real scalar that Born-rule forcing and spectral gap-weight machinery consume. Downstream, BornRuleForcing equates the display inner product with itself to this norm and bridges it to the standard complex norm-square. GapWeight.Projection uses the same scalar for DFT-8 column orthonormality, total discrete-difference energy, and the mode identity that difference energy equals $|\omega_8^k-1|^2$. AlphaGenesis.SpectralForcing packages the trig closure $|\omega_8^k-1|^2=4\sin^2(k\pi/8)$ into the spectral forcing certificate; phi-DFT mode amplitudes are likewise defined via squared modulus.
In the Recognition chain this is the finite-display norm that feeds eight-tick (T7) spectral weights and the alpha-band forcing path: without a uniform $|\cdot|^2$ on the display, mode energies and Born normalization cannot be stated in one place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.