T_proper
plain-language theorem explainer
The exp/log-closed Recognition Science subfield of the reals is a proper subset: it cannot equal all of ℝ. Anyone arguing that RS constants and their generating operations live strictly below the continuum cites this. The proof is a one-line cardinality contradiction: the field is countable while ℝ is not.
Claim. Let $T\subseteq\mathbb{R}$ be the exp/log-closed Recognition Science subfield (the directed union of the countable stages that adjoin field operations, $\exp$, and $\log$ to the seeds). Then $T\neq\mathbb{R}$: as a set, $T$ is a proper subset of the continuum.
background
In the Primitive Recognition Calculus, the workspace for RS constants is built as a directed chain of stages $S_n$. Each stage is a countable subfield of $\mathbb{R}$; the next stage closes under field operations together with real $\exp$ and $\log$. The object $T$ is the directed union (supremum in the lattice of subfields)
$$T:=\bigsqcup_n S_n,$$
the smallest subfield of $\mathbb{R}$ containing the seeds and closed under those operations.
Upstream, $T$ is already known to be countable: a countable union of countable stages ($T$ countable). The classical fact that $\mathbb{R}$ itself is uncountable then forces $T$ to miss continuum-many reals. The local module goal is Item 1 of the deep half: every RS constant construction can be performed inside this countable carrier; the continuum is ambient only.
proof idea
Term-style reductio. Assume for contradiction that the underlying set of $T$ equals $\mathrm{Set.univ}$ (i.e. $T=\mathbb{R}$ as sets). Transport the already-proved countability of $T$ along that equality to conclude that $\mathbb{R}$ is countable. Discharge by the standard cardinality lemma that the reals are not countable (Cardinal.not_countable_real). No further structure of the stages is needed beyond countability.
why it matters
This is the properness half of the countable-carrier claim. Downstream, rs_operations_below_continuum packages $T$ as an explicit witness: a single countable subfield closed under field operations, $\exp$, and $\log$, already containing $\pi$, $\varphi$, and the derived constants. The unified headline cost_and_constants_share_one_countable_field strengthens the same carrier to be closed under the recognition cost $J$ as well.
In framework terms, the continuum is removed from the operations that build RS constants, not merely from their outputs. That supports the broader Primitive Recognition Calculus program: a single countable field fed by the $\delta$/ $J$ cost is enough workspace for the constants (including the $\alpha^{-1}$ band and the $\varphi$-ladder seeds), without treating uncountable $\mathbb{R}$ as an operational primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.