fromReal_toReal
plain-language theorem explainer
The round-trip identity shows that transporting a recovered real to the standard reals and back recovers the original element. Foundation-layer proofs in Recognition Science rely on this when reducing statements about LogicReal to theorems in Mathlib's reals. The argument applies case analysis to the wrapper structure and simplifies using the definitions of the two transport functions.
Claim. For every element $x$ of the recovered real line, the composition fromReal ∘ toReal applied to $x$ equals $x$.
background
LogicReal wraps Mathlib's Bourbaki completion of the rationals, obtained after recovering LogicRat from the law of logic. The map toReal extracts the underlying Mathlib real via the canonical equivalence, while fromReal embeds a standard real back into the wrapper. This construction appears in the module recovering the reals from the rational layer built on LogicNat and LogicInt. Upstream, the definitions of toReal and fromReal establish the transport, and the structure LogicReal prevents instance pollution on the completion.
proof idea
The proof performs case analysis on the constructor of LogicReal, exposing the underlying Bourbaki real, then applies simplification rules for toReal and fromReal to obtain the identity.
why it matters
This identity is the left inverse property required to define the equivalence equivReal between LogicReal and the standard reals. It is invoked in the complex-number recovery and in the equality-transfer lemma eq_iff_toReal_eq. Within the Recognition framework it closes the recovery step from the law-of-logic rationals to the completed reals, enabling all subsequent analysis to reduce to Mathlib theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.