FRSIExpr
plain-language theorem explainer
Pairs two finite F_RS expressions as the real and imaginary parts of a complex scalar in the adjoined field F_RS[i]. Anyone building amplitudes, Born weights, or complex displays over the Recognition carrier cites this type. It is a plain product structure with decidable equality; no proof content.
Claim. An element of $F_{RS}[i]$ is a pair $(a,b)$ where $a,b$ are finite $F_{RS}$ expressions (terms built from rationals and the RS constant inventory $\varphi,\pi,e,\alpha^{-1}$, closed under field operations). The pair is interpreted as the complex number $a+bi$.
background
The Primitive Recognition Calculus builds a minimal real carrier field $F_{RS}$ whose elements are finite expressions: rationals together with the RS inventory $\varphi$, $\pi$, $e$, and $\alpha^{-1}$, closed under the field operations. That syntax is the inductive type of $F_{RS}$ expressions; evaluation lands in the real RS subfield of $\mathbb{R}$.
Complex amplitudes need $i$. Rather than enlarge the real syntax, this module adjoins an imaginary unit at the type level: a complex scalar is just a pair of real $F_{RS}$ expressions. Display into ambient $\mathbb{C}$ is componentwise evaluation. The local setting is finite-description amplitudes before any continuum limit or Born-rule extraction.
proof idea
No proof. The declaration is a two-field structure: real part and imaginary part, each an $F_{RS}$ expression, with derived decidable equality and a printer. Downstream eval is the one-line map sending the pair to $\langle\mathrm{eval}(re),\mathrm{eval}(im)\rangle$ in $\mathbb{C}$.
why it matters
This is the carrier type for complex scalars in the FRS amplitude stack. Downstream, eval displays into $\mathbb{C}$; eval_re/eval_im and the membership lemmas keep both parts inside the real RS field; FRSIAmp is the finite amplitude vector over these pairs; frsi_amplitude_headline, displayAmp, and bornWeight build the Born-rule side of the story.
In the Recognition framework the real carrier already packages the forced constants (including $\varphi$ from T6 and the $\alpha$ band). Complexification is the minimal step that lets recognition amplitudes live in $\mathbb{C}$ while remaining finitely described over that same inventory. It does not itself force dimensions or the eight-tick octave; it only supplies the scalar type those later layers evaluate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.