displayAmp
plain-language theorem explainer
Maps a finite amplitude vector valued in the F_RS[i] scalar carrier to an ambient finite complex amplitude by componentwise evaluation into ℂ. Anyone comparing native F_RS Born weights or norms with the usual complex formulas cites this display. The body is a one-line pointwise application of the carrier evaluation map.
Claim. For each $N\in\mathbb{N}$ and each finite amplitude $\psi:\mathrm{Fin}(N+1)\to F_{RS}[i]$, the display $\mathrm{display}(\psi)$ is the ambient complex amplitude $\mathrm{Fin}(N+1)\to\mathbb{C}$ given by $i\mapsto \mathrm{eval}(\psi_i)$, where $\mathrm{eval}$ sends each $F_{RS}[i]$ expression to its complex value.
background
In the primitive recognition calculus, finite complex amplitudes are first carried by the finite-description scalar field $F_{RS}[i]$ rather than by ambient $\mathbb{C}$. An $F_{RS}[i]$ amplitude of length $N+1$ is a map from $\mathrm{Fin}(N+1)$ into the expression type for that carrier. The ambient side is the ordinary finite complex amplitude type $\mathrm{Fin}(N+1)\to\mathbb{C}$.
Componentwise evaluation of carrier expressions into $\mathbb{C}$ is the bridge: real and imaginary parts land in the minimal RS field, and Born weights are read either natively from the two $F_{RS}$ components or from the displayed complex values. The module treats ambient $\mathbb{C}$ as display only; the finite carrier is the substantive object.
Upstream, the complex amplitude abbreviation and the $F_{RS}[i]$ amplitude abbreviation fix the two vector types this map relates. Downstream lemmas then check that Born weight, squared norm, and normalization are invariant under the display.
proof idea
Definitional one-liner: on each index $i$, apply the carrier evaluation map to the $i$-th $F_{RS}[i]$ component. No lemmas are invoked; the resulting function is already a finite complex amplitude by the type of evaluation.
why it matters
This display is the hinge between native $F_{RS}[i]$ amplitudes and ambient complex language. It feeds the agreement theorems that the displayed complex Born weight equals the native formula, and that the displayed squared norm equals the sum of native Born weights. Normalization of an $F_{RS}$ amplitude is equivalent to complex normalization of its display.
Those facts assemble into the module headline: finite complex amplitudes can be carried by $F_{RS}[i]$; ambient $\mathbb{C}$ is only the display, and the display preserves carrier membership of real/imaginary parts, Born weights, and normalization. The Hilbert display completion reuses the same map as its embedding of an $F_{RS}$ amplitude into a finite Hilbert vector. In the Recognition foundation this keeps the amplitude calculus on the finite carrier while still speaking the language of ordinary complex QM amplitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.