logL_expL
The theorem establishes that the transported natural logarithm and exponential on LogicReal are mutual inverses. Researchers recovering analytic structure from logic in Recognition Science cite this when reducing identities to Mathlib's real line. The proof is a one-line wrapper that rewrites via the transport equivalence and invokes the standard Real.log_exp identity.
claimFor every recovered real number $x$, the transported logarithm satisfies $log_L(exp_L(x)) = x$, where $exp_L$ and $log_L$ are obtained by transporting the standard exponential and natural logarithm through the equivalence between LogicReal and the Mathlib real line.
background
LogicReal is the structure realizing the Cauchy completion of recovered rationals, with canonical transport maps toReal and fromReal that realize the equivalence to Mathlib's ℝ. The functions expL and logL are defined by transport: expL x := fromReal (Real.exp (toReal x)) and logL x := fromReal (Real.log (toReal x)). The upstream theorem eq_iff_toReal_eq states that equality on LogicReal is exactly equality after transport to the standard reals, which is the key reduction tool for all transport lemmas in this module.
proof idea
The proof rewrites the target equality using eq_iff_toReal_eq, then applies the simp theorems toReal_logL and toReal_expL to reduce the statement to Real.log (Real.exp (toReal x)) = toReal x. The final step invokes the Mathlib lemma Real.log_exp directly.
why it matters in Recognition Science
This result supplies the inverse relation for the core pair of transported transcendental functions, completing the basic analytic toolkit on LogicReal. It directly supports the module's goal of allowing later code to reason over the recovered reals while reducing all identities to Mathlib's established library. No downstream uses are recorded yet, but the lemma is a prerequisite for any further transport of hyperbolic or trigonometric identities.
scope and limits
- Does not prove inverse relations for other transported functions such as sine or power.
- Does not address differentiability, continuity, or series expansions of the transported functions.
- Does not extend the result beyond the real line to complex or p-adic settings.
- Does not supply numerical evaluation or approximation algorithms.
formal statement (Lean)
105theorem logL_expL (x : LogicReal) : logL (expL x) = x := by
proof body
Term-mode proof.
106 rw [eq_iff_toReal_eq, toReal_logL, toReal_expL]
107 exact Real.log_exp _
108
109/-- Transported hyperbolic cosine definition. -/