add_assoc
plain-language theorem explainer
Addition of PRC integers is associative: (a+b)+c equals a+(b+c). Anyone building rings, cost algebra, or φ-ladder arithmetic on the signed-orbit integers cites this. The proof is a two-line transport: injectivity of the integer display plus Mathlib's Int.add_assoc.
Claim. For all PRC integers $a,b,c$ (quotient classes of signed orbits under the balanced-length relation), $(a+b)+c = a+(b+c)$, where $+$ is the induced addition on the quotient.
background
PRC integers are the quotient of signed orbits by the internal balanced-length setoid (K4.8). Each class has a canonical display toInt into ordinary $\mathbb{Z}$; addition on representatives is componentwise on the positive and negative orbit parts and descends to the quotient.
The surrounding module builds integers and rationals from the Primitive Recognition Calculus without classical choice in the core operations. Upstream, addition on the underlying signed orbits already agrees with integer addition under toInt (add_toInt), and the same associativity pattern was proved earlier for logic naturals by induction on the successor.
Locally one only needs that equal integer displays imply equal quotient classes, so algebraic identities true in $\mathbb{Z}$ lift once the display is shown to be a homomorphism.
proof idea
Apply injectivity of the integer display on PRC integers. After rewriting both sides under toInt, the goal is ordinary integer associativity, discharged by simp with Mathlib's Int.add_assoc. The homomorphism property of addition under toInt is already available from the sibling add_toInt (and the quotient construction), so no fresh case analysis on representatives is required.
why it matters
This is the associativity half of the additive monoid (and later group) structure on PRC integers. Downstream it is consumed by cost algebra (H_dAlembert, the multiplicative d'Alembert form whose continuous solution is cosh, feeding the Recognition Composition Law and J-cost), by $\mathbb{Z}[\varphi]$ (PhiInt), by F2-power arithmetic, and by concrete $\alpha$-genesis numerical bounds that need ring tactics over integers.
In the forcing chain this sits under the arithmetic substrate that later supports T5 J-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Without associative addition on the native integers, the φ-ladder mass formula and the eight-tick bookkeeping cannot be stated inside the formal development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.