cosL
Cosine on the recovered real line is obtained by transporting Mathlib's cosine through the canonical equivalence between LogicReal and the standard reals. Workers in the Recognition Science foundation cite this definition when they need trigonometric functions that remain inside the LogicReal structure. The implementation is a direct one-line composition of toReal, Real.cos, and fromReal.
claimFor an element $x$ of the recovered real line, define $cos_L(x) := fromReal(Real.cos(toReal(x)))$, where $toReal$ and $fromReal$ are the mutually inverse transport maps realizing the equivalence between LogicReal and $ℝ$.
background
LogicReal is the structure wrapping the Bourbaki completion of the recovered rationals, with toReal extracting the Mathlib real via CompareReals.compareEquiv and fromReal injecting a Mathlib real back by applying the inverse equivalence. The module LogicRealTranscendentals defines the standard transcendental functions on this recovered real line by transport through the equivalence LogicReal.equivReal, so that later proofs can manipulate them while always reducing analytic steps to Mathlib's library.
proof idea
This is a one-line wrapper definition that composes the transport functions around Mathlib's cosine: it applies toReal to the input, passes the result to Real.cos, and wraps the output with fromReal.
why it matters in Recognition Science
This definition is used by the transport theorem toReal_cosL, which proves that toReal(cosL x) equals Real.cos(toReal x). It completes the basic layer of transcendental functions on LogicReal, allowing the Recognition Science framework to import standard real-analysis results without leaving the logic-derived number system. The module documentation states that this transport layer is the right first step before defining more complex operations.
scope and limits
- Does not prove any trigonometric identities for cosine.
- Does not define cosine independently of Mathlib's Real.cos.
- Does not extend the function to complex numbers or other domains.
formal statement (Lean)
44def cosL (x : LogicReal) : LogicReal := fromReal (Real.cos (toReal x))
proof body
Definition body.
45
46/-- Hyperbolic sine on recovered reals. -/