T_countable
plain-language theorem explainer
The exp/log-closed Recognition Science subfield T of the reals is a countable set. Anyone showing that RS field operations, cost, and constants live strictly below the continuum cites this fact. The proof rewrites T as the countable union of the stages S n and applies countable-union-of-countables via stage countability.
Claim. Let $T\subseteq\mathbb{R}$ be the exp/log-closed Recognition Science subfield obtained as the directed supremum of the stage chain $S_n$. Then $T$, viewed as a subset of $\mathbb{R}$, is countable.
background
In this module one builds a single subfield of $\mathbb{R}$ closed under the operations that generate Recognition Science constants: field operations, real exponential, and real logarithm. Start from a finite seed set gens (including $\pi$ and $\varphi$), take its subfield closure as stage $S_0$, and iterate a successor that adjoins exp and log images. The stages form a directed chain $S_n$.
The object $T$ is defined as the subfield supremum $T:=\bigsqcup_n S_n$. Upstream, $T_{\mathrm{coe}}$ identifies the underlying set of $T$ with the set-theoretic union $\bigcup_n(S_n:Set,\mathbb{R})$, using directedness of the chain. Separately, $S_{\mathrm{countable}}$ records that each stage is countable: each is a subfield generated by a countable set (the base case uses finite generation of the seed closure).
Countability of $T$ is the bridge from the inductive stage construction to global claims that the RS workspace need not be the continuum.
proof idea
One-line term proof after a rewrite. First apply $T_{\mathrm{coe}}$ to replace $(T:Set,\mathbb{R})$ by $\bigcup_n(S_n:Set,\mathbb{R})$. Then invoke Set.countable_iUnion on the family $n\mapsto S_n$, feeding the pointwise theorem $S_{\mathrm{countable}},n$. No further field or exp/log reasoning is required; the result is pure countable-set arithmetic on the stage filtration.
why it matters
This is the countability half of the "operations below continuum" package. Downstream, $T_{\mathrm{proper}}$ uses it with non-countability of $\mathbb{R}$ to show $T\neq\mathbb{R}$. The existence theorems rs_operations_below_continuum and cost_and_constants_share_one_countable_field package $T$ as a single countable carrier closed under exp, log, and (in the latter) the canonical cost $J$, already containing the seeds and derived constants.
On the independence side, T_not_complete, completeness_not_forced_by_cost_axioms, and completeness_not_forced_by_genuine_cost_laws use countability of $T$ as a witness that a $J$-closed field model of the genuine cost laws need not be order-complete: $T$ fails the LUB property while $\mathbb{R}$ has it. Order-completeness is therefore an independent commitment, not forced by cost axioms or field structure alone. In framework terms this keeps the primitive recognition calculus on a countable carrier, separating continuum completion from the forcing chain and RCL content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.