toReal_add
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove preservation of multiplication or other ring operations.
- Does not establish that LogicReal is a field or ordered field.
- Does not address completeness or uniform-space properties beyond the transport equivalence.
Lean usage
example (x y : LogicReal) : toReal (x + y) = toReal x + toReal y := toReal_add x yformal statement (Lean)
138@[simp] theorem toReal_add (x y : LogicReal) : toReal (x + y) = toReal x + toReal y :=
proof body
One-line wrapper that applies toReal_fromReal.
139 toReal_fromReal _