mul_one'
plain-language theorem explainer
Right unit law for multiplication on PRC rationals: every ratio-orbit class times one equals itself. Cited by anyone assembling the field axioms on recognition-calculus rationals, and by the rational-field certificate. Proof is a one-line wrapper reusing the underlying integer-rational unit law.
Claim. For every PRC rational $a$ (a ratio-orbit quotient class with nonzero denominator), $a \cdot 1 = 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.
Multiplication and the multiplicative unit are already defined on this quotient. The same right-unit identity appears at every rung of the from-logic tower (naturals, integers, rationals, reals), each time as the statement that multiplying by one leaves the element unchanged.
Upstream, the integer-rational layer already proves mul a one = a by injectivity of the map into classical integers and simplification. Parallel statements hold for LogicInt and LogicRat via transport along toInt / toRat and a ring (or simp) close.
proof idea
One-line wrapper: apply the existing right-unit lemma mul_one at a. No new algebra; the quotient and coercion infrastructure already make the identity hold on PRCRat.
why it matters
This is one of the multiplicative field axioms required by rational_field_certificate, which packages commutativity, associativity, units, and inverses for PRCRat into a single certificate structure. Without the right unit law the certificate cannot be inhabited.
It mirrors the same law on LogicInt, LogicRat, and LogicReal, keeping the from-logic and PRC stacks aligned. Downstream Loom uses related unit identities on matrix letters; the pattern is the same bookkeeping step that lets recognition-built number systems support ordinary algebra before J-cost, the forcing chain (T5–T8), and the phi ladder are imposed.
No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.