add_zero'
plain-language theorem explainer
Right additive identity on PRC rationals: every ratio-orbit class plus zero equals itself. Cited by anyone assembling the additive monoid or field certificate for the PRC rational type. Proof is a one-line wrapper that applies the existing left-to-right add_zero lemma.
Claim. For every PRC rational $a$ (a ratio-orbit quotient class with nonzero denominator), $a + 0 = a$.
background
PRC rationals are the K4.8 construction: nonzero-denominator ratio-orbit quotient classes, identified by cross-multiplication of orbit-level numerator and denominator. They sit in the Primitive Recognition Calculus stack that rebuilds arithmetic from recognition primitives rather than from classical set-theoretic foundations.
The module develops the field operations and identities on this type so that a RationalFieldCertificate can be filled. Upstream, the same right-identity pattern already exists for logic naturals (n + zero = n by reflexivity), logic integers, PRC integers (via injectivity of the integer embedding), and logic rationals (via the toRat embedding and ring normalization).
Here the carrier is PRCRat with its induced addition and zero; the claim is the standard monoid right-unit law for that addition.
proof idea
One-line wrapper: the goal is exactly the statement of the sibling lemma add_zero on PRCRat, so the proof applies add_zero a and stops. No new algebraic work; it only exposes the right-identity under the primed naming used by the field certificate bundle.
why it matters
Fills the add_zero field of rational_field_certificate, which packages commutativity, associativity, left and right zero laws, and left negation for PRC rationals. That certificate is the local capstone showing the PRC rational type carries a field-ready additive structure inside the foundation layer.
Parallel add_zero' lemmas appear for logic integers, logic rationals, and logic reals; this instance is the PRC-native counterpart. It is bookkeeping in the forcing chain toward a complete arithmetic ladder (naturals through reals) built from recognition primitives, not a deep analytic step, but without it the certificate cannot close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.