zero_eq

Primitive Recognition Calculus builds integers internally before any appeal to classical $\mathbb{Z}$. The type PRCInt is the quotient of signed orbits by the balanced-length setoid: two signed orbit displays represent the same integer when their internal lengths balance. The verifier map into classical $\mathbb{Z}$ is a later theorem, not part of the construction.

Within that namespace a named constant zero is the distinguished neutral class, and Lean also supplies the numeral 0 via OfNat. This declaration records that those two presentations are identical, so simp and rewriting can treat them interchangeably when doing orbit-level integer arithmetic.

One-line rfl. The OfNat instance for the PRC integer type is defined to be exactly the named zero constructor, so the equality holds by definitional reduction with no lemmas required.

K4.8 of the Primitive Recognition Calculus layer introduces integers as signed-orbit quotients so that later arithmetic (rationals, completeness, continuity of real multiplication and products) never smuggles in classical $\mathbb{Z}$ prematurely. A clean simp fact that numeral zero is the named zero keeps that arithmetic free of spurious case splits and keeps displays aligned with the internal neutral class.

No downstream theorems currently depend on this edge in the graph; it is infrastructure for local simplification inside the IntegerRational module and any later proofs that rewrite PRC integer expressions. It does not itself touch the forcing chain (T0–T8), the Recognition Composition Law, or the mass ladder; it only keeps the integer layer tidy.