coshL_eq_exp
plain-language theorem explainer
The theorem establishes that hyperbolic cosine on the recovered real line equals the average of the exponential at x and at -x. Analysts working with LogicReal in foundational derivations would cite this when reducing hyperbolic identities to the exponential. The proof reduces both sides to Mathlib reals via transport lemmas and invokes the standard identity there.
Claim. For any element $x$ of the recovered real line, the transported hyperbolic cosine satisfies $cosh_L(x) = (exp_L(x) + exp_L(-x))/2$, where both functions are obtained by transporting the classical real functions through the equivalence with $mathbb{R}$.
background
The module defines transcendental functions on LogicReal by transport through the equivalence with Mathlib reals. coshL is introduced as fromReal (Real.cosh (toReal x)) and expL as fromReal (Real.exp (toReal x)). The supporting transport theorems state that toReal (coshL x) equals Real.cosh (toReal x) and likewise for expL. The equality transfer result asserts that two LogicReal elements coincide precisely when their toReal images coincide. This arrangement lets later modules reason inside LogicReal while delegating analytic identities to the established real-analysis library.
proof idea
The term proof first rewrites the goal via eq_iff_toReal_eq, then applies the transport lemmas toReal_coshL, toReal_div, toReal_add, toReal_expL (twice), toReal_neg, and toReal_fromReal. The resulting identity on Mathlib reals is discharged directly by Real.cosh_eq.
why it matters
The result supplies the standard hyperbolic identity inside the transported setting, fulfilling the module's purpose of preserving classical analysis on the recovered reals. It belongs to the family of transport theorems that includes the corresponding statements for expL, sinL, and cosL. In the Recognition Science chain this ensures that later steps relying on hyperbolic functions remain compatible with the phi-ladder and forcing relations once the real line is recovered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.