IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompletion
Module K4.14 records the first real boundary in Primitive Recognition Calculus: Lean's complete ordered field $\mathbb{R}$, reached only under an explicit classical-extension tag. It packages the rational embedding, its field homomorphisms, completeness, and a boundary certificate. Downstream Kernel imports this as the real substrate for later PRC constructions. The content is mostly structure and certificates rather than deep new proofs.
claimUnder a classical-extension tag, the PRC real boundary is Lean's complete real line $\mathbb{R}$, with a field embedding $\mathrm{ofRat}:\mathbb{Q}\to\mathbb{R}$ preserving $+$, $\cdot$, negation and inversion, together with a completeness claim and a named boundary certificate that this is the first real completion step in the calculus.
background
Primitive Recognition Calculus builds arithmetic substrates in stages. Prior modules supply the integer/rational layer (IntegerRational) and strength/tag machinery (Strength) that mark when a construction leaves the constructive core. This module is the next rung: the passage from $\mathbb{Q}$ to a complete ordered field.
The local objects are a real-boundary marker, a rational embedding ofRat with lemmas that it preserves addition, multiplication, negation and inversion, a completeness assertion for the ambient real space, and a packaged claim/certificate pair (realCompletionClaim, RealCompletionBoundaryCertificate). The doc-comment frames the whole file as K4.14: the first real boundary, available only under the classical-extension tag.
Notation is standard Mathlib $\mathbb{R}$ and $\mathbb{Q}$; the Recognition-specific content is the boundary tagging and the certificate that this completion is an explicit, named step rather than an implicit ambient assumption.
proof idea
Definition-and-certificate module, not a single deep theorem. It introduces the real-boundary marker, defines the rational embedding into Lean's $\mathbb{R}$, and records the standard field-homomorphism identities (add, mul, neg, inv) as short algebraic lemmas. Completeness is taken from the ambient complete space structure on $\mathbb{R}$. The claim and boundary-certificate declarations package those facts under the classical-extension tag so downstream code can depend on a single named K4.14 object rather than ad hoc real axioms.
why it matters in Recognition Science
In the Recognition foundation stack, physics and measurement eventually need a complete scalar field. This module is the first place PRC openly crosses that line, and it does so with an explicit classical tag so the constructive/rational core stays auditable. The Kernel module imports it, so later PRC kernel constructions sit on a certified real substrate rather than an unnamed Mathlib ambient.
Within the broader forcing and recognition story, this is infrastructure rather than a T5–T8 landmark: it does not force $J$, $\varphi$, the eight-tick octave, or $D=3$. It does make those later analytic statements speakable inside Lean by fixing what "real" means at the PRC boundary and by giving Kernel a single import edge for that choice.
scope and limits
- Does not construct a custom Cauchy completion; uses Lean's existing $\mathbb{R}$.
- Does not remove the classical-extension tag or claim a fully constructive real line.
- Does not prove uniqueness of completions up to unique isomorphism beyond the certificate packaging.
- Does not derive physical constants, $J$-uniqueness, $\varphi$, or dimensional forcing.
- Does not itself define the PRC Kernel; it only supplies the real boundary Kernel imports.