toInt_mul'

PRC integers are quotient classes of signed orbits under the internal balanced-length relation. A signed orbit carries a positive and a negative orbit component; the verifier display sends such a pair to the ordinary integer difference of their natural lengths: $\mathrm{toInt}(z) = z_{\mathrm{pos}}^{\mathbb{N}} - z_{\mathrm{neg}}^{\mathbb{N}}$.

The module develops arithmetic on these quotient classes so that the display becomes a ring map into $\mathbb{Z}$. Multiplication on the quotient is induced from orbit-level operations already set up in the Orbit and OrbitArithmetic imports. Upstream, related recovery maps (LogicInt and forced-number embeddings) likewise land in $\mathbb{Z}$ by iteration or balanced-pair counts; here the same integer target is reached from the signed-orbit presentation.

One-line tactic proof: simp unfolds the quotient multiplication and the display definition on representatives, reducing both sides to the same integer product of length differences. No separate lemmas are invoked beyond the simp set already attached to the constructors and the display.

This is the multiplicative half of K4.8: the claim that the verifier display is a ring homomorphism from PRC integers into $\mathbb{Z}$. Together with the additive and unit cases in the same block, it certifies that integers recovered from primitive recognition calculus match ordinary integer arithmetic, not merely as a set bijection but as a ring. That alignment is foundation work for later forcing and mass-ladder constructions that treat $\mathbb{Z}$ as already forced from recognition structure rather than postulated. No downstream users are wired yet in the graph; the lemma sits as a local ring-homomorphism brick inside IntegerRational.