zero_add'
plain-language theorem explainer
Left additive identity on PRC rationals: zero plus any ratio-orbit class equals that class. Cited by anyone assembling the additive group (or field) structure on recognition-derived rationals. Proof is a one-line wrapper that applies the underlying zero_add lemma.
Claim. For every PRC rational $a$ (a nonzero-denominator ratio-orbit quotient class), $0 + a = a$.
background
PRC rationals are the type of ratio-orbit quotient classes: pairs of recognition integers with nonzero denominator, identified when cross-multiplication of orbit-level numerators and denominators agrees. Addition and the additive zero are inherited from that quotient construction.
This sits in the Primitive Recognition Calculus layer that rebuilds $\mathbb{Q}$ from recognition primitives rather than from classical set-theoretic constructions. Parallel left-identity lemmas already exist for logic naturals, logic integers, PRC integers, logic rationals, and logic reals; each reduces addition-with-zero to the corresponding carrier equality.
The local module packages the field axioms on these rationals. Upstream, the integer-level zero_add on PRC integers is the direct computational ancestor that the rational wrapper invokes.
proof idea
One-line wrapper: apply the existing zero_add lemma at the PRC-rational level to the given class $a$. No new quotient reasoning, induction, or ring tactic is introduced here; the identity is delegated entirely to that prior result.
why it matters
Fills the left-zero field axiom slot in rational_field_certificate, which bundles commutativity, associativity, left and right zero, and left negation for PRC rationals. That certificate is the formal witness that recognition-built rationals carry a field-ready additive structure before completeness and real extension.
It mirrors the same named identity on logic integers, logic rationals, and logic reals, keeping the FromLogic and PRC stacks aligned. In the broader Recognition foundation this is bookkeeping on the arithmetic ladder that eventually supports the forcing chain and cost calculus, not a physics claim by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.