real_has_lub
plain-language theorem explainer
The real line has the least-upper-bound property: every nonempty set of reals that is bounded above admits a least upper bound. Anyone separating order-completeness from the Recognition cost axioms cites this as the positive half of the comparison with countable cost-closed subfields. The proof unpacks the bound witness and applies Mathlib's existence theorem for least upper bounds on ℝ.
Claim. For every nonempty set $S \subseteq \mathbb{R}$ that is bounded above, there exists $s \in \mathbb{R}$ that is a least upper bound of $S$.
background
The module on completeness independence separates order-completeness of the continuum from the Recognition Science cost and field axioms. The canonical recognition cost is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), the unique solution forced by the Recognition Composition Law. Cost-closed subfields of $\mathbb{R}$ model those axioms; the $\phi$-ladder, constants, and cost dynamics all live in countable carriers.
A least upper bound of $S$ is an upper bound of $S$ that is $\le$ every other upper bound. A sibling predicate relativizes the same notion to a subfield carrier. The present theorem is the absolute statement on $\mathbb{R}$ itself, the standard continuum model against which countable $J$-closed subfields are compared.
Local setting: order-completeness holds in one cost-closed subfield ($\mathbb{R}$) and fails in another (a countable $J$-closed field $T$), so it is not entailed by being a $J$-closed field.
proof idea
Unpack the existential upper-bound hypothesis to a concrete bound $b$ together with the proof that every element of $S$ is $\le b$. Package that witness as a Mathlib upper-bound structure and apply Real.exists_isLUB to the nonempty hypothesis and that structure. The result is pure real analysis: a thin term-mode bridge to the standard LUB theorem on $\mathbb{R}$, with no Recognition-specific algebra.
why it matters
This is the positive arm of the sharp claim that order-completeness is exactly what the continuum adds. Downstream, the theorem that completeness is exactly the continuum pairs it with the fact that no countable subfield of $\mathbb{R}$ is order-complete: every $\delta$-result places its carrier in a countable field, so that carrier is never order-complete. The independence theorems (completeness not forced by cost axioms; completeness not forced by genuine cost laws) use the same contrast: a countable field $T$ closed under $J$ fails LUB while $\mathbb{R}$ has it, so continuous completion is a strictly stronger, independent commitment, not a $\delta$-consequence. In the forcing chain this sits outside T0–T8: completeness is not derived from J-uniqueness, $\phi$, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.