mul_comm
plain-language theorem explainer
Multiplication on recognition-native integers (signed-orbit quotient classes) is commutative. Anyone assembling a CommRing or monoid instance on PRCInt, or transporting products into CostAlgebra and PhiRing, cites this. The proof is a two-line reduction: injectivity of the integer display plus Mathlib's Int.mul_comm.
Claim. For all recognition-native integers $a,b$ (quotient classes of signed orbits under the balanced-length relation), the product satisfies $a\cdot b=b\cdot a$.
background
PRC integers are the quotient Quot signedOrbitSetoid: signed orbits identified by the internal balanced-length relation. The map toInt is the verifier display into ordinary $\mathbb{Z}$; injectivity of that display is the standard way to transfer algebraic identities from $\mathbb{Z}$ back to the quotient.
Multiplication on signed orbits is defined so that it intertwines with ordinary integer multiplication: (mul a b).toInt = a.toInt * b.toInt (the companion lemma mul_toInt). The same pattern already appears one level down for logic naturals via the recovery theorem toNat_mul.
This module sits in the Primitive Recognition Calculus foundation: integers and rationals are built from orbit arithmetic before any classical choice is used for the rational field bridge.
proof idea
Apply injectivity of the integer display toInt on PRCInt. After that, the goal is an equality in $\mathbb{Z}$. Simplify using Mathlib's Int.mul_comm (and the intertwining of PRC multiplication with toInt, which simp picks up). No induction or case split is needed.
why it matters
Commutativity is the missing monoid axiom that lets PRCInt support the ring and monoid instances consumed upstream of the cost algebra and the $\varphi$-ring. Downstream, CostAlgebra's reciprocal automorphism and the shifted-composition carriers invoke mul_comm when proving that products and inverses are well-defined on positive carriers. PhiRing's PhiInt (pairs $a+b\varphi$) repeatedly uses integer commutativity when multiplying coefficients. In the Recognition chain this is pure scaffolding for later J-cost and RCL algebra, not a forcing step (T5–T8), but without it the native integer layer cannot host those structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.