sinL
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.