display
plain-language theorem explainer
Maps a finite Recognition Science amplitude valued in the field F_RS[i] to an ambient complex vector on the same finite set of distinction alternatives. Anyone working Born weights, Hilbert norms, or display seams (alpha, ionization, kinematic ratios) cites this as the entry into ordinary complex Hilbert space. The body is a one-line alias of the componentwise evaluation map that sends each F_RS[i] entry to ℂ.
Claim. For each $N \in \mathbb{N}$ and each finite amplitude $\psi : \{0,\ldots,N\} \to F_{RS}[i]$, the display of $\psi$ is the ambient complex vector $(\mathrm{eval}(\psi_0),\ldots,\mathrm{eval}(\psi_N)) \in \mathbb{C}^{N+1}$.
background
The module sits in the Primitive Recognition Calculus layer and builds a finite Hilbert display from F_RS[i]-valued amplitudes. An F_RS[i] amplitude is a map from Fin(N+1) into the native Recognition field expressions; the finite Hilbert display carrier is simply Fin(N+1) → ℂ, an ambient complex vector indexed by the same distinction alternatives.
Upstream, the complex-amplitude module already defines the componentwise evaluation that turns each F_RS[i] entry into a complex number ("Display an F_RS[i] finite amplitude as an ambient finite complex amplitude"). The present definition re-exports that map under the Hilbert-display name so later norm, Born-weight, and normalization lemmas can speak in ordinary ℂ language without carrying the F_RS[i] type.
Sibling abbreviations in the same file (squared norm, Born weight, norm bridge) all consume this display, so the type change is the seam between native RS amplitudes and classical finite-dimensional Hilbert space.
proof idea
One-line wrapper: the body is exactly the upstream componentwise evaluation map applied to ψ. No extra coercion, no normalization, no proof obligations beyond noncomputability inherited from the complex evaluation of F_RS[i] expressions.
why it matters
This is the standard display seam from native F_RS[i] amplitudes into ℂ^{N+1}. Downstream it is consumed heavily: chemistry uses it for φ-scaled ionization and band multipliers; the AlphaGenesis stack (calibration forcing, loop certificate, resummation forcing) routes channel-budget and self-similar dressing through display-level quantities; KDisplay and KDisplayCore compare kinematic ratios and speed-of-light identities on the displayed vectors.
In the broader framework it is the finite-dimensional analogue of the RS-to-classical bridge: once amplitudes live in ℂ, ordinary squared norms and Born weights become available, which later feed the alpha band, mass-ladder displays, and coherence-tick energy predictions. It does not itself force constants (T5–T8 live upstream); it only opens the Hilbert language those results need when they are shown to a classical observer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.