Foundation Primitive Recognition Calculus Real Completion

The real boundary

The real numbers are the continuum we use for lengths, times, and most of physics. A ledger, a discrete record of events, works with whole counts and rational fractions. The question is how a system built from counting ever gets to the smooth real line. The answer in Recognition Science is a bridge: a map that embeds each rational number from the ledger into the real numbers, preserving addition, multiplication, negation, and inversion.

The framework's library, a machine-checked collection of formal theorems, proves these preservation properties directly. The map respects the arithmetic: adding two ledger numbers and then converting gives the same real number as converting each and adding. The same holds for multiplication, negation, and reciprocal. This means the discrete arithmetic is genuinely compatible with the continuous one, not just approximately aligned.

The real numbers are complete: every Cauchy sequence converges to a limit within the line. The library shows the embedded ledger inherits this completeness through the standard real structure. So the ledger gains access to limits, continuity, and the rest of real analysis, but only by stepping onto a structure that already exists.

In Recognition Science, this step is called the real-completion boundary. The framework's own audit record tags it as a classical extension, meaning it uses the standard real numbers rather than building a new completion from scratch inside the ledger. The certificate that records this boundary states plainly that the embedding exists, preserves the four arithmetic operations, and uses classical completeness. It is an honest label: the bridge is available, but it is a chosen extension, not a forced consequence of the counting rules.

The practical effect is that the framework can now talk about continuous quantities when it needs to, while the discrete ledger remains its native ground. The real line is a tool the ledger can use, not a replacement for it. This matters because later framework results about constants and scaling live in the continuous setting, and this boundary is the point where that setting becomes available.

@[simp] theorem ofRat_add (a b : PRCRat) :
    ofRat (a + b) = ofRat a + ofRat b := by
  unfold ofRat
  rw [PRCRat.toRat_add']
  norm_num

@[simp] theorem ofRat_mul (a b : PRCRat) :
    ofRat (a * b) = ofRat a * ofRat b := by
  unfold ofRat
  rw [PRCRat.toRat_mul']
  norm_num

@[simp] theorem ofRat_neg (a : PRCRat) :
    ofRat (-a) = -ofRat a := by
  unfold ofRat
  rw [PRCRat.toRat_neg']
  norm_num

@[simp] theorem ofRat_inv (a : PRCRat) :
    ofRat (a⁻¹) = (ofRat a)⁻¹ := by
  unfold ofRat
  rw [PRCRat.toRat_inv']
  norm_num

/-- K4.14. The real boundary carries Lean's complete-space structure. -/
theorem complete_space : CompleteSpace PRCRealBoundary := by
  infer_instance

/-- K1/K4.14. Audit record: the real-completion boundary is a classical
extension until an internal PRC Cauchy quotient is built. -/
def realCompletionClaim : StrengthClaim where
  label := "K4.14_real_completion_boundary"
  tag := StrengthTag.classicalExtension
  statement := "The first PRC real boundary embeds PRCRat into Lean Real and uses classical completeness."

/-- K4.14. The classical real boundary is available and tagged honestly. -/
theorem real_completion_boundary_certificate :
    RealCompletionBoundaryCertificate where
  real_boundary_exists := ⟨0⟩
  rational_embedding_exists := ⟨PRCRealBoundary.ofRat⟩
  preserves_add := PRCRealBoundary.ofRat_add
  preserves_mul := PRCRealBoundary.ofRat_mul
  complete := PRCRealBoundary.complete_space
  strength_tag := rfl

What this page does not claim

The real numbers are not derived from the ledger's counting rules; they are imported as a classical extension. The embedding does not prove that the ledger itself is complete, only that its rationals sit inside a complete structure. No claim is made about how the real line relates to the forcing chain that produces constants and dimensions.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompletion.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: