T_not_complete
plain-language theorem explainer
The countable exp/log-closed RS field T lacks the least-upper-bound property: some nonempty S ⊆ T is bounded above in T yet has no T-internal least upper bound. Independence theorems cite this to separate order-completeness from cost/field axioms. Proof is a one-line application of countable-subfield incompleteness to T.
Claim. There exists a nonempty set $S \subseteq T$ and some $b \in T$ with $x \le b$ for all $x \in S$, yet no $s \in T$ is a least upper bound of $S$ relative to $T$ (i.e., no $s \in T$ bounds $S$ and is $\le$ every upper bound of $S$ that lies in $T$).
background
In the Primitive Recognition Calculus, $T$ is the exp/log-closed RS field: the directed union $T = \bigsqcup_n S_n$ of an increasing chain of subfields of $\mathbb{R}$, starting from a generator closure and closing under exp/log steps. By construction $T$ is a subfield, and $T$ is countable (countable union of countable stages).
Order-completeness is phrased relative to a subfield $K$ via $\mathrm{IsLUBIn}, K, S, s$: $s \in K$ bounds $S$ and is $\le$ every $K$-element that bounds $S$. That is the internal supremum $K$ would supply if it were order-complete.
Upstream, every countable subfield of $\mathbb{R}$ fails this property: countability forces properness ($\mathbb{R}$ is uncountable), and any proper subfield fails LUB by a density-of-$\mathbb{Q}$ cut argument. The module isolates that incompleteness from the cost axioms that $T$ does satisfy.
proof idea
One-line term proof: instantiate the general lemma that every countable subfield of $\mathbb{R}$ lacks the least-upper-bound property, at $K = T$, using the already-proved fact that $T$ is countable. No extra case analysis; the witness set $S$ and the missing internal LUB are supplied by that lemma.
why it matters
This is the concrete incompleteness fact for the RS carrier $T$. Downstream it is packaged into two independence theorems: completeness is not forced by $J$-cost closure plus countability of $T$, and (stronger) not forced by the genuine cost laws (unit $J(1)=0$, reciprocal symmetry, nonnegativity) together with $J$-closure on the countable field $T$.
In Recognition Science terms, the continuous completion of the cost-closed field is an independent commitment, not a consequence of the recognition cost structure or the exp/log field axioms that build $T$. The continuum (order-completeness of $\mathbb{R}$) is exactly what countability cannot buy; $T$ is the working countable model that makes the separation sharp.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.