coshL
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.
claimFor $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 in Recognition Science
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.
scope and limits
- Does not prove any functional equations or addition formulas for coshL.
- Does not extend the definition to complex arguments or other fields.
- Does not address convergence, series expansions, or analytic continuation.
formal statement (Lean)
50def coshL (x : LogicReal) : LogicReal := fromReal (Real.cosh (toReal x))
proof body
Definition body.
51