expL_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish positivity for other transported functions such as logL or sinhL.
- Does not supply growth rates or derivative bounds beyond strict positivity.
- Does not extend to complex exponentials or vector-valued cases.
- Applies only inside the LogicReal structure and its equivalence to standard reals.
formal statement (Lean)
88theorem expL_pos (x : LogicReal) : (0 : LogicReal) < expL x := by
proof body
Term-mode proof.
89 rw [lt_iff_toReal_lt, toReal_zero, toReal_expL]
90 exact Real.exp_pos _
91
92/-- Transported non-negativity of square root. -/