mk

Primitive Recognition Calculus builds integers before importing classical $\mathbb{Z}$. A signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, intended as the difference $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are identified when they are balanced-length equivalent (same integer value after cancellation).

PRC integers are defined as the quotient type of signed orbits by that setoid. The verifier map into classical $\mathbb{Z}$ is a separate lift; the quotient itself is native to the recognition layer. This constructor is the canonical injection of a concrete signed-orbit display into that quotient.

The surrounding K4.8 block also introduces zero and one as images of the zero and unit signed orbits, and proves that the integer display of a constructed class recovers the signed orbit's own integer display.

One-line definition: apply the quotient constructor for the signed-orbit setoid to the given signed orbit. No further lemmas or tactics; well-definedness of later maps (such as the lift to $\mathbb{Z}$) is handled at those definitions via the setoid's equivalence proof.

This is the entry point for K4.8 PRC integers: every concrete integer in the recognition layer is obtained by packaging a signed orbit and quotienting. Downstream siblings in the same block (integer display, zero, one, and equality of classes from balanced orbits) are written in terms of it. It sits under the broader program of reconstructing $\mathbb{Z}$ and $\mathbb{Q}$ from orbit arithmetic before classical number types are trusted as primitives, parallel to how rationals are later formed as ratio-orbit quotients. No forcing-chain landmark (T5–T8) is discharged here; the role is foundational bookkeeping for the integer layer of the calculus.