const_mem

In Primitive Recognition Calculus one works with a countable list of named real constants $\kappa:\mathbb{N}\to\mathbb{R}$. The generable reals relative to $\kappa$ are defined as the subfield of $\mathbb{R}$ obtained by closing the range of $\kappa$ under the field operations (equivalently: everything reachable from those constants and the rationals by finitely many $+,\cdot,-,(\cdot)^{-1}$).

Formally, that carrier is $\mathrm{genField}(\kappa):=\mathrm{Subfield.closure}(\mathrm{range},\kappa)$. The present lemma records the most basic membership: each named constant itself sits inside its own generated subfield. Downstream work packages this with rational membership and closure under the four field operations into a single "operational carrier" certificate.

One-line term proof. The range of $\kappa$ is contained in the subfield closure of that range by the universal property of $\mathrm{Subfield.closure}$. Instantiating the range membership witness as $\langle n,\mathrm{rfl}\rangle$ places $\kappa(n)$ in the closed set, hence in $\mathrm{genField}(\kappa)$.

This is the named-constant half of the operational-carrier package. The parent theorem $\mathrm{genField_is_operational_carrier}$ conjoins five facts: rationals sit in the carrier, every named constant sits in the carrier (this lemma), and the carrier is closed under $+$, $\cdot$, and additive inverse. Without constant membership the carrier would be a bare algebraic hull rather than a genuine home for the named constants of the calculus.

In the broader Recognition foundation this supports the claim that the generable reals form a countable, operationally closed scalar domain strictly smaller than $\mathbb{R}$ (countability is the sibling fact that rules out the continuum). It is pure field-theoretic scaffolding, not a forcing-chain step (T0–T8), but it underwrites every later construction that treats named constants as live scalars inside a proper subfield of $\mathbb{R}$.