one_mul'
plain-language theorem explainer
Left unit law for multiplication on PRC rationals: the multiplicative identity acts as a left identity. Anyone assembling the field axioms for the ratio-orbit quotient cites this. The proof is a one-line wrapper reusing the existing left-unit lemma on the same carrier.
Claim. For every PRC rational $a$ (a ratio-orbit quotient class with nonzero denominator), $1 \cdot a = a$.
background
PRC rationals are the carrier PRCRat: quotient classes of ratio orbits under cross-multiplication identification of numerator and denominator orbits, with nonzero denominator (K4.8). They sit in the Primitive Recognition Calculus stack that rebuilds arithmetic from recognition primitives rather than from classical set-theoretic constructions.
Multiplication and the unit 1 are already defined on this carrier. Parallel left-unit statements exist upstream for logic naturals (succ zero * n = n), logic integers, PRC integers (mul one a = a), and the logic-rational and logic-real layers. The present lemma is the same algebraic fact specialized to the PRC rational field layer.
The local module packages the field axioms needed for a RationalFieldCertificate, so each monoid and group identity appears as a named lemma before being bundled.
proof idea
One-line wrapper: apply the existing left-unit lemma one_mul on PRCRat to the same argument a. No new algebra; the primed name matches the certificate and Loom naming convention used across the foundation stack.
why it matters
Feeds rational_field_certificate, which records the field axioms for PRC rationals (add_comm, add_assoc', zero_add', add_zero', add_left_neg', and the multiplicative unit laws). Parallel one_mul' lemmas appear for logic integers, logic rationals, logic reals, and Loom matrices, so this entry keeps the PRC rational layer aligned with that naming and proof pattern.
In the Recognition foundation, a certified rational field is a prerequisite for completing reals and for any later analytic structure (costs, continuity, ladder arithmetic). This is ordinary monoid algebra, not a forcing-chain step (T5–T8), but without it the rational-field certificate cannot close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.