IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompletion

   1/-
   2  PrimitiveRecognitionCalculus/RealCompletion.lean
   3
   4  Round-trip source:
   5    PRC_Kernel_Spec_20260526.html
   6
   7  Spec anchors:
   8    K1 (`classical extension`), K4.14, A5
   9
  10  This is the honest real-completion boundary. It embeds the quotient-native
  11  PRC rational surface into Lean's `ℝ` and records completeness as a
  12  classical-extension fact. It is not a claim that the PRC-internal Cauchy
  13  quotient has already been built.
  14-/
  15
  16import Mathlib
  17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
  18import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Strength
  19
  20namespace IndisputableMonolith
  21namespace Foundation
  22namespace PrimitiveRecognitionCalculus
  23
  24/-- K4.14. The first real boundary: Lean's complete real line, reached only
  25under the classical-extension tag. -/
  26abbrev PRCRealBoundary : Type := ℝ
  27
  28namespace PRCRealBoundary
  29
  30/-- K4.14/A5. Embed a PRC rational into the real boundary through its
  31conservative rational display. -/
  32def ofRat (q : PRCRat) : PRCRealBoundary :=
  33  (q.toRat : ℝ)
  34
  35@[simp] theorem ofRat_add (a b : PRCRat) :
  36    ofRat (a + b) = ofRat a + ofRat b := by
  37  unfold ofRat
  38  rw [PRCRat.toRat_add']
  39  norm_num
  40
  41@[simp] theorem ofRat_mul (a b : PRCRat) :
  42    ofRat (a * b) = ofRat a * ofRat b := by
  43  unfold ofRat
  44  rw [PRCRat.toRat_mul']
  45  norm_num
  46
  47@[simp] theorem ofRat_neg (a : PRCRat) :
  48    ofRat (-a) = -ofRat a := by
  49  unfold ofRat
  50  rw [PRCRat.toRat_neg']
  51  norm_num
  52
  53@[simp] theorem ofRat_inv (a : PRCRat) :
  54    ofRat (a⁻¹) = (ofRat a)⁻¹ := by
  55  unfold ofRat
  56  rw [PRCRat.toRat_inv']
  57  norm_num
  58
  59/-- K4.14. The real boundary carries Lean's complete-space structure. -/
  60theorem complete_space : CompleteSpace PRCRealBoundary := by
  61  infer_instance
  62
  63end PRCRealBoundary
  64
  65/-- K1/K4.14. Audit record: the real-completion boundary is a classical
  66extension until an internal PRC Cauchy quotient is built. -/
  67def realCompletionClaim : StrengthClaim where
  68  label := "K4.14_real_completion_boundary"
  69  tag := StrengthTag.classicalExtension
  70  statement := "The first PRC real boundary embeds PRCRat into Lean Real and uses classical completeness."
  71
  72/-- K4.14. First real-completion boundary certificate. -/
  73structure RealCompletionBoundaryCertificate : Prop where
  74  real_boundary_exists : Nonempty PRCRealBoundary
  75  rational_embedding_exists : Nonempty (PRCRat → PRCRealBoundary)
  76  preserves_add : ∀ a b : PRCRat,
  77    PRCRealBoundary.ofRat (a + b) =
  78      PRCRealBoundary.ofRat a + PRCRealBoundary.ofRat b
  79  preserves_mul : ∀ a b : PRCRat,
  80    PRCRealBoundary.ofRat (a * b) =
  81      PRCRealBoundary.ofRat a * PRCRealBoundary.ofRat b
  82  complete : CompleteSpace PRCRealBoundary
  83  strength_tag : realCompletionClaim.tag = StrengthTag.classicalExtension
  84
  85/-- K4.14. The classical real boundary is available and tagged honestly. -/
  86theorem real_completion_boundary_certificate :
  87    RealCompletionBoundaryCertificate where
  88  real_boundary_exists := ⟨0⟩
  89  rational_embedding_exists := ⟨PRCRealBoundary.ofRat⟩
  90  preserves_add := PRCRealBoundary.ofRat_add
  91  preserves_mul := PRCRealBoundary.ofRat_mul
  92  complete := PRCRealBoundary.complete_space
  93  strength_tag := rfl
  94
  95end PrimitiveRecognitionCalculus
  96end Foundation
  97end IndisputableMonolith
  98