IsLUBIn
plain-language theorem explainer
Relativized least-upper-bound: a real s is an LUB of S that lives inside a subfield K of R. Anyone proving that order-completeness is independent of the cost/field axioms cites this predicate. It is a pure three-conjunct definition (membership in K, upper bound, least among K-bounds).
Claim. For a subfield $K \subseteq \mathbb{R}$, a set $S \subseteq \mathbb{R}$, and $s \in \mathbb{R}$, write that $s$ is a least upper bound of $S$ in $K$ when $s \in K$, every $x \in S$ satisfies $x \le s$, and every $u \in K$ that bounds $S$ from above obeys $s \le u$.
background
The module separates order-completeness of the real line from the Primitive Recognition Calculus cost and field structure. Carriers arising from cost dynamics, the phi-ladder, and related constructions sit in countable subfields of $\mathbb{R}$; the question is whether the least-upper-bound property is forced by those axioms or is an independent continuum commitment.
Ordinary completeness says every nonempty set of reals that is bounded above has a supremum in $\mathbb{R}$. Here the ambient object is a subfield $K \subseteq \mathbb{R}$, so the supremum must be required to lie in $K$ and to be least only among upper bounds that also lie in $K$. That is the relativized LUB notion recorded by this definition.
Downstream theorems use it to state failure of completeness: a witness set $S \subseteq K$, nonempty and bounded above in $K$, for which no element of $K$ is an LUB of $S$ inside $K$.
proof idea
Definitional abbreviation, not a proved statement. The body is the conjunction of three propositions: $s$ belongs to the carrier of $K$; $s$ is an upper bound of $S$; and among all upper bounds of $S$ that lie in $K$, $s$ is least. No tactics or lemmas are applied.
why it matters
This is the atomic predicate for the module's independence theorems. subfield_not_complete shows every proper subfield of $\mathbb{R}$ admits a cut with no LUB inside the subfield; countable_subfield_not_complete specializes to countable carriers; T_not_complete applies the same failure to the countable cost-closed field $T$.
Those feed completeness_not_forced_by_cost_axioms and the upgraded completeness_not_forced_by_genuine_cost_laws (unit, reciprocal symmetry, nonnegativity of $J$, plus $J$-closure of $T$). The sharp form completeness_is_exactly_the_continuum packages the countable-failure half with the classical LUB property of $\mathbb{R}$: order-completeness is precisely what uncountability buys, not a consequence of the recognition cost laws. In the broader RS forcing picture this keeps continuum completeness off the T0-T8 chain and off the RCL/$J$-cost axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.