add_comm'
plain-language theorem explainer
Addition commutes for elements of LogicReal, the Cauchy completion of logic-derived rationals. Foundation developers cite this when transporting ring identities from Mathlib reals into the recovered layer. The proof rewrites equality through the transport map and reduces the statement to the ring tactic on the underlying Bourbaki reals.
Claim. For all recovered reals $x, y$ in the Cauchy completion of the logic rationals, $x + y = y + x$.
background
The module recovers the real line from the Law-of-Logic layer by completing the recovered rationals LogicRat via Mathlib's Bourbaki completion of Q. LogicReal is defined as a wrapper around CompareReals.BourbakiR whose transport map toReal pulls back the standard real structure, so algebraic operations on LogicReal are defined by transport. Upstream results supply the same commutativity statement for LogicInt and LogicRat, each proved by reducing via their own equality transport (eq_iff_toInt_eq, eq_iff_toRat_eq) and applying ring.
proof idea
One-line wrapper that rewrites the goal with eq_iff_toReal_eq, then applies simp followed by ring on the images under toReal.
why it matters
The theorem supplies the additive commutativity axiom for the recovered reals, closing the transport of ring structure from Mathlib into the logic-derived line. It sits downstream of the integer and rational commutativity results and is itself referenced by those same statements in the dependency graph, completing the algebraic layer before further Recognition Science constructions. No open scaffolding remains for this identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.