toInt_zero'
plain-language theorem explainer
The zero class of the signed-orbit quotient (PRC integers) maps to ordinary integer zero under the verifier display. Anyone assembling the integer homomorphism from recognition orbits cites this as the additive unit case. The proof is a one-line simplification of the zero constructor and the difference-of-lengths display.
Claim. If $0$ denotes the zero class in the signed-orbit quotient of primitive-recognition integers, then its verifier display into $\mathbb{Z}$ equals $0$.
background
In the Primitive Recognition Calculus, integers are not postulated: they arise as quotient classes of signed orbits. A signed orbit pairs a positive orbit length with a negative one; two pairs are identified when their balanced lengths agree. The type of such classes is the PRC integer type.
The verifier display sends a signed orbit to an ordinary integer by subtracting the two natural lengths: $\mathrm{toInt}(z) = z_{+} - z_{-}$ in $\mathbb{Z}$. On the quotient this becomes a well-defined map from PRC integers into $\mathbb{Z}$. The zero class is the class of the balanced empty (or equal-length) pair.
Upstream, the same recovery pattern appears for logic integers and forced naturals: each has a toInt that reads off an iteration or length count. Here the display is the signed difference of two such counts.
proof idea
One-line tactic proof: simp unfolds the zero constructor of the PRC integer type and the definition of the verifier display on a signed orbit (difference of the two toNat lengths). Both sides reduce to the integer literal $0$.
why it matters
Labeled K4.8 in the module: the display must preserve zero before it can be a ring (or even monoid) homomorphism from recognition integers into $\mathbb{Z}$. Together with the companion one-preservation fact, it anchors the claim that the signed-orbit quotient really recovers classical integers rather than a parallel copy with a shifted unit.
No downstream dependents are wired yet in the graph, so this is presently a leaf of the K4.8 integer package. In the broader Recognition foundation it sits under the forcing of discrete arithmetic from orbit structure, parallel to the Integers-from-Logic and Forced-Integers recovery maps. It does not itself touch the T5–T8 chain (J-cost, $\varphi$, eight-tick, $D=3$), but supplies the additive unit case those later layers assume when they count on $\mathbb{Z}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.