eval_im_mem
plain-language theorem explainer
Every displayed imaginary part of a finite-description complex scalar stays inside the real RS carrier field. Anyone assembling complex amplitudes over F_RS[i] cites this to keep ambient ℂ as display only. The proof is a one-line reduction: carrier soundness applied to the imaginary component.
Claim. For every finite-description complex scalar $z$ whose real and imaginary parts are RS carrier expressions, the imaginary part of its evaluation in $\mathbb{C}$ lies in the minimal RS carrier field $F_{\mathrm{RS}}\subseteq\mathbb{R}$.
background
The module builds complex amplitudes whose coordinates are finite-description scalars over the Recognition Science carrier, not free elements of ambient $\mathbb{C}$. An FRSIExpr is a pair of carrier expressions (real and imaginary parts), each drawn from the syntax of the real RS field.
The minimal carrier field $F_{\mathrm{RS}}$ is the subfield of $\mathbb{R}$ generated by the named RS constants (hence automatically containing $\mathbb{Q}$). Display evaluation sends a carrier expression into $\mathbb{R}$ (and a complex pair into $\mathbb{C}$), but soundness demands the image never leave $F_{\mathrm{RS}}$.
Upstream, carrier soundness states: every carrier term evaluates into the countable field rsField; the finite-description syntax never escapes the carrier. The present lemma is the imaginary-part half of that guarantee for complex scalars.
proof idea
One-line wrapper. Unfold the complex display evaluation, then apply carrier soundness (FRSCarrier.eval_mem) to the imaginary-part expression z.im. Simplification closes membership of (eval z).im in $F_{\mathrm{RS}}$.
why it matters
Feeds the module headline frsi_amplitude_headline: finite complex amplitudes are carried by $F_{\mathrm{RS}}[i]$; ambient $\mathbb{C}$ is only the display, and that display preserves real/imaginary carrier membership, Born weights, and normalization. Without both real and imaginary membership lemmas, the fourth conjunct of the headline (carrier closure of displayed parts) fails.
In the Primitive Recognition Calculus stack this keeps complex amplitudes on the same countable carrier used for real RS quantities, so Born weights and normalization stay inside the RS-native arithmetic rather than drifting into transcendental ambient junk. It is local foundation plumbing, not a forcing-chain step (T0–T8), but it is required before double-slit style amplitude sums can be stated over the finite carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.