mul_comm

Distinction-orbit naturals are the inductive type with constructors zero and successor: the base-neutral finite orbit of repeated distinction (K2.12). Orbit arithmetic equips this type with addition and multiplication defined by the usual Peano recursion on the second argument, so the defining equations $a \cdot 0 = 0$ and $a \cdot S(b) = a \cdot b + a$ hold by reflexivity, as do the left-sided companions $0 \cdot a = 0$ and $S(a) \cdot b = a \cdot b + b$.

The module builds the arithmetic layer on top of the orbit type imported from PrimitiveRecognitionCalculus.Orbit, parallel to the Peano structure already forced for logic naturals (successor as one more generator application). A sibling commutativity result for the integer layer (PRCInt) proceeds by injection into Lean integers; here the argument stays internal to the orbit type.

Induct on the left factor $a$. In the zero case, rewrite with the left-zero and right-zero multiplication rules to obtain $0 = 0$. In the successor case, rewrite with the left-successor and right-successor multiplication rules, then apply the inductive hypothesis to equate the remaining products; the shared additive structure finishes the equality. No external lemmas beyond the four multiplication recursion identities are required.

Commutativity is the gate that lets orbit multiplication feed commutative algebraic structure higher in the stack. Downstream, CostAlgebra uses it inside the reciprocal automorphism (so the inverse map respects the product) and in the shifted-composition carriers that realize the doubled-product form of the Recognition Composition Law. PhiRing constructions on $\mathbb{Z}[\varphi]$ repeatedly invoke the same fact when normalizing products of integer coefficients. Causality bounds (neighbor-card sums) also rewrite products freely under this law. Within the foundation chain it is ordinary Peano bookkeeping, but without it the later J-cost and $\varphi$-ladder algebra cannot treat multiplication as symmetric.