equivReal
plain-language theorem explainer
EquivReal constructs the canonical equivalence between logic-recovered reals and Mathlib's standard reals. Researchers recovering analysis from the Law-of-Logic layer cite it to transport theorems without information loss. The definition is a one-line wrapper assembling the forward map toReal, the inverse fromReal, and the two round-trip identities already proved in the module.
Claim. The recovered real numbers form a type equivalent to the standard reals: there is a bijection between the Cauchy completion of the recovered rationals and $ℝ$ whose forward direction is the canonical transport map and whose inverse is the embedding of a standard real.
background
The module recovers the real numbers from the Law-of-Logic rational layer. It applies Mathlib's Bourbaki completion of $ℚ$ to the recovered rationals LogicRat, where LogicRat is already equivalent to $ℚ$. LogicReal wraps CompareReals.Bourbakiℝ to avoid global instance pollution while still reusing the completed real line.
proof idea
The definition is a one-line wrapper that sets the forward function to toReal, the inverse function to fromReal, and cites the theorems fromReal_toReal and toReal_fromReal to witness the left and right inverses.
why it matters
This equivalence closes the recovery step from LogicRat to the completed reals, allowing every subsequent theorem on LogicReal to reduce to a standard real theorem and be read back. It supplies the transport layer required for the recognition functional equation and the derivation of constants such as the fine-structure interval. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.