complete_space

In Primitive Recognition Calculus, the first real boundary is introduced only under a classical-extension tag. The abbreviation is definitionally Lean’s real line $\mathbb{R}$, not an internal PRC Cauchy quotient of rationals. The module’s audit note states that this boundary remains a classical extension until such a quotient is built.

Sibling structure embeds PRC rationals into this boundary via a conservative rational display, with lemmas that the embedding preserves addition, multiplication, negation, and inversion. Completeness is the metric property that every Cauchy sequence has a limit in the space; Mathlib already equips $\mathbb{R}$ with that instance.

K4.14 packages existence of the boundary, the rational embedding, and algebraic preservation into a single certificate. Completeness is the remaining structural fact that the boundary inherits from classical analysis.

One-line term proof: infer_instance. Because the real boundary is an abbreviation for $\mathbb{R}$, Lean finds Mathlib’s existing CompleteSpace \mathbb{R} instance and discharges the goal with no further lemmas or tactics.

Feeds real_completion_boundary_certificate (K4.14): that certificate records that the classical real boundary is available and tagged honestly, bundling existence, rational embedding, and ring operations. Completeness is the analytic half of calling the boundary “real” rather than merely a dense ordered field.

In the Recognition stack this is scaffolding honesty, not a derivation of continuum structure from the forcing chain (T0–T8). The module doc flags the open path: replace the classical tag by an internal PRC Cauchy quotient when that construction exists. Until then, downstream analysis that needs limits on the boundary may cite this instance, knowing the foundation is still classical.