classify_completion
plain-language theorem explainer
Every nonempty upper-bounded subset of the reals has a least upper bound. The ObjecthoodRegistry cites this to register continuum completeness as a distinct objecthood class in Primitive Recognition Calculus. The proof is a one-line wrapper around Mathlib's Real.exists_isLUB after unpacking the bound witness.
Claim. For every nonempty set $S \subseteq \mathbb{R}$, if there exists $b \in \mathbb{R}$ such that $x \le b$ for all $x \in S$, then there exists $s \in \mathbb{R}$ that is a least upper bound of $S$.
background
In Primitive Recognition Calculus, objecthood is stratified by how a real quantity is forced: by discrete cost structure, by scale, by display convention, by quotient, or by continuum completion. The ObjecthoodRegistry records each stratum as a named classification theorem.
Completion means the least-upper-bound property of $\mathbb{R}$. The module doc points to the companion fact that no countable cost-closed carrier has this property, so completeness is an independent continuum-side axiom (PRCCompletenessIndependence.completeness_is_exactly_the_continuum). Upstream cost and scale definitions (J-cost on recognition events, phi-powers as rung scales, stage chain $S_n$ of subfields) supply the discrete side against which this continuum axiom is contrasted.
Notation: IsLUB S s is the standard Mathlib predicate that $s$ is a least upper bound of $S$.
proof idea
Term-mode wrapper. Introduce the set $S$, nonempty hypothesis, and bounded-above witness. Unpack the existential bound $b$ with obtain. Feed Mathlib's Real.exists_isLUB the nonempty proof and the bundled upper-bound package ⟨b, fun x hx => hb x hx⟩. No Recognition-specific lemmas are required; the content is pure real analysis.
why it matters
Registers continuum completeness inside the objecthood periodic table of PRC. Sibling classifiers cover forced rationals, forced scale, display, convention, quotient, observable, and permitted strata; this entry isolates the LUB axiom as the continuum contribution.
The doc-comment ties the result to independence: countable cost-closed carriers never force completeness, so the continuum is not generated by discrete recognition cost alone. That separation matters for later claims that gauge units and free reals sit outside the forced discrete ladder (phi-rungs, eight-tick structure, J-cost). No downstream users are recorded yet; the theorem is registry infrastructure rather than a computational lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.