ofInt_toInt
plain-language theorem explainer
For every PRC integer a, rebuilding from its verifier display recovers a: ofInt(toInt a) = a. Anyone citing the K4.8 isomorphism PRCInt ≃ ℤ needs this as the left inverse. The proof is a short injectivity argument: apply injectivity of toInt and rewrite by the already-proved right inverse toInt ∘ ofInt = id.
Claim. For every PRC integer $a$ (a class in the signed-orbit quotient), $\mathrm{ofInt}(\mathrm{toInt}(a)) = a$. Equivalently, reconstructing a PRC integer from its verifier integer display is the identity on the quotient.
background
In the Primitive Recognition Calculus, integers are not imported as a primitive. PRCInt is the quotient of signed orbits by the internal balanced-length relation: each class is a pair of distinction-nat orbits (positive and negative parts) modulo that setoid. The verifier map toInt sends a signed orbit to $(n_+ : \mathbb{Z}) - (n_- : \mathbb{Z})$ and descends to the quotient.
The reverse map ofInt builds a PRC integer from a verifier ℤ by routing the positive and negative parts through the δ-orbit constructor. Upstream, toInt_ofInt already shows the right inverse on ℤ, and toInt_injective records that distinct quotient classes have distinct verifier displays. The local K4.8 claim is that the PRC surface reproduces verifier integers rather than assuming them.
proof idea
Short tactic proof. Apply injectivity of the display toInt to reduce the goal ofInt(toInt a) = a to equality after toInt. Rewrite with the right-inverse lemma toInt_ofInt, which gives toInt(ofInt n) = n for every verifier integer n, and the two sides match. No induction on the quotient is needed at this step because injectivity already absorbs the class structure.
why it matters
This is the left inverse half of K4.8: the PRC integer surface is literally isomorphic to verifier ℤ. Downstream, equivInt packages toInt and ofInt into an equivalence PRCInt ≃ ℤ with left_inv := ofInt_toInt and right_inv := toInt_ofInt. The doc-comment states the philosophical point: verifier ℤ is not assumed; it is a downstream display the PRC quotient happens to reproduce.
In the Recognition foundation stack this closes the integer layer of the primitive recognition calculus before rationals and further arithmetic structure are built on the same orbit surface. It sits under the Integers-from-logic recovery story and supports later claims that classical number types appear as displays of recognition quotients rather than as axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.