RealCompletionBoundaryCertificate
plain-language theorem explainer
Bundled Prop certificate that the classical real line is available as a PRC real boundary: nonempty, with a ring-homomorphic embedding of PRC rationals, metric completeness, and an honest classical-extension strength tag. Kernel first-pass audits and the companion existence theorem cite it. Pure structure definition; six fields, no proof body.
Claim. A real-completion boundary certificate is the conjunction of: the classical real line $\mathbb{R}$ is nonempty as a PRC real boundary; there exists a map from PRC rationals into that boundary; the map preserves addition and multiplication; the boundary is a complete space; and the associated claim is tagged as a classical extension (not a constructive PRC derivation).
background
Primitive Recognition Calculus (PRC) builds number carriers in stages. PRC rationals are ratio-orbit quotient classes (nonzero-denominator pairs identified by cross-multiplication). Earlier modules supply internal Cauchy ledgers and null-distance quotients; those stay inside the constructive PRC stack.
This module opens a different door. The real boundary is defined as Lean's ordinary complete real line $\mathbb{R}$, reached only under an explicit classical-extension strength tag. The embedding of a PRC rational is the conservative display map sending the quotient class to its underlying $\mathbb{Q}$ value, then coercing to $\mathbb{R}$.
The certificate packages existence of that boundary, existence of the embedding, the two ring laws for the embedding, completeness of the boundary, and the strength-tag equality that records the classical status of the step (K4.14).
proof idea
No proof body: this is a structure whose type is Prop. Each field is a named hypothesis the companion theorem must supply. Downstream, real_completion_boundary_certificate fills them by inhabiting $\mathbb{R}$ with $0$, taking the ofRat embedding, quoting the ofRat add/mul lemmas, invoking completeness of $\mathbb{R}$, and checking the classical-extension tag on realCompletionClaim.
why it matters
K4.14 is the first honest handoff from PRC carriers to classical analysis. The companion theorem witnesses the certificate; KernelFirstPassCertificate consumes it as part of the first-pass kernel audit ("concrete Lean objects for each stage in the first theorem chain").
In the Recognition stack this is not a forcing step like T5–T8. It is infrastructure: once the classical boundary is certified, later analytic claims (limits, completeness arguments, continuum-level mass or cost statements) may cite $\mathbb{R}$ without pretending the reals were derived from the Recognition Composition Law. The strength tag is the audit point that keeps that distinction sharp.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.