delta_amplitude_headline
plain-language theorem explainer
Finite real amplitude vectors on N+1 alternatives have nonnegative Born weights ψ_i²; when the squared norm is one those weights sum to one; and any squared-norm-preserving map sends normalized amplitudes to normalized amplitudes. Anyone citing the delta-native Born package or the strong-closure certificate will use this headline. The proof is a three-component term that packages the three already-proved component lemmas.
Claim. For every $N\in\mathbb{N}$ and every real amplitude vector $\psi:\{0,\ldots,N\}\to\mathbb{R}$: (i) $\psi_i^2\ge 0$ for all $i$; (ii) if $\sum_j\psi_j^2=1$ then $\sum_i\psi_i^2=1$; (iii) if $U$ satisfies $\sum_i(U\psi)_i^2=\sum_i\psi_i^2$ for all $\psi$, then $U$ sends normalized amplitudes to normalized amplitudes.
background
This module builds the finite, delta-native amplitude layer of Recognition Science: real vectors on a finite set of alternatives, before any Hilbert-space completion. An amplitude is a map $\psi:\mathrm{Fin}(N+1)\to\mathbb{R}$. The Born weight of alternative $i$ is simply $\psi_i^2$. The squared norm is the sum of those weights; $\psi$ is normalized when that sum equals one.
A map $U$ on amplitude space is called norm-preserving when it fixes the squared norm of every vector. The module doc frames this as the finite native core of unitary evolution; full Hilbert-space unitaries are the display-completion version. Upstream, the component facts already exist: nonnegativity of each Born weight (by positivity of squares), the sum-to-one identity for normalized vectors, and the elementary transfer of normalization along norm-preserving maps.
The surrounding foundation links this discrete amplitude calculus to the recognition evolution family (matrix exponentials on finite registers) and to RS-native units with $c=1$, but the present statement is purely algebraic on finite real vectors.
proof idea
Term-mode packaging, not a new argument. The proof is the triple $\langle$bornWeight_nonneg, $\lambda,h_\psi.,$born_weights_sum_one $h_\psi$, $\lambda,h_U,h_\psi.,$normalized_of_normPreserving $h_U,h_\psi\rangle$.
First conjunct is the already-proved nonnegativity of each squared component. Second applies the sum-of-Born-weights identity under the normalization hypothesis. Third applies the lemma that any squared-norm-preserving map sends normalized vectors to normalized vectors. No tactics beyond the anonymous fun binders; the three component theorems do all the work.
why it matters
This is the public headline for the finite real Born package: nonnegativity, probability normalization, and invariance under norm-preserving evolution, stated as one conjunction. Downstream it is consumed by strongClosureCertificate in DeltaNativeStrongClosure, which assembles the closed delta-native theorem surface (real forgetful display, generable carrier, certified analytic protocols, certified transformers).
In the Recognition framework this sits under the primitive recognition calculus that precedes continuum QM display. It is the finite native core of the Born rule and of unitary preservation of probability, matching the finite-register philosophy used for the eight-tick octave and the Hamiltonian emergence operator on $C^N$ (no infinite-dimensional Stone theory required). It does not itself force $\phi$, $D=3$, or the RCL; it certifies that the amplitude layer used by those later steps already has a clean probability interpretation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.