expL_logL
The theorem establishes that the transported exponential and logarithm on the recovered real line are inverses for positive arguments. Researchers carrying analytic identities across the LogicReal equivalence would cite this to justify reductions to Mathlib. The proof is a short tactic sequence that rewrites via equality transport, applies the toReal lemmas, transfers positivity, and invokes the standard Real.exp_log.
claimFor every positive $x$ in the recovered real line, the transported exponential satisfies $exp_L(log_L(x)) = x$, where $exp_L$ and $log_L$ are obtained by transporting the classical exponential and logarithm through the equivalence with Mathlib's reals.
background
The module defines transcendental functions on LogicReal by transport through the equivalence with Mathlib's ℝ. LogicReal is the structure wrapping the Bourbaki completion of the rationals, with toReal and fromReal providing the isomorphism. expL(x) is defined as fromReal(Real.exp(toReal x)) and logL(x) as fromReal(Real.log(toReal x)). Upstream results supply the transport theorems toReal_expL and toReal_logL, which state that toReal(expL x) equals Real.exp(toReal x) and likewise for logL, together with eq_iff_toReal_eq equating equality on LogicReal with equality after transport.
proof idea
The proof is a short tactic sequence. It rewrites the goal using eq_iff_toReal_eq to move to an equality on the classical reals. It then applies the simp lemmas toReal_expL and toReal_logL to reach Real.exp(Real.log(toReal x)) = toReal x. After transferring the positivity hypothesis via lt_iff_toReal_lt, it invokes the standard theorem Real.exp_log.
why it matters in Recognition Science
This lemma completes the inverse pair for the transported log and exp in the foundation layer, allowing analytic manipulations on LogicReal to reduce directly to established real-analysis facts. It supports the broader program of deriving physics from logic by providing a faithful copy of the reals inside the Recognition framework. No immediate downstream uses are recorded, but it underpins any later work that requires exponentiation or logarithms on recovered reals.
scope and limits
- Does not establish the result for non-positive arguments.
- Does not prove the symmetric logL_expL identity.
- Does not cover other functions such as sinL or cosL.
- Does not derive any physical constants or mass formulas.
formal statement (Lean)
98theorem expL_logL {x : LogicReal} (hx : (0 : LogicReal) < x) :
99 expL (logL x) = x := by
proof body
Tactic-mode proof.
100 rw [eq_iff_toReal_eq, toReal_expL, toReal_logL]
101 have hx' : 0 < toReal x := by simpa [lt_iff_toReal_lt] using hx
102 exact Real.exp_log hx'
103
104/-- Transported logarithm/exponential inverse. -/