completeness_is_exactly_the_continuum
plain-language theorem explainer
Order-completeness is exactly what the continuum contributes: no countable subfield of the reals has the least-upper-bound property, while the reals do. Anyone separating Recognition carriers (δ-results living in countable fields) from Dedekind completeness will cite this. The proof is a one-line pairing of the countable-subfield incompleteness lemma with the standard LUB theorem for ℝ.
Claim. Every countable subfield $K \subseteq \mathbb{R}$ admits a nonempty set $S \subseteq K$ that is bounded above in $K$ yet has no least upper bound inside $K$; and every nonempty bounded-above subset of $\mathbb{R}$ has a least upper bound in $\mathbb{R}$.
background
The local setting is Primitive Recognition Calculus completeness-independence: whether order-completeness of the carrier can be forced by the cost/field axioms, or is an extra continuum axiom. The relativized supremum predicate used here says $s$ is a least upper bound of $S$ lying in a subfield $K$: $s \in K$, $s$ bounds $S$, and $s$ is $\le$ every upper bound that also lies in $K$. That is the notion order-completeness of $K$ would always supply.
Upstream, every countable subfield of $\mathbb{R}$ is proper (since $\mathbb{R}$ is uncountable), and every proper subfield fails the LUB property by a density-of-$\mathbb{Q}$ cut argument: for $r \notin K$, the cut ${x \in K : x < r}$ is nonempty and $K$-bounded above, yet no element of $K$ is its LUB. Separately, $\mathbb{R}$ itself has the classical LUB property. Recognition $\delta$-results place carriers in countable fields (constants, the $\varphi$-ladder, cost dynamics), so those carriers sit on the incomplete side of this dichotomy.
proof idea
Term-mode pairing: the theorem is the ordered pair of the two upstream results. The left conjunct is exactly countable_subfield_not_complete (countability implies properness, properness implies a missing internal LUB). The right conjunct is exactly real_has_lub (Mathlib's Real.exists_isLUB applied to a nonempty bounded-above set). No further rewriting.
why it matters
This is the sharp final form of the completeness-independence thread in Primitive Recognition Calculus. It pins that order-completeness is not a consequence of the cost axioms or of living in a field of characteristic zero: it is precisely the uncountable continuum. Downstream it is consumed by the objecthood registry's display classification, which treats $\mathbb{R}$ as the forgetful display of the $\mathbb{R}_\delta$ protocol interface (surjective value map, observational equality = equal value). In the broader Recognition framework, every $\delta$ carrier is countable, so none is order-complete; completeness remains an independent axiom whose only model among subfields of $\mathbb{R}$ is uncountable. That separation keeps the forcing chain (T0–T8) and the cost laws from smuggling continuum structure into the discrete ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.