add_zero'
plain-language theorem explainer
The declaration proves that zero functions as the additive identity in the field of fractions LogicRat built from logic integers. Researchers constructing the Recognition Science number systems from first principles cite it when verifying ring axioms at the rational level. The proof reduces the claim to the corresponding identity in Mathlib's Rat via transport lemmas and finishes by ring normalization.
Claim. For every $a$ in the field of fractions of the logic-constructed integers, $a + 0 = a$.
background
LogicRat is the quotient of PreRat pairs by the setoid equivalence relation, forming the field of fractions of LogicInt. The module builds rationals after the integers from IntegersFromLogic, using the transfer principle eq_iff_toRat_eq that equates LogicRat equality with equality after mapping to standard Rat. Upstream, the add_zero' theorem for LogicInt supplies the integer-level identity, while toRat_add and toRat_zero supply the compatibility of addition and zero with the transport map.
proof idea
The proof rewrites the goal with eq_iff_toRat_eq, replaces the left-hand side via toRat_add and toRat_zero, and applies the ring tactic to obtain the identity in Rat.
why it matters
This supplies the additive identity axiom for LogicRat and is invoked by the add_zero' theorems in IntegersFromLogic and RealsFromLogic. It closes one step in the foundation layer that equips the constructed numbers with ring structure needed for the Recognition Composition Law and the T0-T8 forcing chain. No open scaffolding remains at this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.