toReal_fromReal
The round-trip theorem shows that embedding any classical real into the logic-recovered reals via fromReal and projecting back via toReal recovers the original value exactly. Researchers reducing statements about LogicReal to standard real analysis cite it as the key identity that justifies the transport API. The proof is a one-line simp wrapper that unfolds the two transport definitions and applies the underlying equivalence.
claimFor every real number $x$, the composition of the embedding from the standard reals into the Bourbaki completion of the recovered rationals followed by the canonical projection back equals $x$.
background
The module recovers the reals from the Law-of-Logic rational layer: LogicNat, LogicInt and LogicRat are constructed first, then LogicReal is obtained as the Bourbaki completion of LogicRat inside Mathlib's uniform-space framework. LogicReal wraps CompareReals.Bourbakiℝ; the map toReal applies the comparison equivalence to the wrapped value, while fromReal applies the inverse equivalence. This transport-first design lets every algebraic or order statement on LogicReal reduce to the corresponding statement on ℝ and be read back.
proof idea
One-line wrapper that applies simp to the definitions of toReal and fromReal. The tactic directly reduces the composition to the identity map on the underlying equivalence CompareReals.compareEquiv.
why it matters in Recognition Science
It closes the round-trip for the real transport and is invoked by twenty-one downstream results, including the complex round-trip toComplex_fromComplex and the transported transcendentals toReal_expL, toReal_coshL, toReal_logL and toReal_piL. The declaration supports the module's stated goal of allowing every downstream theorem to reduce to an existing real theorem before being transported back, thereby anchoring the Recognition Science phi-ladder and mass formulas in classical analysis.
scope and limits
- Does not establish algebraic or order properties of LogicReal beyond the round-trip identity.
- Does not construct or verify the LogicRat layer itself.
- Does not address completeness or uniform-space properties directly.
- Does not provide numerical evaluation or approximation results.
Lean usage
example (z : ℂ) : toComplex (fromComplex z) = z := by apply Complex.ext <;> simp [toReal_fromReal]formal statement (Lean)
79theorem toReal_fromReal (x : ℝ) : toReal (fromReal x) = x := by
proof body
One-line wrapper that applies simp.
80 simp [toReal, fromReal]
81