toReal_sinhL
plain-language theorem explainer
The declaration shows that the hyperbolic sine transported to the recovered real line equals the standard real hyperbolic sine after transport. Workers building analytic identities over LogicReal in the Recognition Science foundation cite it to reduce calculations to Mathlib. The proof is a one-line wrapper that invokes the general transport theorem toReal_fromReal after unfolding the definition of sinhL.
Claim. For every recovered real $x$, the transport map applied to the transported hyperbolic sine of $x$ equals the hyperbolic sine of the transport of $x$.
background
The module equips the recovered real line with standard transcendental functions by transport through the equivalence to Mathlib's real line. LogicReal is the Cauchy completion of the recovered rationals, realized through the canonical completion of ℚ together with the equivalence LogicRat ≃ ℚ. The function sinhL is defined by sinhL(x) := fromReal(Real.sinh(toReal(x))). The upstream lemma toReal_fromReal states that toReal(fromReal(y)) = y for any real y, and toReal itself is the comparison equivalence map.
proof idea
The proof is a one-line wrapper that applies the lemma toReal_fromReal. Unfolding sinhL produces toReal(fromReal(Real.sinh(toReal(x)))), which reduces directly to Real.sinh(toReal(x)) by the transport theorem.
why it matters
This transport lemma belongs to the layer that equips the recovered reals with standard transcendental functions while preserving equivalence to ℝ. It supports the foundation for using analytic identities in Recognition Science without leaving the LogicReal structure. No immediate downstream theorems are listed, but the result closes one link in the chain that lets later modules reduce hyperbolic identities to Mathlib.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.