toInt_injective
plain-language theorem explainer
The verifier display from PRC integers into ℤ is injective: equal displays force equal quotient classes of signed orbits. Ring-law proofs for PRC integers cite it constantly, transporting ℤ identities back across the display. The argument is double Quot.ind plus Quot.sound via the balanced-orbit characterization of equal displays.
Claim. The verifier display map sending each PRC integer (a quotient class of signed $\delta$-orbits) to an element of $\mathbb{Z}$ is injective: if two PRC integers have the same integer display, then they are equal.
background
In the Primitive Recognition Calculus, a signed orbit pairs a positive and a negative $\delta$-orbit length. Its verifier display is the ordinary integer difference of those lengths: $\mathrm{toInt}(z) = z_{\mathrm{pos}} - z_{\mathrm{neg}}$ in $\mathbb{Z}$.
Two signed orbits are balanced when $a_{\mathrm{pos}} + b_{\mathrm{neg}} = b_{\mathrm{pos}} + a_{\mathrm{neg}}$. That relation is the setoid used to form PRC integers as a quotient. An upstream lemma records the exact match: signed orbits are equivalent under balance if and only if their displays agree in $\mathbb{Z}$.
The present statement lifts that characterization from representatives to the quotient: the induced display on PRC integers separates points. The module sits in the foundation layer that rebuilds $\mathbb{Z}$ and $\mathbb{Q}$ from recognition data rather than assuming them as primitives.
proof idea
Term-mode proof by double quotient induction. Fix $a,b$ in the PRC-integer quotient with equal displays. Apply Quot.ind to both, reducing to representatives. On representatives, the reverse direction of signedOrbitEquiv_iff_toInt_eq turns equal displays into balanced equivalence. Quot.sound then identifies the two classes. No arithmetic on $\mathbb{Z}$ is needed beyond that equivalence.
why it matters
This injectivity is the transport hinge for the entire PRC integer ring. Downstream lemmas add_assoc, add_comm, add_zero, add_negate, mul_assoc, mul_comm, mul_one, and left_distrib all open with apply toInt_injective and finish by simplifying the corresponding $\mathbb{Z}$ identity. Without it, ring laws would have to be proved by hand on balanced representatives.
Doc label K4.8 places the result in the integer-display block of the foundation chain: distinct PRC integers must carry distinct verifier displays before arithmetic can be forced from recognition structure. It is pure scaffolding for the later forcing of $\mathbb{Z}$ and $\mathbb{Q}$ inside Recognition Science, not a physics claim itself, but every later mass or constant identity that quotes PRC arithmetic inherits this separation property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.