zero_add'
plain-language theorem explainer
Zero addition holds for the logic rationals: given any a in the field of fractions of LogicInt, the sum with zero recovers a. Researchers extending the Recognition Science number hierarchy to reals cite this when confirming additive identities layer by layer. The argument is a one-line wrapper that transports the equation to Mathlib's Rat via eq_iff_toRat_eq, toRat_add and toRat_zero, then closes by ring.
Claim. Let $a$ be an arbitrary element of the field of fractions of the logic integers. Then $0 + a = a$.
background
LogicRat is the quotient of PreRat by the equivalence setoid, yielding the field of fractions of LogicInt. The module RationalsFromLogic builds this structure after IntegersFromLogic, supplying the rational layer required for later real-number constructions in the Recognition Science foundation. The upstream integer result states that zero plus any LogicInt recovers the integer, proved by the same transport-plus-ring pattern.
proof idea
The term proof invokes eq_iff_toRat_eq to replace LogicRat equality by equality of images under toRat. It then applies toRat_add and toRat_zero to obtain the equation 0 + toRat a = toRat a inside Mathlib's Rat, after which ring finishes the proof.
why it matters
This theorem is invoked by the zero_add' statements in IntegersFromLogic and RealsFromLogic, guaranteeing that the additive identity behaves uniformly across the constructed number systems. It supplies the rational step in the foundation that precedes the reals, supporting the Recognition Science derivation of constants from the single functional equation and the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.