toReal_expL
plain-language theorem explainer
The lemma equates the transported exponential on recovered reals with the standard real exponential after applying the equivalence map. Analysts working with LogicReal cite it to reduce analytic identities to Mathlib's library. The proof is a one-line wrapper that invokes the general transport theorem toReal_fromReal on the definition of expL.
Claim. For any recovered real $x$, the transported exponential satisfies $toReal(exp_L(x)) = exp(toReal(x))$, where $exp_L$ is obtained by transporting the standard exponential through the equivalence between recovered and standard reals.
background
LogicReal is the structure that realizes the Cauchy completion of the recovered rationals via the canonical completion of ℚ and the equivalence LogicRat ≃ ℚ; the wrapper prevents global instance pollution while reusing Mathlib's completed real line. The map toReal sends a LogicReal to its image in ℝ via CompareReals.compareEquiv, and fromReal is the inverse transport. The exponential expL is defined by transport: expL x := fromReal (Real.exp (toReal x)). This module defines all standard transcendentals by the same transport and proves the corresponding reduction lemmas so that later modules can reason over LogicReal while delegating analytic facts to Mathlib.
proof idea
The proof is a one-line wrapper that applies toReal_fromReal. Substituting the definition of expL immediately reduces toReal (fromReal (Real.exp (toReal x))) to Real.exp (toReal x) by the transport property.
why it matters
This lemma is invoked directly in the proofs of expL_logL, logL_expL, expL_pos, and coshL_eq_exp to establish the functional equations and positivity properties of the transported transcendentals. It completes the transport layer in the foundation module, ensuring the recovered reals carry the full analytic structure needed for the J-cost function and the phi-ladder. In the Recognition Science framework this step supports the recovery of the real line as a prerequisite for deriving the eight-tick octave and the constants in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.