PRCRealBoundary

Primitive Recognition Calculus (PRC) builds arithmetic from discrete recognition data before any continuum is assumed. Integers and rationals appear first; the real line is not native. The module RealCompletion records the classical step that adjoins a complete ordered field as a boundary object.

K4.14 names that boundary and tags it as classical extension rather than a forced recognition primitive. The synonym simply points at Mathlib's $\mathbb{R}$. Downstream, rationals of type PRCRat embed by their conservative rational display (cast to $\mathbb{R}$), and the boundary inherits Lean's complete-space instance.

The surrounding certificate package asks only that the boundary be nonempty, that a rational embedding exist, and that addition and multiplication be preserved. No continuum is derived from the forcing chain T0–T8 here; the continuum is imported and labelled.

Definitional abbreviation: the type is definitionally equal to $\mathbb{R}$. No tactics, no lemmas, no construction. Completeness and the field operations are those already on Lean's reals; they are recovered later by infer_instance and by casting lemmas on the rational embedding.

This synonym is the carrier type for the K4.14 real-completion boundary. It is what complete_space equips with Lean's CompleteSpace structure, what ofRat targets when embedding PRC rationals, and what the structure RealCompletionBoundaryCertificate quantifies over (nonemptiness, embedding, add/mul preservation). The audit theorem real_completion_boundary_certificate packages those facts so the classical tag is explicit.

In the Recognition framework this is bookkeeping, not a forcing step: T5–T8 force J, phi, the eight-tick octave, and D=3 inside discrete recognition; the continuum remains an optional classical boundary. The declaration exists so later analytic layers can write against a named PRC boundary instead of bare $\mathbb{R}$, while the certificate keeps the classical-extension status honest.