toReal_cosL
plain-language theorem explainer
The transport lemma shows that cosine defined on the recovered real line agrees with standard cosine after mapping to Mathlib reals. Analysts working with recovered reals cite this to reduce trigonometric identities to the established library. The proof is a one-line application of the fromReal transport theorem.
Claim. For every recovered real $x$, the transport of the cosine on recovered reals satisfies $toReal(cos_L(x)) = cos(toReal(x))$, where $cos_L$ is the transported cosine.
background
The module defines transcendental functions on LogicReal by transport through the equivalence to Mathlib's real line. LogicReal is the structure wrapping the Bourbaki completion of recovered rationals to avoid global instance pollution. The map toReal sends a LogicReal to its Mathlib real via CompareReals.compareEquiv. The cosine on recovered reals is defined by cosL(x) := fromReal(Real.cos(toReal(x))). Upstream, toReal_fromReal states that toReal(fromReal(x)) = x for any real x. The module documentation states that this transport layer lets later modules reason over LogicReal while reducing analytic identities to Mathlib's library.
proof idea
This is a one-line wrapper that applies toReal_fromReal. Because cosL x is defined as fromReal(Real.cos(toReal x)), applying toReal yields toReal(fromReal(Real.cos(toReal x))), which equals Real.cos(toReal x) by the transport theorem.
why it matters
This completes the transport for cosine, allowing later modules to work directly with LogicReal while preserving compatibility with standard real analysis. It forms part of the foundational layer for transcendental functions in the recovered reals, as described in the module documentation. No downstream uses are listed, but it supports the overall equivalence between LogicReal and the reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.