expL
plain-language theorem explainer
The exponential on the recovered reals is obtained by transporting Mathlib's standard exponential through the canonical equivalence between LogicReal and ℝ. Analysts working within the Recognition Science framework cite this when they need to lift real-analytic identities to the logic-derived number system. The definition is a direct composition of toReal, Real.exp, and fromReal.
Claim. Define the exponential function $exp_L : LogicReal → LogicReal$ by $exp_L(x) = fromReal(exp(toReal(x)))$, where $toReal$ and $fromReal$ realize the equivalence $LogicReal ≃ ℝ$.
background
LogicReal is the structure realizing the recovered real line as the Cauchy completion of the logic-derived rationals, equipped with an equivalence to Mathlib's ℝ via the maps toReal and fromReal. The module LogicRealTranscendentals transports the standard transcendental functions across this equivalence so that later developments can work directly with LogicReal while delegating analytic facts to the established library.
proof idea
This is a one-line definition that composes the transport toReal, applies Mathlib's Real.exp, and returns via fromReal. No tactics are used; the body is the direct term fromReal (Real.exp (toReal x)).
why it matters
This definition supplies the exponential for the suite of transported transcendentals in LogicRealTranscendentals. It is invoked by the inverse theorems expL_logL and logL_expL, the positivity result expL_pos, the transport lemma toReal_expL, and the hyperbolic identity coshL_eq_exp. In the Recognition Science framework it provides the analytic foundation needed to define J-cost and related functions on the recovered reals without re-proving real analysis from the seven axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.