left_distrib'
plain-language theorem explainer
Multiplication on PRC rationals distributes on the left over addition: a(b+c)=ab+ac for all a,b,c. Anyone assembling the RationalFieldCertificate (or any field-axiom bundle over PRCRat) cites this form. The proof is a one-line term that reuses the underlying left_distrib lemma under operator notation.
Claim. For all PRC rationals $a,b,c$ (nonzero-denominator ratio-orbit quotient classes), $a\cdot(b+c)=a\cdot b+a\cdot c$.
background
PRC rationals (PRCRat) are the choice-light quotient of ratio orbits with nonzero denominator, identified by cross-multiplication of orbit-level numerators and denominators. Arithmetic is lifted from the integer layer (PRCInt) through that quotient; the module builds the field operations and the primed axiom forms needed by the certificate.
At the integer layer, left distributivity is already proved by injecting into ordinary Int and using Int.mul_add. The rational layer inherits the same identity once multiplication and addition are defined on quotient classes. Sibling lemmas in this file supply the other additive and multiplicative field laws in the same primed, operator-notation style.
Structural nontriviality (0 ≠ 1) is handled separately by the choice-free isZero discriminator on balanced signed orbits, so the field package never needs a classical ℚ display.
proof idea
One-line term proof: apply the existing left_distrib lemma at a, b, c. No new quotient induction or cross-multiplication algebra is done here; the primed name is only the operator-notation packaging (* and +) expected by the field certificate.
why it matters
This is one of the multiplicative-distributive slots in rational_field_certificate, which packages the full field axiom bundle for PRC rationals (add_comm, add_assoc', zero_add', add_zero', add_left_neg', and the matching mul/distrib laws). Without left distributivity the certificate cannot close.
In the Primitive Recognition Calculus stack, a verified rational field is the bridge from the integer/orbit layer toward the real-completion and continuity modules that later host the J-cost and the forcing chain. The result is pure foundation algebra: it does not itself invoke T5–T8, RCL, or the phi ladder, but every later analytic step that treats PRCRat as a field depends on this certificate entry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.