eval_re
plain-language theorem explainer
The real part of the complex display of an F_RS[i] expression equals the ordinary F_RS evaluation of its real component. Anyone wiring complex amplitudes or Born weights in the primitive recognition calculus cites this. The equality is definitional: a one-line reflexivity proof after unfolding the display.
Claim. For every finite-description complex scalar $z\in F_{RS}[i]$ (with real and imaginary parts themselves $F_{RS}$ expressions), $\mathrm{Re}(\mathrm{eval}(z)) = \mathrm{eval}_{F_{RS}}(z_{\mathrm{re}})$.
background
In the primitive recognition calculus, $F_{RS}$ is the carrier of finitely described real scalars built from certified analytic protocols. An $F_{RS}[i]$ expression is a pair of such carriers: real and imaginary parts, packaged as a complex scalar with a finite description.
Display (here called eval) sends that pair into the ambient complex field $\mathbb{C}$ by evaluating each component and forming $a+bi$. The real-part projection on $\mathbb{C}$ is the usual one. Upstream, real evaluation of an $F_{RS}$ expression is the protocol value (supremum of lower endpoints, equivalently the unique real in every certified interval).
This module sits under Foundation and feeds Hilbert-display and Born-weight constructions for recognition amplitudes.
proof idea
Term-mode proof by rfl. Unfolding the definition of complex display on an $F_{RS}[i]$ pair makes the real component exactly the real $F_{RS}$ evaluation, so the two sides are definitionally equal. No lemmas are applied.
why it matters
Complex amplitudes in Recognition Science are not free $\mathbb{C}$-data; they are pairs of certified $F_{RS}$ expressions. This lemma is the real-part half of that interface: it lets later arguments (Born weights, squared norms, Hilbert display) replace $\mathrm{Re}(\mathrm{eval},z)$ by a pure real $F_{RS}$ evaluation without bookkeeping.
Sibling facts cover the imaginary part, membership of those values, the amplitude type, display into finite Hilbert space, and nonnegativity of Born weight. No downstream users are wired yet in the graph, so this is infrastructure for the complex layer rather than a step in the T0–T8 forcing chain. It does not touch J-uniqueness, $\phi$, or the eight-tick octave directly; it only keeps the amplitude display honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.