subfield_not_complete
plain-language theorem explainer
Any proper subfield of the reals fails the least-upper-bound property: some nonempty subset of the subfield is bounded above inside it yet has no least upper bound in the subfield. Analysts and foundation workers cite this to separate algebraic field structure from order-completeness. The proof builds the Dedekind cut below a missing real and uses density of the rationals plus trichotomy on any candidate supremum.
Claim. Let $K \subseteq \mathbb{R}$ be a subfield with $K \neq \mathbb{R}$. 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., no $s \in K$ bounds $S$ from above and is $\le$ every upper bound of $S$ that lies in $K$).
background
The ambient setting is order-completeness for subfields of $\mathbb{R}$, in the Primitive Recognition Calculus completeness-independence module. Completeness here means every nonempty subset of $K$ that is bounded above in $K$ has a least upper bound still lying in $K$.
The relativized supremum predicate IsLUBIn packages that demand: $s$ lies in $K$, bounds $S$, and is $\le$ every other upper bound from $K$. Every subfield of $\mathbb{R}$ contains $\mathbb{Q}$, and $\mathbb{Q}$ is dense in $\mathbb{R}$. Density supplies rationals in every open interval, which is the only analytic input beyond the subfield axioms.
The theorem isolates properness ($K \neq \mathbb{R}$) as already enough to destroy the LUB property. Countability is not used here; it appears only in the immediate corollary that routes through uncountability of $\mathbb{R}$.
proof idea
From $K \neq \mathbb{R}$ pick $r \notin K$. Set $S = {x \in K : x < r}$.
Membership in $K$ is immediate. Nonemptiness: some rational $q < r$ lands in $K$ by the subfield's rational cast. An upper bound in $K$: some rational $q > r$ bounds every element of $S$.
No LUB in $K$: if $s$ were one, trichotomy on $s$ versus $r$ yields three contradictions. If $s < r$, a rational in $(s,r)$ sits in $S$ and exceeds $s$. If $s = r$, then $s \in K$, contradicting the choice of $r$. If $s > r$, a rational in $(r,s)$ is already an upper bound in $K$ strictly below $s$, so $s$ is not least.
why it matters
This is the properness half of the completeness-independence argument in PRC. The sole downstream consumer is countable_subfield_not_complete, whose doc-comment states the moral: "order-completeness and countability are flatly incompatible for subfields of $\mathbb{R}$: completeness is exactly what uncountability (the continuum) buys. Whatever countable carrier $\delta$ uses, it is never order-complete."
Sibling results in the same module (completeness_not_forced_by_cost_axioms, completeness_not_forced_by_genuine_cost_laws, completeness_is_exactly_the_continuum) use this separation to show that the Recognition cost axioms and genuine cost laws do not force the continuum. Completeness is an independent structural commitment, not a consequence of the J-cost or RCL layer (T5). The result therefore keeps the foundation honest: algebraic and cost structure live on countable carriers if desired; the continuum is an extra postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.