normSq
plain-language theorem explainer
Squared Euclidean norm of a finite real amplitude vector on N+1 alternatives: the sum of component squares. Anyone building Born weights, normalization, or DFT-mode energies on the recognition lattice cites it. The body is the direct Finset sum of squares, not a derived identity.
Claim. For $N\in\mathbb{N}$ and a real amplitude vector $\psi:\{0,\ldots,N\}\to\mathbb{R}$, the squared norm is $\|\psi\|^2:=\sum_{i=0}^{N}\psi(i)^2$.
background
In the primitive recognition calculus, an amplitude vector on a finite menu of alternatives is a real map $\mathrm{Amp},N:=\mathrm{Fin}(N+1)\to\mathbb{R}$. The squared norm is the elementary $\ell^2$ energy of that vector: sum of squares over the $N+1$ slots.
The same module later defines Born weights as the individual squares and a normalized class of amplitude vectors whose total squared norm is one. A parallel complex squared-norm lives on the finite Hilbert display and routes through this real construction when the display is real-valued.
Upstream, the only structural dependency is the amplitude type itself. Sibling names such as Hamming weight or planar $|p|^2$ are unrelated carriers that happen to share the identifier; they do not constrain this definition.
proof idea
Pure definition: unfold to the universe sum $\sum_{i:\mathrm{Fin}(N+1)}(\psi,i)^2$. No lemmas, no tactics, no noncomputable choice beyond the ambient real arithmetic. Downstream proofs simply simp or unfold this name when they need the sum-of-squares form.
why it matters
This is the real $\ell^2$ energy that feeds Born-rule forcing: inner8_self_eq and normSq_eq_norm_sq identify the inner product of an eight-tick amplitude with its squared norm, which is the bridge from recognition amplitudes to probabilities.
On the constants side it underwrites gap-weight and alpha-genesis machinery. phiDFTAmplitude is the squared modulus of a $\varphi$-pattern DFT coefficient; diffEnergy8 and diffEnergy8_mode express discrete-difference energy of DFT-8 modes as a squared norm, recovering the factor $4\sin^2(k\pi/8)$ that appears in the spectral forcing certificate and the trig closure $|\omega_8^k-1|^2=4\sin^2(k\pi/8)$. That spectrum is the eight-tick octave landmark (T7) written in Fourier language.
With forty downstream uses, the definition is the shared energy primitive for finite recognition states, DFT projections, and the M6 spectral certificate rather than a one-off helper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.