real_completion_boundary_certificate
plain-language theorem explainer
K4.14 certificate that the classical real boundary is inhabited in the Primitive Recognition Calculus: rationals embed into it by a map preserving addition and multiplication, and the carrier is a complete space. The first-pass kernel certificate cites this as its real-completion boundary witness. The proof is a pure term packing preexisting ofRat morphisms, their add/mul lemmas, and Lean's CompleteSpace instance.
Claim. The real-completion boundary certificate holds: the classical real boundary carrier is nonempty; there is an embedding of the PRC rationals into that carrier; the embedding preserves addition and multiplication; and the carrier carries a complete-space structure.
background
In the Primitive Recognition Calculus real-completion layer, the classical real boundary is the ordinary real line used as a display carrier for completed ledgers. The embedding ofRat sends a PRC rational $q$ to its ordinary rational image in $\mathbb{R}$ via the conservative display $q \mapsto (q.\mathrm{toRat}:\mathbb{R})$. Sibling lemmas record that this map is a ring homomorphism on the nose: it preserves addition and multiplication by rewriting through the corresponding toRat identities and a short norm_num cleanup.
Completeness is not rebuilt from Cauchy sequences here. The module already exposes complete_space, which simply reuses Lean's CompleteSpace instance on the boundary carrier ("The real boundary carries Lean's complete-space structure"). Upstream constant-protocol and Cauchy-ledger embeddings (ofRat in DeltaReal, RealCauchy, and the null-distance quotient) supply the broader story of how rationals sit inside various PRC real presentations; this certificate only needs the classical boundary face.
Local setting (module RealCompletion): audit record K4.14/A5 that the real-completion boundary is available classically and tagged honestly, rather than reconstructed from first principles inside the kernel.
proof idea
Term-mode structure inhabitant. Nonemptiness of the boundary is witnessed by the zero real. The rational embedding field is the existing ofRat map packaged as a nonempty function type. Additivity and multiplicativity are the simp lemmas ofRat_add and ofRat_mul (unfold ofRat, rewrite the corresponding toRat identity, finish by norm_num). Completeness is the already-proved complete_space theorem, itself a one-line infer_instance. The strength tag is discharged by rfl. No new analysis is performed; the certificate only assembles prior facts into the K4.14 Prop bundle.
why it matters
This is the K4.14 first real-completion boundary certificate. Downstream, kernel_first_pass_certificate (K7/A2) consumes the broader first-pass kernel surface; the real boundary is the classical completion face that kernel audit expects to be present and honestly tagged. In the Recognition foundation stack it marks the point where PRC stops insisting on internal Cauchy ledgers alone and admits the ordinary complete ordered field as a display boundary, while still recording the embedding and homomorphism laws that keep rational arithmetic coherent.
It does not itself force $\phi$, the eight-tick octave, or $D=3$ (those live in the T0–T8 forcing chain). Its job is narrower: close the classical-real slot so later kernel and strength certificates can cite a single inhabited Prop rather than re-proving embedding and completeness at each use site. The "tagged honestly" clause in the doc-comment is the audit stance: the boundary is classical Lean $\mathbb{R}$, not a new constructive real type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.