sinhL
plain-language theorem explainer
The definition equips the recovered real line with hyperbolic sine by transporting the classical sinh through the equivalence to Mathlib reals. Researchers extending real analysis inside the Recognition framework cite this when they need hyperbolic functions to stay inside the recovered line. The construction is a direct one-line wrapper composing the two transport maps around Real.sinh.
Claim. For an element $x$ of the recovered real line, the hyperbolic sine is defined by $sinh(x) := iota^{-1}(sinh(iota(x)))$, where $iota$ is the canonical equivalence transporting the recovered reals to the classical reals $mathbb{R}$.
background
The recovered real line is realized as a structure whose underlying value is the Bourbaki completion of the rationals, wrapped to avoid polluting global instances on the completion. The forward transport extracts the classical real value via the equivalence, while the inverse transport injects a classical real back into the recovered line. This module transports the standard transcendental functions across that equivalence so that analytic identities reduce directly to Mathlib's library.
proof idea
The definition is a one-line wrapper that applies the inverse transport to Real.sinh composed with the forward transport on the input.
why it matters
This definition supplies hyperbolic sine on the recovered reals and is invoked by the transport theorem confirming that the equivalence commutes with sinh. It forms part of the foundational layer that lets the Recognition framework handle transcendental functions by reduction to Mathlib, supporting later analytic development without re-proving basic facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.