add_assoc'
plain-language theorem explainer
Addition of PRC rationals is associative: $(a+b)+c = a+(b+c)$ for all quotient classes built from ratio orbits. Field-structure and certificate authors cite it when assembling the additive monoid laws on the recognition-calculus rationals. The proof is a one-line wrapper that applies the existing `add_assoc` lemma on the same type.
Claim. For all recognition-calculus rationals $a,b,c$ (quotient classes of ratio orbits with nonzero denominator), $(a+b)+c = a+(b+c)$.
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 distinction orbits rather than from a bare set-theoretic copy of $\mathbb{Q}$.
The surrounding section collects operator-form field laws (associativity, units, inverses) in the style used by the parallel LogicNat / LogicInt / LogicRat towers. Upstream, the same identity is already proved for distinction naturals, logic naturals, PRC integers (via injectivity of the integer embedding and Mathlib Int.add_assoc), and logic integers (via the toInt transfer principle). This declaration is the rational-level instance of that chain.
proof idea
One-line wrapper: the goal is exactly the statement of the in-scope add_assoc lemma on PRCRat, so the proof applies that lemma to the three arguments and stops. No new quotient reasoning or transfer step is performed here.
why it matters
The rational field certificate packages this lemma as its add_assoc field, together with commutativity, zero laws, and left negation. That certificate is the formal witness that PRC rationals carry a field-ready additive structure inside the recognition stack.
Parallel add_assoc' results in the IntegersFromLogic, RationalsFromLogic, and RealsFromLogic modules follow the same naming pattern and feed the corresponding logic-number towers. In the broader Recognition Science foundation, these operator laws underwrite the arithmetic substrate on which the forcing chain (T0–T8), the J-cost calculus, and later continuum constructions rest. The declaration itself is closed (proved, no sorry); it does not touch open physics claims such as the alpha band or mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.