eval
plain-language theorem explainer
Componentwise display of a finite-description complex scalar in F_RS[i] into the ambient field ℂ. Real and imaginary parts are ordinary F_RS expressions; each is evaluated by the real carrier map and paired as a complex. Anyone working with F_RS[i] amplitudes, Born weights, or Hilbert displays cites this as the scalar embedding. The body is a one-line pair constructor.
Claim. There is a noncomputable map $\mathrm{eval}: F_{RS}[i]\text{-Expr}\to\mathbb{C}$ sending a complex expression $z=(z_{\mathrm{re}},z_{\mathrm{im}})$ to the complex number whose real and imaginary parts are the real carrier evaluations of $z_{\mathrm{re}}$ and $z_{\mathrm{im}}$ respectively: $\mathrm{eval}(z)=\langle\mathrm{eval}_{\mathbb{R}}(z_{\mathrm{re}}),\,\mathrm{eval}_{\mathbb{R}}(z_{\mathrm{im}})\rangle$.
background
In the primitive recognition calculus, $F_{RS}$ expressions are finite syntactic descriptions of real scalars built from the recognition carrier. Their evaluation lands in $\mathbb{R}$ via the real carrier map (the same style of value/eval used for certified analytic protocols and $\Delta$-real protocols: a denoted real obtained by evaluating the expression tree).
An $F_{RS}[i]$ expression is the complex analogue: a pair of $F_{RS}$ expressions, one for the real part and one for the imaginary part. The ambient target is ordinary $\mathbb{C}$, not a custom complex carrier. This module sits between the real $F_{RS}$ carrier and the finite Hilbert display of complex amplitudes: once scalars embed into $\mathbb{C}$, one can form amplitude vectors, squared norms, and Born weights.
Upstream, real evaluation is already fixed (carrier eval, protocol value as a supremum of lower endpoints). This definition only lifts that real map componentwise.
proof idea
Pure definition, not a proved theorem. On input $z:\mathrm{FRSIExpr}$, return the complex pair whose components are FRSCarrier.eval applied to $z.\mathrm{re}$ and $z.\mathrm{im}$. No lemmas, no tactics: a single lambda that reuses the real carrier evaluation twice and packs the results as an element of $\mathbb{C}$.
why it matters
Recognition Science needs complex amplitudes (Born weights, finite Hilbert displays) while keeping every scalar finitely described in the $F_{RS}$ language. This display is the bridge: it turns an $F_{RS}[i]$ expression into an ordinary complex number so downstream objects (FRSIAmp, displayAmp, bornWeight, and the Hilbert-display completion that packages amplitudes as finite vectors) can talk about $\mathbb{C}$-valued physics without leaving the certified expression layer.
It does not itself force $\phi$, the eight-tick octave, or $D=3$; those live in the T0–T8 forcing chain. Its role is infrastructural inside Primitive Recognition Calculus: without a coherent $\mathbb{C}$-display, complex amplitude identities and Born nonnegativity cannot even be stated in Lean. The dependency graph lists no external used_by edges yet; in-module siblings (eval_re, eval_im, display and Born lemmas) are the immediate consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.