toInt_ofInt
plain-language theorem explainer
Converting a verifier integer into a PRC signed orbit and reading it back recovers the original integer. Anyone building the PRC≃ℤ equivalence cites this as the right inverse. The proof unfolds the positive/negative δ-orbit embedding, cancels ofNat/toNat, and finishes by integer arithmetic (omega).
Claim. For every integer $n\in\mathbb{Z}$, if one embeds $n$ as a PRC integer by sending the nonnegative part $n_{\mathrm{toNat}}$ and the nonnegative part of $-n$ through the distinction orbit, then the signed display $(\mathrm{pos}-\mathrm{neg})$ equals $n$ again.
background
In the Primitive Recognition Calculus, integers are not primitive. A signed orbit is a pair of distinction orbits (finite base-neutral chains of repeated distinction, DistinctionNat), interpreted as positive and negative parts. The display map sends such a pair to the verifier integer $(\mathrm{pos.toNat}:\mathbb{Z})-(\mathrm{neg.toNat}:\mathbb{Z})$.
The reverse embedding routes a verifier $n$ through the δ-orbit: nonnegative $n$ contributes to the positive slot via ofNat n.toNat, and $-n$ contributes to the negative slot the same way. Upstream, DistinctionNat.toNat_ofNat says that building an orbit from a natural and reading the iteration count recovers that natural. The module sits in the foundation layer that reconstructs arithmetic surfaces from recognition structure rather than assuming $\mathbb{Z}$.
proof idea
Term-mode proof after a show that expands both maps: the claim becomes
$((\mathrm{ofNat},n.\mathrm{toNat}).\mathrm{toNat}:\mathbb{Z})-((\mathrm{ofNat},(-n).\mathrm{toNat}).\mathrm{toNat}:\mathbb{Z})=n$.
Two rewrites by DistinctionNat.toNat_ofNat erase the orbit round-trip on each side, leaving the elementary identity $n.\mathrm{toNat}-(-n).\mathrm{toNat}=n$, which omega discharges for all signs of $n$.
why it matters
This is the right-inverse half of K4.8: the PRC integer surface is literally isomorphic to verifier $\mathbb{Z}$. Downstream, equivInt packages toInt/ofInt with this lemma as right_inv and ofInt_toInt as left_inv, so the verifier integers are a display the PRC quotient reproduces, not an assumption. The sibling ofInt_toInt reduces injectivity of the display to this identity. In the broader forcing chain this is pure foundation scaffolding (arithmetic from recognition orbits), not yet T5–T8 physics, but it locks the integer layer those later steps sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.