zero_add'
plain-language theorem explainer
The recovered real numbers satisfy the zero-addition identity. Foundation-layer proofs in Recognition Science cite this result when lifting additive identities from the completed rationals. The short tactic proof applies the equality-transfer lemma to reduce the claim to Mathlib's reals and lets simplification finish the verification.
Claim. For every recovered real number $x$, one has $0 + x = x$.
background
LogicReal is the wrapper around Mathlib's Bourbaki completion of the rationals, obtained after recovering LogicRat from the law of logic. The module recovers the real line by completing the recovered rationals and transporting all structure along the equivalence toReal. Upstream, the integers and rationals layers already establish the corresponding zero-addition identities, and eq_iff_toReal_eq states that equality on LogicReal is equivalent to equality after transport to the standard reals.
proof idea
The proof first rewrites the goal using eq_iff_toReal_eq, which converts the statement into an equality on the underlying Bourbaki real. Simplification then invokes the known zero-addition property on the completed reals.
why it matters
This result completes the additive monoid structure on the recovered reals, feeding the same identity into the integer and rational layers via transport. It sits inside the RealsFromLogic module whose purpose is to obtain ℝ from the logic-derived rationals, directly supporting the T0-T8 forcing chain by ensuring the real numbers behave as expected under addition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.