expL_pos
plain-language theorem explainer
The transported exponential on LogicReal is strictly positive for every input. Analysts using the recovered reals in Recognition Science cite this when deriving inequalities for growth rates or probabilities. The proof reduces the claim to Mathlib's Real.exp_pos via three transport lemmas in a single rewrite step.
Claim. For every $x$ in LogicReal, $0 < exp_L(x)$, where $exp_L$ is the exponential obtained by transporting Real.exp through the equivalence LogicReal ≃ ℝ.
background
LogicReal is the structure realizing the Cauchy completion of recovered rationals, equivalent to Mathlib's ℝ via toReal and fromReal. The module defines standard transcendentals by transport so that later modules can reason over LogicReal while reducing analytic identities to Mathlib's library. Upstream results include the definition expL x := fromReal (Real.exp (toReal x)), the transport theorem toReal_expL stating toReal (expL x) = Real.exp (toReal x), and the order isomorphism lt_iff_toReal_lt together with toReal_zero from RealsFromLogic.
proof idea
The proof rewrites the LogicReal inequality using lt_iff_toReal_lt, toReal_zero, and toReal_expL. This reduces the goal to Real.exp (toReal x) > 0, which is discharged by Real.exp_pos.
why it matters
This lemma secures positivity of the exponential on the recovered reals, supporting constructions that rely on growth properties in the foundation layer. It fills a basic transport gap consistent with the module's strategy of reducing to Mathlib while preserving the LogicReal interface. No downstream parents are recorded in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.