Foundation Primitive Recognition Calculus Real Completion Real Completion Bounda

The first real boundary

The real numbers are the standard continuum used across mathematics and physics. They include every rational number, plus irrationals like the square root of 2 and pi, and they are complete: every Cauchy sequence of real numbers converges to a real number. This completeness is what makes calculus, limits, and continuous functions work. In the Recognition Science framework, the declaration real_completion_boundary_certificate establishes that this complete real line can serve as a boundary for the framework's primitive recognition calculus, but only under a clearly labeled condition.

The certificate is a machine-checked theorem in the framework's library of formal theorems. It proves four facts. First, the real boundary exists as a type. Second, every rational number from the framework's internal arithmetic embeds into this real boundary. Third, that embedding preserves addition and multiplication: adding two rationals in the internal system and then embedding gives the same result as embedding each one first and then adding in the reals. Fourth, the real boundary is complete, inheriting the standard completeness of the real line.

In Recognition Science, the framework's own numbers are rationals built from a discrete ledger of recognition events. The real boundary is not one of those internal constructions. It is an external classical extension, imported from the ambient type theory. The certificate's strength tag says so explicitly: it is a classical extension, not an internal derivation. The framework has not yet built its own Cauchy quotient of rationals to produce the reals from within. That internal construction remains open.

What the certificate does not claim is just as important as what it proves. It does not claim that the real numbers arise from the ledger. It does not claim that completeness is forced by the framework's own axioms. It merely records that the classical real line is available and that the embedding of rationals behaves correctly. The tag is an honesty device: it marks the boundary as borrowed, not earned.

For a reader, the payoff is a clear line between what the framework derives and what it imports. The real boundary is a bridge to classical analysis, usable for future work, but it carries a signpost saying the bridge was not built from framework materials. That signpost is the whole point of the certificate.

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

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

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

/-- 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 framework's internal ledger. The certificate does not claim that completeness is forced by the framework's own axioms. An internal Cauchy quotient of framework rationals has not been built.

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: