toReal_logL
The theorem asserts that the transported natural logarithm on the recovered real line commutes with the map to standard reals. It is cited by the inverse-pair theorems for the transported exponential and logarithm. The proof is a one-line wrapper that invokes the general transport identity toReal_fromReal after the definition of logL inserts fromReal around the standard logarithm.
claimFor any recovered real $x$, the transport of the natural logarithm of $x$ equals the standard natural logarithm of the transport of $x$, where the logarithm on recovered reals is obtained by transporting the standard logarithm through the equivalence between the recovered line and Mathlib's real line.
background
The module defines transcendental functions on LogicReal by transport through its equivalence to Mathlib's ℝ. LogicReal is the structure wrapping the Bourbaki completion of the recovered rationals, with toReal sending an element to its image under the canonical equivalence. The logarithm is introduced by the definition logL x := fromReal (Real.log (toReal x)). The upstream lemma toReal_fromReal states that toReal (fromReal x) = x for any standard real x, providing the exact cancellation needed for transport lemmas.
proof idea
The proof is a one-line wrapper that applies the lemma toReal_fromReal. Unfolding the definition of logL replaces the left-hand side with toReal (fromReal (Real.log (toReal x))), after which toReal_fromReal directly yields Real.log (toReal x).
why it matters in Recognition Science
This result feeds the inverse theorems expL_logL and logL_expL, which establish that the transported exponential and logarithm satisfy the expected functional equations on the recovered reals. It thereby allows analytic identities to reduce to Mathlib's library while the rest of the Recognition framework works over LogicReal. The module documentation notes that this transport layer is the correct first step before higher constructions that rely on the recovered real line.
scope and limits
- Does not address branch cuts or complex logarithms.
- Does not prove continuity, differentiability, or other analytic properties of the transported logarithm.
- Applies only under the specific equivalence between LogicReal and the standard reals.
formal statement (Lean)
60@[simp] theorem toReal_logL (x : LogicReal) :
61 toReal (logL x) = Real.log (toReal x) :=
proof body
One-line wrapper that applies toReal_fromReal.
62 toReal_fromReal _
63