toReal_add
plain-language theorem explainer
The transport map from recovered reals to standard reals preserves addition. Foundation-layer developers cite it when reducing algebraic identities on the logic-derived reals to their Mathlib counterparts. The proof is a one-line wrapper that invokes the round-trip identity toReal_fromReal.
Claim. For any recovered reals $x$ and $y$, the transport map satisfies $toReal(x + y) = toReal(x) + toReal(y)$.
background
The module recovers the real line from the law-of-logic rationals by completing LogicRat via Mathlib's Bourbaki completion of ℚ. LogicReal is a thin wrapper around CompareReals.Bourbakiℝ that isolates the recovered structure and lets algebra be pulled back along the transport map toReal. This yields a transport-first API so that every identity on recovered reals reduces to a standard real theorem and is read back.
proof idea
One-line wrapper that applies toReal_fromReal.
why it matters
The result feeds directly into coshL_eq_exp, where it lets the transported hyperbolic-cosine identity reduce to the standard Real.cosh_eq via repeated application of toReal_add, toReal_neg and toReal_fromReal. It closes one link in the reals-from-logic recovery chain, confirming that the pullback algebra on LogicReal is faithful to the completed rationals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.