toReal_coshL
plain-language theorem explainer
The transport theorem equates the hyperbolic cosine on recovered reals to the standard real hyperbolic cosine after applying the equivalence map. Researchers handling analytic identities inside the LogicReal framework cite it to reduce computations to Mathlib's real-analysis library. The proof is a one-line term that invokes the defining property of the fromReal constructor.
Claim. For every recovered real $x$, the transport satisfies $toReal(cosh_L(x)) = cosh(toReal(x))$, where $cosh_L$ is the hyperbolic cosine obtained by transporting the standard real function through the equivalence.
background
The module defines transcendental functions on LogicReal by transport through the equivalence to Mathlib's real line. LogicReal is the Cauchy completion of the recovered rationals via the canonical completion of ℚ, with toReal the map to the standard reals and fromReal its inverse. The function coshL is introduced as coshL x := fromReal (Real.cosh (toReal x)). This setting lets later modules reason directly over LogicReal while delegating analytic identities to established results. The upstream lemma toReal_fromReal supplies the reduction used here.
proof idea
The proof is a one-line term that applies toReal_fromReal directly to the definition of coshL.
why it matters
This lemma feeds the identity coshL_eq_exp, which rewrites coshL in terms of expL. It belongs to the foundational transport layer that preserves the recovered real structure while allowing reduction to Mathlib, a prerequisite for later derivations involving the phi-ladder and constants such as alpha inverse. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.