ofInt
plain-language theorem explainer
Embeds a verifier integer into the PRC integer type by splitting it into nonnegative and nonpositive natural parts and routing each through the finite distinction orbit. Anyone proving the PRC≃ℤ surface isomorphism or the simp lemmas for add, mul, and negate cites this map as the inverse display. The body is a one-line constructor into the signed-orbit quotient.
Claim. For any $n \in \mathbb{Z}$, form the PRC integer whose positive orbit is the distinction-orbit of $n$ as a natural number and whose negative orbit is the distinction-orbit of $-n$ as a natural number (so one side is zero when $n$ has definite sign).
background
In the Primitive Recognition Calculus, integers are not assumed from the verifier. They are rebuilt as quotient classes of signed orbits. A signed orbit pairs two finite distinction orbits (the inductive type of repeated distinction steps, with zero and successor). The quotient identifies pairs that differ by a balanced-length relation; the resulting type is the PRC integer surface.
The distinction orbit carries the usual bridge to verifier naturals: ofNat builds an orbit by iterating successor, and toNat reads the iteration count back. The present map lifts that bridge to integers by applying it separately to the positive and negative parts of $n$ (via Lean's toNat on $n$ and on $-n$), then packaging the pair as a signed-orbit class.
Local setting is K4.8 of the foundation layer: arithmetic reconstructed from recognition orbits rather than imported from classical $\mathbb{Z}$.
proof idea
Definitional one-liner. Read $n$ and $-n$ as naturals, embed each via the distinction-orbit constructor from a verifier Nat, form the signed-orbit pair, and pass it to the PRC integer constructor (the quotient class of that pair). No lemmas are applied; the body is pure data construction.
why it matters
This is the inverse leg of the K4.8 surface isomorphism: the PRC integer type is literally equivalent to verifier $\mathbb{Z}$, so classical integers are a downstream display the quotient happens to reproduce, not an assumption. Downstream, equivInt sets invFun to this map, and the round-trip theorems (ofInt_toInt, toInt_ofInt) discharge the equivalence laws.
It also anchors the simp suite that shows the embedding is a ring homomorphism on the nose: add, mul, negate, zero, and one all commute with the map. Those lemmas let later arithmetic and rung constructions treat PRC integers as interchangeable with ordinary integers while keeping the recognition origin explicit. In the broader forcing chain this sits under foundation reconstruction of number from distinction, before mass ladders and constants are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.