sinL
sinL defines sine on the recovered real line LogicReal by transporting Mathlib's Real.sin through the canonical maps toReal and fromReal. Foundation-layer analysts cite it when extending trigonometric identities to logic-derived reals while preserving reduction to established analysis. The definition is a direct one-line composition that inherits all analytic properties via the equivalence.
claimLet $x$ belong to the recovered real line. Define the sine function on recovered reals by $sin_L(x) = fromReal(Real.sin(toReal(x)))$, where toReal and fromReal are the mutual inverse transports realizing the equivalence between LogicReal and the standard reals.
background
LogicReal is the structure wrapping the Bourbaki completion of the rationals, realized through the canonical equivalence LogicRat ≃ ℚ. The maps toReal and fromReal are the noncomputable transports: toReal extracts the Mathlib real via CompareReals.compareEquiv, while fromReal injects a standard real back into the wrapper. The module LogicRealTranscendentals defines standard transcendental functions by transport through this equivalence, allowing analytic identities to reduce directly to Mathlib's real-analysis library.
proof idea
This is a one-line definition that applies fromReal to the result of Real.sin applied to toReal x, directly transporting the function without additional lemmas or tactics.
why it matters in Recognition Science
This definition supplies the sine operation required by the downstream transport theorem toReal_sinL, which asserts toReal(sinL x) = Real.sin(toReal x). It belongs to the foundational layer that equips LogicReal with transcendentals while preserving reduction to Mathlib, supporting later development of analytic identities on the recovered reals.
scope and limits
- Does not prove any trigonometric identities or addition formulas for sinL.
- Does not define sine on complex numbers or other extensions.
- Does not address series expansions or convergence questions.
- Does not connect directly to the phi-ladder or rung-fraction machinery.
formal statement (Lean)
41def sinL (x : LogicReal) : LogicReal := fromReal (Real.sin (toReal x))
proof body
Definition body.
42
43/-- Cosine on recovered reals. -/