ofInt_mul
plain-language theorem explainer
The embedding of classical integers into primitive recognition calculus (PRC) integers is a multiplicative homomorphism. Anyone simplifying PRC integer algebra or orbit-arithmetic expressions cites this simp lemma. The proof applies injectivity of the classical display map and closes by simplification on both sides.
Claim. For all $m,n\in\mathbb{Z}$, the PRC embedding of the product equals the PRC product of the embeddings: the image of $m\cdot n$ is the product of the images of $m$ and $n$.
background
Primitive recognition calculus (PRC) integers are signed $\delta$-orbits built from distinction naturals. The embedding from verifier $\mathbb{Z}$ routes the positive part $n.\mathrm{toNat}$ and the negative part $(-n).\mathrm{toNat}$ each through $\mathrm{DistinctionNat.ofNat}$, then packages them as a signed orbit.
A classical display map sends each PRC integer back to $\mathbb{Z}$. Upstream result K4.8 states that this display is injective: distinct PRC integers have distinct verifier displays. Equality of PRC integers may therefore be checked after projecting to $\mathbb{Z}$.
The surrounding module develops the integer/rational layer of PRC on top of Orbit and OrbitArithmetic, inside the Foundation stack.
proof idea
Apply injectivity of the classical display map. It then suffices that both sides display to the same integer. A single simp reduces the displays of the embedded product and of the PRC product of embeddings to the ordinary product $m*n$ in $\mathbb{Z}$, using the definitions of the embedding, PRC multiplication, and the display.
why it matters
This is basic ring-homomorphism infrastructure for the PRC integer layer: products of embedded integers normalize under simp. It sits in Foundation.PrimitiveRecognitionCalculus.IntegerRational and supports orbit arithmetic and rung bookkeeping that the broader forcing chain (T0–T8, RCL, $\phi$-ladder) eventually consumes. No recorded downstream theorems yet; the lemma is foundation plumbing rather than a paper-level proposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.