eval_re_mem
plain-language theorem explainer
The real part of any finite-description complex scalar in F_RS[i], after display into ambient ℂ, still lands in the real RS carrier field rsField. Amplitude and carrier authors cite this to keep displayed Re(ψ) inside the countable RS subfield rather than free ℝ. The proof is a one-line reduction to the real-carrier soundness lemma on the real component.
Claim. For every finite-description complex scalar $z\in F_{RS}[i]$ (real and imaginary parts both $F_{RS}$ expressions), the real part of its display evaluation satisfies $(\mathrm{eval}\,z).\mathrm{re}\in rsField$, where $rsField\subseteq\mathbb{R}$ is the minimal RS carrier subfield generated by the named constants.
background
In the Primitive Recognition Calculus, physical scalars are not free elements of $\mathbb{R}$ or $\mathbb{C}$. The real carrier $F_{RS}$ is a finite-description expression language whose evaluation map lands in $rsField$, the subfield of $\mathbb{R}$ generated by the named RS constants (so it automatically contains $\mathbb{Q}$). Upstream soundness states: every carrier term evaluates into the countable field $rsField$; the finite-description syntax never escapes the carrier.
Complex amplitudes are handled by adjoining a formal $i$: an $F_{RS}[i]$ expression is a pair of real $F_{RS}$ expressions (real and imaginary parts). Display evaluation sends such a pair into ambient $\mathbb{C}$ by evaluating each component and forming $a+bi$. The present lemma isolates the real-part half of carrier membership after that display.
The module sits in the foundation layer that equips finite complex amplitudes for later Born-weight and normalization statements, without treating ambient $\mathbb{C}$ as the ontological carrier.
proof idea
One-line term proof. Unfold the complex display evaluation so that $(\mathrm{eval},z).\mathrm{re}$ is identified with the real-carrier evaluation of $z.\mathrm{re}$. Apply the upstream real soundness theorem $FRSCarrier.eval_mem$ to that real component, then close with simpa.
why it matters
This is one of the two membership legs (real and imaginary) that the module headline theorem packages. Downstream, frsi_amplitude_headline asserts that finite complex amplitudes can be carried by the finite-description scalar carrier $F_{RS}[i]$; ambient $\mathbb{C}$ is only the display, and the display preserves real/imaginary carrier membership, Born weights, and normalization. The fourth conjunct of that headline is exactly $\forall z,\ (\mathrm{eval},z).\mathrm{re}\in rsField\land(\mathrm{eval},z).\mathrm{im}\in rsField$, of which this lemma is the real half.
In the broader Recognition stack this keeps complex amplitudes inside the same countable RS field that hosts the forcing-chain constants and the $\varphi$-ladder arithmetic, rather than smuggling unrestricted complex reals into the foundation. It is bookkeeping, but the bookkeeping is load-bearing for any later claim that Born weights and normalizations computed from displayed amplitudes remain RS-native.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.