logL
plain-language theorem explainer
Natural logarithm on the recovered real line is defined by transporting the standard logarithm through the equivalence maps to and from Mathlib reals. Researchers working on analytic identities over the logic-derived reals cite this construction when reducing to established real analysis. The definition is a direct one-line transport enabling inverse relations with the exponential.
Claim. For a recovered real $x$ in the logic-derived line, the natural logarithm is defined by transporting the standard logarithm: $x$ maps to the Mathlib real via the canonical extraction, the logarithm is taken there, and the result is injected back via the embedding map.
background
LogicReal wraps the Bourbaki completion of recovered rationals, realized as the Cauchy completion of ℚ with the equivalence LogicRat ≃ ℚ; the wrapper avoids polluting global instances on Completion ℚ while reusing Mathlib's completed reals. The toReal map extracts the Mathlib real via CompareReals.compareEquiv, and fromReal injects a Mathlib real back by applying the symmetric equivalence. The module LogicRealTranscendentals transports standard transcendental functions across this equivalence so analytic identities reduce directly to Mathlib's real-analysis library.
proof idea
one-line wrapper that applies fromReal to Real.log composed with toReal on the input.
why it matters
Supplies the logarithm operation required to establish the mutual inverses with the exponential in the same module. This transport layer supports analytic machinery needed for the J-uniqueness fixed point and phi-ladder constructions in the forcing chain. Downstream results expL_logL and logL_expL rely on it to recover the standard inverse properties after transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.