equivInt
plain-language theorem explainer
The PRC integer type, formed as the signed-orbit quotient by balanced length, is definitionally equivalent to ordinary verifier integers. Anyone citing K4.8 recovery of ℤ from primitive recognition structure uses this carrier equivalence. The definition simply packages the already-proved forward and inverse maps and their round-trip identities into a single type equivalence.
Claim. There is a type equivalence between the PRC integer quotient (signed orbits modulo the internal balanced-length relation) and ordinary integers $\mathbb{Z}$. The forward map sends a class to the difference of its positive and negative natural lengths; the inverse rebuilds a signed orbit from the positive and negative parts of an integer. The two maps are mutual inverses on the nose.
background
In the Primitive Recognition Calculus, a signed orbit pairs a positive distinction-length with a negative one. The display map sends such a pair to the ordinary integer equal to (positive length) minus (negative length). PRC integers are the quotient of signed orbits by the internal balanced-length setoid: two displays represent the same integer when they differ only by balanced padding.
The inverse construction routes a verifier integer through the δ-orbit: non-negative and negative parts become distinction-naturals that rebuild a signed orbit class. The module's local claim (K4.8) is that this quotient surface is not an assumption of ℤ but a structure that reproduces it.
Upstream, the same pattern appears for LogicInt in IntegersFromLogic: a recovery equivalence built from toInt/fromInt and the two round-trip lemmas. Here the carrier is the PRC quotient rather than the logic-integer quotient, but the packaging is parallel.
proof idea
Definitional packaging, not a tactic proof. The forward function is the existing display of a PRC integer into ℤ; the inverse is the existing constructor from a verifier integer through the δ-orbit. Left-inverse is the already-proved identity that rebuilding from the display recovers the original class; right-inverse is the dual identity that displaying the rebuild recovers the original integer. No new algebra is performed at this site.
why it matters
K4.8 asserts that the PRC integer surface is literally isomorphic to verifier ℤ, so ordinary integers are a downstream display rather than a primitive assumption. This equivalence is the carrier form of that claim: once the round-trips are in hand, the type equivalence is the clean citation object.
Downstream it is consumed by the first-pass kernel certificate (K7/A2), which needs a inhabited judgment surface and related kernel witnesses, and it parallels the LogicInt recovery equivalence in IntegersFromLogic. In the broader forcing chain it sits in the foundation layer that must recover discrete arithmetic before later steps (T5–T8, mass ladder, constants) can speak in ordinary integer language without smuggling ℤ in as an axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.