ofInt_one
plain-language theorem explainer
The integer embedding sends verifier 1 to the multiplicative unit of the PRC integers. Anyone normalizing PRCInt arithmetic or simp-closing unit identities will cite it. The proof is a two-step injectivity argument: push both sides through the toInt display and simplify.
Claim. The canonical embedding of the verifier integer $1$ into the PRC integers equals the multiplicative unit of that type: $\mathrm{ofInt}(1) = 1_{\mathrm{PRC}}$.
background
PRC integers (K4.8) are quotient classes of signed orbits under the internal balanced-length relation. The verifier display toInt lands in ordinary $\mathbb{Z}$; injectivity of that display is already proved, so equality of PRC integers may be checked after display.
The constructor ofInt builds a PRC integer from a verifier Int by routing the positive and negative parts through the $\delta$-orbit (DistinctionNat of the absolute values). The unit one is the multiplicative identity in this quotient type. The surrounding module develops the integer and rational layers of the Primitive Recognition Calculus on top of orbit arithmetic.
proof idea
Apply injectivity of the toInt display to reduce the goal to an equality in $\mathbb{Z}$. A single simp then closes both sides: toInt (ofInt 1) and toInt one both reduce to the verifier integer 1. No case analysis on the quotient is needed once injectivity is in hand.
why it matters
This is a basic simp lemma in the K4.8 PRC-integer layer: it pins the embedding of the unit so later arithmetic (products, rung displays, forced-integer bridges) can cancel or normalize without unfolding the signed-orbit constructor. It sits beside the zero embedding and the injectivity theorem for the verifier display. No downstream users are recorded yet; the lemma is infrastructure for ring-structure instances and for matching PRC integers against ordinary $\mathbb{Z}$ in the UniversalForcing forced-integers path. It does not itself touch the T0–T8 forcing chain, but it keeps the integer layer of the recognition calculus coherent with verifier arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.