bourbaki_complete
The Bourbaki completion of the logic-recovered rationals forms a complete uniform space. Researchers recovering classical analysis inside the Recognition Science foundation layer cite this to treat LogicReal as a complete ordered field. The proof rewrites the target to the standard completion of the rationals and invokes the ambient Mathlib completeness instance.
claimThe Bourbaki real numbers, defined as the uniform completion of the logic rationals, constitute a complete space: $CompleteSpace(Bourbakiℝ)$.
background
The module recovers the reals from the Law-of-Logic rational layer. LogicRat is equivalent to the standard rationals ℚ, after which LogicReal wraps Mathlib's Bourbaki completion of ℚ, written CompareReals.Bourbakiℝ. Algebra and order on LogicReal are obtained by transport along the canonical equivalence toReal, so every downstream statement reduces to a classical real theorem.
proof idea
The proof is a term-mode one-liner. It applies change to rewrite the goal as CompleteSpace(Completion CompareReals.Q), then uses infer_instance to obtain the result from Mathlib's built-in fact that the completion of any uniform space is complete.
why it matters in Recognition Science
The declaration completes the formal recovery of the reals in the foundation layer. It guarantees that LogicReal inherits completeness, enabling reduction of analysis statements to classical results via the transport API. The result sits at the end of the chain LogicNat ⊢ LogicInt ⊢ LogicRat ≃ ℚ ⊢ Completion ℚ ≃ ℝ and supplies the missing completeness step for any later work on limits or continuity inside the recovered reals.
scope and limits
- Does not construct the reals without Mathlib's uniform-space completion.
- Does not prove the equivalence toReal without the sibling theorems.
- Does not supply explicit Cauchy sequences or metrics beyond the inherited structure.
- Does not address non-Archimedean or alternative real constructions.
formal statement (Lean)
208theorem bourbaki_complete : CompleteSpace CompareReals.Bourbakiℝ := by
proof body
Term-mode proof.
209 change CompleteSpace (Completion CompareReals.Q)
210 infer_instance
211
212/-- Every recovered real is represented by a Mathlib real and vice versa. -/