FRSIAmp
plain-language theorem explainer
A finite complex amplitude of length N+1 whose entries live in the finite-description carrier F_RS[i], not ambient ℂ. Anyone building Born weights, display maps, or normalization for discrete RS amplitudes cites this type. It is a one-line type synonym: maps from Fin(N+1) into FRSIExpr.
Claim. For each $N \in \mathbb{N}$, an $F_{RS}[i]$ finite amplitude is a map $\psi : \{0,\ldots,N\} \to F_{RS}[i]$, where each value is a complex scalar whose real and imaginary parts are $F_{RS}$ expressions.
background
In the primitive recognition calculus, complex scalars are not taken as ambient $\mathbb{C}$ a priori. An $F_{RS}[i]$ expression (FRSIExpr) is a pair of $F_{RS}$ carrier expressions, one for the real part and one for the imaginary part. Evaluation into $\mathbb{C}$ is a display map only.
This module packages finite vectors of such scalars. The index set is $\mathrm{Fin}(N+1)$, matching the discrete amplitude type used by the continuum-bridge and double-slit amplitude constructions: a length-$(N+1)$ complex amplitude whose native arithmetic stays inside the finite-description field.
Upstream, FRSIExpr supplies the scalar type; the ambient complex amplitude and Born-weight infrastructure sit in DeltaAmplitude and related quantum modules, ready to receive a display of these native vectors.
proof idea
Pure abbreviation: FRSIAmp N is defined to be the function type Fin (N + 1) → FRSIExpr. No proof obligations; the body is the type synonym itself.
why it matters
This is the native carrier for finite RS complex amplitudes. Downstream, displayAmp sends an FRSIAmp into an ambient ComplexAmp; bornWeight computes $|\psi_i|^2$ from the two $F_{RS}$ components; nonnegativity, display agreement of Born weights and norm-squares, and the normalization equivalence all quantify over FRSIAmp.
The headline theorem frsi_amplitude_headline packages the claim that finite complex amplitudes can be carried by $F_{RS}[i]$, with ambient $\mathbb{C}$ only as display, preserving membership, Born weights, and normalization. Without this type, that discrete-to-display bridge has nothing to quantify over. It is definitional scaffolding for the F_RS[i] amplitude story, not a forcing-chain step (T0–T8), but it is how amplitudes enter the finite carrier before continuum display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.