Foundation Primitive Recognition Calculus Real Completion Complete Space

The first real boundary

The real numbers are the standard setting for calculus: the line you can draw without gaps, where every convergent sequence has a limit. The Recognition Science framework, which builds its structures from a discrete ledger of recognition events, reaches this boundary only at a specific labeled step. Its declaration complete_space states that the framework's first real boundary, called PRCRealBoundary, is a complete space in the usual mathematical sense. This means that within this boundary, every Cauchy sequence, every sequence whose terms get arbitrarily close to one another, converges to a real number. The declaration is a theorem in the framework's machine-checked library of formal theorems, and its proof is a single line: the boundary is defined to be the real numbers, so completeness is inherited from them.

The boundary is not built from scratch. The framework first defines its own rational numbers, PRCRat, as a discrete structure. The declaration ofRat embeds these rationals into the real boundary by mapping each one to its standard real value. The framework then proves that this embedding respects the arithmetic operations: adding two rationals and then embedding gives the same result as embedding each and adding the results, and the same holds for multiplication, negation, and inverse. These preservation theorems are what make the embedding a genuine copy of the rationals inside the reals, not just a naming convention.

In Recognition Science, this step is marked as a classical extension, not a derivation from the framework's own principles. The framework's internal certificate, RealCompletionBoundaryCertificate, records this honestly: it bundles the existence of the boundary, the embedding, the preservation theorems, and the completeness property into one package, and labels the whole thing as classical. The framework's own path to a complete space, built from its internal Cauchy sequences, remains an open target. The declaration complete_space does not claim that the real numbers arise from the ledger; it claims only that the framework can use them, under a clearly marked external assumption.

What this changes is practical: the framework can now do analysis. Limits, continuity, and the tools of real calculus become available at this boundary. The step is small, a single import, but it is the first real boundary in a framework that otherwise works with discrete structures. It is a bridge, not a new land.

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

/-- K4.14/A5. Embed a PRC rational into the real boundary through its
conservative rational display. -/
def ofRat (q : PRCRat) : PRCRealBoundary :=
  (q.toRat : ℝ)

@[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

/-- 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."

What this page does not claim

The real numbers are not derived from the ledger; they are imported as a classical extension. The completeness property is not proved from framework-internal principles. The certificate does not claim that the real boundary is the framework's only possible complete space.

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: