toInt_one'
plain-language theorem explainer
The multiplicative unit of the PRC integers displays as the ordinary integer 1 under the signed-orbit verifier map. Anyone checking that recognition-calculus integers recover classical ℤ cites this identity. The proof is a one-line simplification of the unit constructor and the display definition.
Claim. If $1$ denotes the multiplicative unit in the PRC integers (signed-orbit quotient classes), then its verifier display into $\mathbb{Z}$ equals $1$.
background
PRC integers are quotient classes of signed orbits under the internal balanced-length relation. A signed orbit carries a positive and a negative orbit component; the verifier display sends such a pair to the difference of their natural-number lengths in $\mathbb{Z}$, namely $(\mathrm{pos}.\mathrm{toNat}:\mathbb{Z})-(\mathrm{neg}.\mathrm{toNat}:\mathbb{Z})$.
The surrounding module (K4.8) builds integer and rational structure inside Primitive Recognition Calculus from these orbit displays. A parallel recovery map $\mathrm{LogicInt}\to\mathbb{Z}$ appears upstream in IntegersFromLogic; here the same idea is realized on signed orbits before the quotient is taken, then lifted to the quotient type.
The next section of the module turns to ratio orbits and cross-multiplication, so the unit and zero display lemmas sit at the boundary between integer and rational constructions.
proof idea
One-line tactic proof: simp. Unfolding the definition of the unit as a PRC integer and the quotient-level display map reduces both sides to the same concrete integer expression, which simplification closes immediately. No intermediate lemmas are invoked by name.
why it matters
Doc-comment labels this K4.8: the toInt display preserves one. Together with the sibling zero-display lemma it anchors the claim that PRC integers recover classical $\mathbb{Z}$ at the multiplicative and additive units. That recovery is a prerequisite for treating ratio orbits (numerator over nonzero orbit denominator) as genuine rationals later in the same module.
No downstream consumers are recorded yet. In the broader Recognition framework this is foundation-layer arithmetic scaffolding: integers forced from orbit logic, not yet the forcing chain T5–T8 or the mass ladder, but the substrate those later steps assume when they count ticks, rungs, and gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.