zero_toInt

In Primitive Recognition Calculus, integers are recovered from signed orbits: a pair of finite distinction-orbits (positive and negative legs). The verifier map sends a signed orbit $z$ to $\mathrm{toInt}(z) = z_{\mathrm{pos}}^{\mathbb{N}} - z_{\mathrm{neg}}^{\mathbb{N}}$ in $\mathbb{Z}$. The zero signed orbit is the balanced origin of that construction (both legs at the empty/zero distinction count).

The same recovery idea appears upstream as the LogicInt quotient map to ordinary integers; here the display is the concrete orbit-level version used throughout IntegerRational and IntegerOrder. Native unit and divisibility predicates on distinction-nats sit beside this layer but are not needed for the zero identity itself.

One-line reflexivity. Unfolding the zero constructor and the definition of toInt yields $0 - 0$ in $\mathbb{Z}$, which is definitionally $0$, so rfl closes the goal. Marked @[simp] for automatic rewriting.

This is the base case that lets every later bridge between signed-orbit structure and $\mathbb{Z}$ treat the origin correctly. Downstream it discharges the zero side of divisibility (dvdZ_zero: every signed orbit divides zero), the nonnegativity characterization of ratio-orbit order (zero_leQ_iff: $0 \le r$ iff the numerator integer is nonnegative), and the absolute-value/balance cluster in IntegerOrder (abs_eq_zero_iff_balanced_zero, the mul-zero variants, and the abs-sub-zero identities). Without $\mathrm{toInt}(0)=0$, those rewrites cannot collapse balanced-with-zero to integer zero. It is pure foundation scaffolding for the forced-integer layer, not a physics landmark (T5–T8), but it is the arithmetic zero that those later chains inherit.