right_distrib'
plain-language theorem explainer
Right distributivity of multiplication over addition holds on the primitive recognition calculus rationals: (a+b)·c = a·c + b·c. Cited by anyone packaging the PRCRat field axioms. The proof is a one-line wrapper of the already-proved right-distributivity identity.
Claim. For all primitive recognition rationals $a,b,c$, $(a+b)\cdot c = a\cdot c + b\cdot c$.
background
The carrier is the primitive recognition calculus rationals: nonzero-denominator ratio-orbit quotient classes, identified by cross-multiplication of orbit-level numerator and denominator (K4.8). Arithmetic on this quotient is induced from the integer layer.
At the integer layer, right distributivity is already proved: multiplication distributes on the right over addition for the primitive recognition integers, via injectivity of the integer embedding and the classical law on $\mathbb{Z}$. The present module lifts the remaining field axioms to the rational quotient so that a single certificate can assert a field structure.
Local setting is the RationalField development inside Primitive Recognition Calculus: assemble addition, multiplication, and distributivity on the ratio-orbit quotient before completeness and cost calculus.
proof idea
One-line wrapper that applies the established right-distributivity lemma to the three arguments. No new algebra is performed here; the identity is inherited from the prior proof on the integer (or already-lifted rational) operations.
why it matters
Supplies the right-distributivity field of the rational field certificate in this module. That certificate packages commutativity, associativity, units, negation, and the distributive laws so later PRC developments can treat the ratio-orbit quotient as a field.
In the Recognition Science stack this sits in Foundation, under Primitive Recognition Calculus: rationals must be a field before real completion, J-cost analysis, and the forcing chain (T5 J-uniqueness through T8). Without right distributivity the certificate cannot close, and downstream real and cost constructions lack a clean rational base.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.