add_zero'
plain-language theorem explainer
Additive identity holds for the recovered real numbers: any element of LogicReal plus zero equals itself. Researchers constructing ring or field axioms on the logic-derived reals cite this to confirm the zero element. The proof is a one-line wrapper that transports the claim via equality transfer and simplifies on the underlying Mathlib reals.
Claim. For all $x$ in the Cauchy completion LogicReal of the recovered rationals, $x + 0 = x$.
background
The module recovers the real numbers from the Law-of-Logic rational layer by completing LogicRat ≃ ℚ via Mathlib's Bourbaki uniform-space completion. LogicReal is defined as a wrapper around CompareReals.Bourbakiℝ to avoid polluting global instances while reusing the completed real line; algebra is pulled back along the transport maps toReal and fromReal. The module doc states the chain: Law of Logic yields LogicNat, LogicInt, LogicRat ≃ ℚ, then Completion ℚ ≃ ℝ. Upstream results supply the matching add_zero' theorems on LogicInt and LogicRat, each proved by transport to the base type followed by ring simplification.
proof idea
One-line wrapper that applies the equality transfer theorem eq_iff_toReal_eq to reduce to an identity on Mathlib reals, then invokes simp to discharge the statement using the underlying addition and zero.
why it matters
This result closes the additive monoid structure on LogicReal and is referenced by the parallel add_zero' statements in IntegersFromLogic and RationalsFromLogic, maintaining uniformity across the logic-to-reals recovery. It fills the algebraic layer needed before order or metric properties are lifted, consistent with the module's transport-first design that lets every downstream theorem reduce to an existing real-number fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.