Normalized
plain-language theorem explainer
A finite real amplitude vector is normalized precisely when the sum of its squared components equals one. Anyone working with Born weights, finite recognition displays, or unit-norm states on Fin(N+1) cites this predicate. It is a one-line definitional abbreviation of the squared-norm condition, not a proved theorem.
Claim. For $N \in \mathbb{N}$ and a real amplitude $\psi : \mathrm{Fin}(N+1) \to \mathbb{R}$, $\psi$ is normalized when $\sum_{i} \psi(i)^2 = 1$.
background
In the primitive recognition calculus, a finite real amplitude is a map from the discrete index set $\mathrm{Fin}(N+1)$ into $\mathbb{R}$. The squared norm of such a vector is the ordinary Euclidean sum of squares over all indices. Normalization is the unit-sphere condition for that sum.
The same module defines Born weights as the individual squared components and proves they are nonnegative. A parallel complex-display notion of normalization (sum of complex Born weights equals one) lives in the FRS complex-amplitude layer; the real version here is the elementary special case used for finite real displays.
Local setting: DeltaAmplitude builds the finite real amplitude layer that feeds Born-rule bookkeeping and the delta-amplitude headline results.
proof idea
Definitional: the predicate is literally the equality of the squared-norm function to $1$. No tactics or lemmas are required. Downstream proofs unfold this abbreviation and rewrite with the sum-of-squares definition of the squared norm.
why it matters
Unit-norm amplitudes are the admissible states for Born-weight calculus. In-module consumers include the theorem that Born weights of a normalized amplitude sum to one, and the delta-amplitude headline that packages the finite Born rule. The same normalization language appears in reciprocal-cost axioms (cost vanishing at the fixed point), D'Alembert/RCL uniqueness scaffolding, cosmic-Z scale-affine laws (normalized ledger fractions with fixed endpoints), and chemistry proxies that speak of normalized radii or affinities within a period. It is the shared unit-sphere gate for finite recognition displays before complex or Hilbert completion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.