countable_subfield_not_complete
plain-language theorem explainer
Every countable subfield of the reals fails the least-upper-bound property: some nonempty, K-bounded subset of K has no least upper bound inside K. Anyone arguing that Recognition carriers (φ-ladder, cost-closed fields, δ-dynamics) cannot be order-complete cites this. The proof reduces to the proper-subfield incompleteness lemma by using uncountability of ℝ to force properness from countability.
Claim. Let $K \subseteq \mathbb{R}$ be a subfield whose underlying set is countable. Then there exists a nonempty set $S \subseteq K$ that is bounded above by some element of $K$, yet no element of $K$ is a least upper bound of $S$ relative to $K$ (i.e., $K$ is not order-complete).
background
The module separates order-completeness of subfields of $\mathbb{R}$ from the cost axioms of Primitive Recognition Calculus. Completeness here means: every nonempty subset of $K$ that is bounded above in $K$ has a least upper bound that still lies in $K$.
The relativized supremum predicate records exactly that: $s$ is in $K$, bounds $S$, and is $\le$ every upper bound of $S$ that also lies in $K$. The sibling result on proper subfields states that any $K \neq \mathbb{R}$ fails this property, because every subfield contains $\mathbb{Q}$, density supplies cuts around any missing real, and no candidate in $K$ can be least.
Countability is the bridge from that properness lemma to concrete RS carriers: $\mathbb{R}$ is uncountable, so any countable subfield is automatically proper.
proof idea
One-step reduction to the proper-subfield incompleteness lemma. Apply that lemma to $K$, discharging the hypothesis $K \neq \top$ (as a subfield of $\mathbb{R}$) by contradiction: if $K$ equalled $\mathbb{R}$ as sets, countability of $K$ would imply countability of $\mathbb{R}$, contradicting the standard cardinal fact that $\mathbb{R}$ is uncountable. The existential witness set $S$ is whatever the proper-subfield argument constructs (a Dedekind-style cut at a missing real).
why it matters
Feeds the sharp closing theorem that order-completeness is exactly the continuum: the universal quantifier over countable subfields is this result, paired with the classical LUB property of $\mathbb{R}$. Also specializes immediately to the countable cost-closed field $T$, proving $T$ is incomplete.
In the Recognition framework this seals an independence claim: cost laws, the $\varphi$-ladder, and $\delta$-carriers live in countable fields, so they never force order-completeness. Completeness is an extra axiom whose only model among subfields of $\mathbb{R}$ is the uncountable continuum itself. That keeps analytic completeness out of the forcing chain (T0–T8) and out of the Recognition Composition Law; those constrain $J$ and $\varphi$, not Dedekind completeness of the carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.