add_comm
plain-language theorem explainer
Addition of PRC integers (signed-orbit quotient classes) is commutative. Anyone assembling the ring axioms on the recognition-calculus integers, or any algebra that sits on that ring, cites this lemma. The proof is a two-line push through the injective integer display, then Mathlib's ordinary integer commutativity.
Claim. For all PRC integers $a,b$ (equivalence classes of signed orbits under the balanced-length relation), $a+b=b+a$.
background
PRC integers are the quotient of signed orbits by the internal balanced-length setoid. Each class has an injective display toInt into ordinary $\mathbb{Z}$; the verifier identity of two classes is settled by equality of those displays. Addition on representatives is defined so that it descends to the quotient and satisfies (add a b).toInt = a.toInt + b.toInt.
The surrounding module builds integer and rational arithmetic from primitive recognition orbits (K4.8), after the LogicNat layer has already recovered Peano-style addition and multiplication. The ring-axioms subsection then lifts the usual $\mathbb{Z}$ laws across the display.
Upstream, signed-orbit addition already agrees with integer addition (add_toInt), and LogicNat addition is commutative by induction on the step constructor. Those facts make the quotient-level commutativity a pure transport argument.
proof idea
Apply injectivity of the integer display on PRC integers. The goal becomes an equality in $\mathbb{Z}$. Simplify with the simp lemmas that unwind PRC addition to integer addition, then finish by Mathlib's Int.add_comm. No induction on orbits is needed at this layer; the work was already done on representatives and on LogicNat.
why it matters
This is one of the basic ring axioms on PRC integers under K4.8, the bridge from recognition orbits to ordinary arithmetic. Downstream it is consumed widely: CostAlgebra's proof that $H$ satisfies the multiplicative d'Alembert equation (the RCL form whose continuous solution is cosh, feeding T5 J-uniqueness), the $\mathbb{Z}[\varphi]$ structure PhiInt, F2Power group laws, Cosmology rung-coarsening cross-adds, Cost expansions of $J$, and numerical bounds in AlphaGenesis measurement verdicts. Without commutativity of the underlying integer addition, none of those algebraic or constant-extraction developments typecheck on the PRC carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.