toReal_sinL
The theorem shows that sine defined on the recovered real line commutes with the transport map to Mathlib's standard reals. Researchers formalizing analytic identities over custom real structures cite it to reduce trigonometric calculations to the established library. The proof is a one-line wrapper that substitutes the definition of the transported sine and invokes the general transport lemma.
claimFor any recovered real $x$, the transport of the sine of $x$ equals the standard sine of the transport of $x$.
background
The module transports standard transcendental functions onto LogicReal, the Cauchy completion of recovered rationals, via the equivalence to Mathlib's real line. LogicReal carries a transport map toReal that sends each element to its counterpart in ℝ and an inverse fromReal. The sine operation is introduced by the definition sinL(x) := fromReal(Real.sin(toReal(x))).
proof idea
The proof is a one-line wrapper that applies the transport lemma toReal_fromReal. After substituting the definition of sinL, the expression reduces to toReal(fromReal(Real.sin(toReal(x)))), which the lemma simplifies directly to Real.sin(toReal(x)).
why it matters in Recognition Science
This result belongs to the transport layer that equips the recovered reals with analytic operations while preserving reduction to Mathlib. It supports the Recognition framework's strategy of deriving physical models over LogicReal without re-proving trigonometric identities. The lemma closes the sine case in the sequence of transported transcendentals defined in the same module.
scope and limits
- Does not establish any new trigonometric identities beyond the transport equality.
- Does not address complex extensions or other transcendental functions.
- Does not depend on Recognition Science constants or the forcing chain.
- Does not provide numerical evaluation or approximation results.
formal statement (Lean)
71@[simp] theorem toReal_sinL (x : LogicReal) :
72 toReal (sinL x) = Real.sin (toReal x) :=
proof body
One-line wrapper that applies toReal_fromReal.
73 toReal_fromReal _
74