Amp
plain-language theorem explainer
Finite real amplitude data on N+1 alternatives is the type of maps from the finite index set {0,...,N} into the reals. Anyone proving delta-native Born weights, normalization, or finite norm-preservation cites this carrier type. It is a one-line type abbreviation with no proof obligations.
Claim. For each natural number $N$, a finite real amplitude vector on $N+1$ alternatives is a function $\psi:\{0,\ldots,N\}\to\mathbb{R}$ (equivalently, a real vector of length $N+1$).
background
The module develops a finite, delta-native amplitude calculus: real vectors on a discrete set of alternatives, squared entries as Born weights, and exact norm-one normalization. The carrier is deliberately finite: indices run over $\mathrm{Fin}(N+1)$, so every sum is a Finset sum and positivity is elementary.
Downstream, the Born weight of alternative $i$ is $(\psi_i)^2$, the squared norm is the sum of those weights, and a vector is normalized when that sum equals one. Norm-preserving maps are those that fix the squared norm pointwise; they automatically send normalized vectors to normalized vectors. The complex double-slit amplitude in the quantum layer is a separate, continuous construction; this abbrev is the real finite skeleton used by the primitive recognition calculus.
proof idea
One-line type abbreviation: identify the amplitude type with the function space $\mathrm{Fin}(N+1)\to\mathbb{R}$. No lemmas are applied and there is no tactic proof.
why it matters
This carrier underpins the whole delta-amplitude layer. Born weights, nonnegativity, the sum-to-one identity for normalized vectors, the NormPreserving predicate, and the headline theorem that packages nonnegativity, probability one, and preservation of normalization all quantify over it.
In Recognition Science terms it is the finite native core of the Born rule and of unitary evolution before Hilbert-space language is restored: squared real amplitudes give probabilities on a discrete alternative set, matching the discrete tick and recognition-event setting of the foundation chain. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; those live upstream in the forcing chain. Its job is to make the probability and norm-preservation statements type-check on finite data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.