PRCInt
plain-language theorem explainer
PRC integers are the quotient of signed orbits by the internal balanced-length equivalence. Anyone building arithmetic or the ℤ-display from the primitive recognition calculus cites this type. The definition is the bare quotient construction; injectivity of the integer display is proved later and carries the ring laws.
Claim. The type of PRC integers is the quotient of signed orbits by the balanced-length setoid: two signed orbits represent the same integer when they are equivalent under the internal balanced-length relation. The map into ordinary $\mathbb{Z}$ is a separate theorem, not part of this definition.
background
In the primitive recognition calculus, a signed orbit packages a pair of (positive and negative) orbit data. The balanced-length relation identifies signed orbits that differ only by equal increments on both sides, so the net count is invariant. That relation is packaged as a setoid on signed orbits.
This module sits in the foundation layer that reconstructs ordinary number systems from recognition primitives rather than importing $\mathbb{Z}$ as primitive. The quotient is the native carrier; the verifier display into Lean's $\mathbb{Z}$ is deferred so that arithmetic can be stated and proved on the quotient first.
Upstream, the setoid is exactly the equivalence of signed orbits under balanced length. Related scaffolding ties the ledger floor to the T0–T8 forcing chain, but that bridge is not required to form the quotient type itself.
proof idea
One-line definition: the type is the quotient of signed orbits by the signed-orbit setoid. No tactics or lemmas are applied at the definition site; subsequent constructors and the toInt display live in the PRCInt namespace.
why it matters
This is the K4.8 carrier for integer arithmetic internal to the recognition calculus. Downstream, pointwise addition of signed orbits descends to the quotient and yields associativity, commutativity, zero laws, and additive inverses, all proved by injectivity of the integer display. The same type underpins the Add instance and the equivalence with Lean's $\mathbb{Z}$.
In the broader Recognition Science stack, reconstructing $\mathbb{Z}$ from signed orbits keeps the number system on the same footing as the forcing chain (T0–T8) and the recognition composition law, rather than treating integers as an external import. The open task remains closing any remaining ledger-floor bridge into the T-chain; the quotient definition itself is already closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.