mul_eq

PRC integers are the K4.8 construction: quotient of signed orbits by the internal balanced-length relation. The map into ordinary $\mathbb{Z}$ is a later display theorem, not part of the type itself.

This module builds integer and rational arithmetic inside Primitive Recognition Calculus before real completeness. Sibling material covers truncated subtraction, absolute difference, and the signed-orbit embedding into integers. Multiplication is introduced as an explicit operation on the quotient; the infix * is the usual Lean notation layer over that operation.

Upstream, the same pattern appears for rationals (ratio-orbit quotients identified by cross-multiplication). Continuity and completeness modules import the rational side; the integer side is the discrete base for that ladder.

One-line reflexivity. The instance that equips PRC integers with * is definitionally the named mul, so a * b = mul a b holds by rfl. Marked @[simp] so the tactic engine normalizes notation to the explicit map.

Bookkeeping for K4.8 integer arithmetic: keeps proofs that mention mul interchangeable with ordinary product syntax. No downstream dependents are recorded yet; the lemma is local infrastructure so later orbit-arithmetic and display theorems can rewrite freely.

In the broader Recognition stack this sits under the foundation layer that eventually feeds the forcing chain (T0–T8), but the lemma itself does not touch J-cost, $\varphi$, the eight-tick octave, or dimension forcing. It only stabilizes the discrete multiplicative structure on signed-orbit classes.