Foundation Primitive Recognition Calculus Real Completion Real Completion Claim

The real boundary

The real numbers are the standard arena for calculus: a number line with no gaps, where every Cauchy sequence converges to a limit. The framework's primitive recognition calculus works with recognition tokens, discrete records of events, whose arithmetic is rational. The declaration realCompletionClaim records the first bridge between those two worlds: it embeds the rational tokens into the real line and notes that the embedding preserves addition, multiplication, negation, and inverses.

The embedding is a function that sends each rational token to its ordinary real-number value. The machine-checked library proves that this map respects the arithmetic operations: adding two tokens and then embedding gives the same real number as embedding each and adding the results, and the same holds for multiplication, negation, and inversion. The declaration also notes that the real line, as the target of this embedding, carries the complete-space structure: every Cauchy sequence of real numbers converges to a real limit.

In Recognition Science, the declaration is tagged as a classical extension, not as an internal derivation. The real line is imported from the ambient mathematical environment rather than built from recognition tokens by the framework's own Cauchy-quotient construction. The certificate records this honestly: it states that the real boundary exists, that the rational embedding exists and preserves arithmetic, that the space is complete, and that the strength tag is the classical-extension tag.

The practical consequence is a working interface. Framework computations that need real-valued limits can use the standard real line through this embedding, while the framework's own ledger stays discrete. The declaration does not claim that the real numbers are derived from recognition; it claims only that the rational tokens sit inside the real line in a way that respects their arithmetic, and it labels that step as an external classical resource.

@[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 recognition tokens by the framework's own construction. The embedding does not claim that the real line is the unique completion of the rational tokens. The declaration does not assert that the real boundary is needed for any specific framework theorem.

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: