Normalized
plain-language theorem explainer
Normalization of a finite recognition-field amplitude means the Born weights of its N+1 components sum to one. Anyone stating probability conservation or unitarity for native F_RS[i] amplitudes (or their complex display) cites this predicate. It is a one-line definitional equality, not a derived theorem: the sum of native Born weights equals 1.
Claim. For $N\in\mathbb{N}$ and a finite amplitude $\psi$ with $N+1$ components in the recognition field $F_{RS}[i]$, $\psi$ is normalized when $\sum_{k=0}^{N} w(\psi_k)=1$, where the native Born weight is $w(\psi_k)=\mathrm{eval}(\mathrm{Re}\,\psi_k)^2+\mathrm{eval}(\mathrm{Im}\,\psi_k)^2$.
background
The module builds finite complex amplitudes over the recognition carrier $F_{RS}[i]$. A finite amplitude is a map from $\mathrm{Fin}(N+1)$ into pairs of carrier expressions (real and imaginary parts). Display maps those pairs into ordinary complex numbers.
Native Born weight of component $i$ is the sum of squares of the evaluated real and imaginary carrier parts. Upstream, the real finite-amplitude layer defines Born weight as a plain square and calls an amplitude normalized when its squared norm equals one. The local doc states the design intent: normalization over $F_{RS}[i]$ is exactly normalization of the ambient complex display.
Thus this predicate is the $F_{RS}$-native form of the unit-sum Born condition used throughout the primitive recognition calculus.
proof idea
Definitional, not a proof. The predicate is the proposition that the finite sum over $\mathrm{Fin}(N+1)$ of the native Born weights equals $1$. No tactics, no lemmas, no reduction steps.
why it matters
This is the unitarity gate for native $F_{RS}[i]$ amplitudes before they are displayed into complex Hilbert space. Downstream it is consumed by the delta-amplitude headline results (Born weights sum to one; the amplitude headline theorem), by chemistry radius and electron-affinity proxies that need normalized shell weights, by cosmic-$Z$ scale-affinity structures that treat normalized ledger fractions, and by cost/RCL uniqueness arguments that rely on normalized reciprocal costs.
In the Recognition framework it sits under the primitive recognition calculus that feeds the forcing chain and the Recognition Composition Law: without a crisp native normalization predicate, Born-rule statements and display-agreement lemmas cannot even be stated. It does not itself force $J$-uniqueness or $\varphi$, but it is the bookkeeping layer those later steps assume when amplitudes are treated as probabilities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.