bourbaki_complete
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.