realCompletionClaim
plain-language theorem explainer
Audit record K4.14 tagging the first PRC real-completion boundary as a classical extension: PRC rationals embed into Lean Real and rely on classical completeness. Foundation auditors cite it when scoring how far the primitive recognition calculus has left the constructive core. The body is a pure StrengthClaim record (label, tag, statement), not a proved theorem.
Claim. Define the strength-audit claim with label $\mathrm{K4.14\_real\_completion\_boundary}$, strength tag classical extension, and statement that the first primitive-recognition-calculus real boundary embeds the PRC rationals into Lean $\mathbb{R}$ and uses classical completeness.
background
In the Primitive Recognition Calculus (PRC), rationals are built first as PRCRat: nonzero-denominator ratio-orbit quotient classes identified by cross-multiplication (K4.8). The real layer is the next completion step. This module records the first real-completion boundary: an embedding of those rationals into Lean's classical Real, together with the usual field operations and completeness.
StrengthClaim is a small audit structure (label, strength tag, human statement) used to classify how constructive or classical each PRC boundary is. The tag here is classical extension: the construction is accepted as a bridge into Mathlib reals until an internal PRC Cauchy quotient exists.
Upstream, the rational type and the strength taxonomy are already fixed; this declaration only packages the K4.14 audit line for the certificate that follows.
proof idea
No mathematical proof. The definition is a structure literal for StrengthClaim: set label to the K4.14 string, tag to StrengthTag.classicalExtension, and statement to the fixed English sentence about embedding PRCRat into Lean Real via classical completeness. One-line field assignments only.
why it matters
Feeds RealCompletionBoundaryCertificate, the K4.14 Prop that packages existence of a real boundary, a rational embedding, and preservation of addition (and related field laws on the boundary). In the Recognition foundation stack this marks where PRC leaves its integer/rational core and borrows classical completeness, matching the doc-comment note that the boundary stays a classical extension until an internal PRC Cauchy quotient is built.
Auditors use the strength tag to keep classical Mathlib Real out of the constructive forcing chain (T0–T8) until that internal completion exists. The claim does not itself force dimension, $\phi$, or the eight-tick octave; it only grades the real-completion step in the PRC ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.