eval_im
plain-language theorem explainer
The imaginary part of the complex display of an F_RS[i] scalar equals the F_RS carrier evaluation of its imaginary component. Anyone assembling complex amplitudes or Born weights in the primitive recognition calculus cites this projection lemma. The equality is definitional: a one-line reflexivity proof.
Claim. For every finite-description complex scalar $z\in F_{RS}[i]$ (with real and imaginary parts themselves $F_{RS}$ expressions), $\mathrm{Im}(\mathrm{display}(z)) = \mathrm{eval}_{F_{RS}}(z_{\mathrm{im}})$.
background
The module builds complex amplitudes over the Recognition Science carrier field $F_{RS}$. An FRSIExpr is a pair of $F_{RS}$ expressions $(z_{\mathrm{re}}, z_{\mathrm{im}})$, the finite-description model of a scalar in the formal extension $F_{RS}[i]$.
Display sends such a pair into the ambient complex field by evaluating each component via the carrier evaluator and packing the results as a complex number. The real-part companion states the same fact for $\mathrm{Re}$. Together they pin how complex display factors through the two real carrier evaluations.
Local setting is the primitive recognition calculus: amplitudes, Born weights, and norm-squared identities are written against this display, so componentwise projection lemmas keep later equalities inside the real carrier rather than in $\mathbb{C}$.
proof idea
Term-mode proof by rfl. By definition, display of $z$ is the complex number whose imaginary part is exactly FRSCarrier.eval z.im, so the stated equality holds definitionally with no rewrite or lemma application.
why it matters
Sits in the FRS complex-amplitude layer beside eval_re, membership lemmas, displayAmp, and bornWeight. It lets later identities (Born weight nonnegativity, norm-squared display equalities) reason about imaginary parts as ordinary $F_{RS}$ values rather than as opaque complex projections.
No downstream users are recorded yet; the lemma is infrastructure for amplitude bookkeeping rather than a forcing-chain step. It does not touch T5–T8, the RCL, or the mass ladder; it only stabilizes the complex display interface used when recognition amplitudes are written over $F_{RS}[i]$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.