zero_mul'
plain-language theorem explainer
Left multiplication by zero annihilates every PRC rational: $0\cdot a=0$. Anyone assembling the field axioms for the primitive recognition calculus rationals cites this. The proof is a one-line wrapper that reuses the existing zero-multiplication lemma on the same carrier.
Claim. For every PRC rational $a$ (a ratio-orbit quotient class with nonzero denominator), left multiplication by the additive identity satisfies $0 \cdot a = 0$.
background
PRC rationals (PRCRat) are the K4.8 carrier: nonzero-denominator ratio-orbit quotient classes, identified by cross-multiplication of orbit-level numerator and denominator. They sit above the PRC integers and ultimately above the logic naturals built in ArithmeticFromLogic.
The module develops the ordered-field skeleton needed by the primitive recognition calculus, importing the J-cost layer and the integer/rational constructions. Zero multiplication is already known on logic naturals (by induction on the successor) and on PRC integers (by injectivity of the integer embedding). This declaration lifts the same identity to the rational quotient.
proof idea
One-line wrapper: apply the existing zero_mul lemma at type PRCRat to the given argument. No new algebra is performed; the proof simply re-exports the annihilator identity under the primed name used by the surrounding field-axiom suite (siblings include zero_add', add_zero', add_assoc').
why it matters
Field axioms on the PRC rationals are infrastructure for the Recognition Composition Law and the forcing chain that produces $J$, $\varphi$, the eight-tick octave, and $D=3$. Without $0\cdot a=0$, the multiplicative monoid and the later completeness/continuity layers cannot be stated cleanly. Downstream use is currently empty in the graph, so the lemma is local scaffolding for the rational field instance rather than a cited step in a named paper proposition. It closes a routine gap in the K4.8 arithmetic package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.