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