coshL
plain-language theorem explainer
coshL defines hyperbolic cosine on the recovered real line LogicReal by transporting Mathlib's Real.cosh through the toReal and fromReal equivalence maps. Analysts working inside the Recognition Science foundation cite it when they need hyperbolic functions without exiting the LogicReal type. The definition is a direct one-line transport that inherits all Mathlib properties via the isomorphism.
Claim. For $x$ in the recovered real line, the hyperbolic cosine is defined by transporting the standard function: $cosh_L(x) = fromReal(Real.cosh(toReal(x)))$, where toReal and fromReal realize the equivalence between LogicReal and $ℝ$.
background
LogicReal is the structure that wraps the Bourbaki completion of the recovered rationals, with toReal extracting the underlying Mathlib real and fromReal injecting a Mathlib real back into LogicReal. The module LogicRealTranscendentals defines standard transcendental functions by transport through the equivalence LogicReal ≃ ℝ, so that later modules can reason over LogicReal while reducing analytic identities to Mathlib's real-analysis library. Upstream results establish the transport: fromReal and toReal give the isomorphism, while the RungFractions toReal handles related real conversions for exponents.
proof idea
One-line definition that applies fromReal to Real.cosh composed with toReal.
why it matters
This definition supplies the base for the transport theorems coshL_eq_exp and toReal_coshL, which reduce hyperbolic identities back to Mathlib's Real.cosh_eq. It completes the first layer of transcendentals on LogicReal inside the Recognition Science foundation, allowing subsequent modules to stay inside the recovered reals. No direct link to the T0-T8 chain, but it supports the real-analysis substrate needed for later physical derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.