mul_zero'

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 above PRC integers and the logic-native naturals in the Primitive Recognition Calculus stack.

The module assembles the field operations on these quotients. Sibling lemmas already record additive monoid laws (associativity, zero-add, add-zero) and positivity facts; the present statement is the matching multiplicative annihilator.

Upstream, the same identity is proved first for logic naturals by reflexivity, then for PRC integers by injectivity of the integer embedding and simplification. The rational case inherits the law from the integer/rational arithmetic layer already installed on the quotient.

One-line wrapper: apply the existing mul_zero lemma at type PRCRat to the given element. No new algebra is performed; the instance or theorem already present on the rational type discharges the goal.

Completes the zero-annihilator half of the multiplicative monoid laws for PRC rationals, parallel to the additive zero laws already in the module. Downstream field and ordered-field development on the recognition ladder needs $a\cdot 0=0$ as a simp-friendly identity when normalizing costs, defects, and rung arithmetic.

In the broader RS foundation, rationals are the bridge from discrete recognition counts to the real completion used by the J-cost and the forcing chain. This lemma is elementary bookkeeping rather than a forcing step (T5–T8), but without it the rational field interface is incomplete. No used-by edges are recorded yet; it is infrastructure for later field proofs.