instZero
plain-language theorem explainer
Equips PRC integers (signed-orbit quotient classes) with a canonical zero element via Lean's Zero typeclass. Anyone building additive structure, displays into ℤ, or arithmetic lemmas on these classes will cite it. The body is a one-line instance packaging the existing zero constructor.
Claim. The type of PRC integers (quotient of signed orbits by the balanced-length relation) carries a distinguished zero element, namely the class of the zero signed orbit.
background
Primitive Recognition Calculus (PRC) builds integers internally before any external map to classical $\mathbb{Z}$. The carrier PRCInt is the quotient of signed orbits by the internal balanced-length setoid: two signed orbit displays represent the same integer when their balanced lengths agree. The verifier display into $\mathbb{Z}$ is a later theorem, not part of the type definition.
In this module the zero element is already constructed as a named signed-orbit class. The present declaration only registers that class as the typeclass zero, so notation and generic additive lemmas can see it. Related siblings include the signed-orbit constructor, the map to integers, and the lemma that zero displays as $0$.
proof idea
One-line instance: the Zero structure is inhabited by the already-defined zero signed-orbit class. No tactics, no lemmas, no proof obligations beyond the constructor.
why it matters
K4.8 in the foundation layer treats integers as recognition-native quotient data rather than imported classical integers. A Zero instance is the first piece of additive structure on that carrier: without it, sums, differences, and the later display theorems cannot use standard zero notation or typeclass-driven arithmetic.
No downstream theorems currently list this instance as a direct edge, but every additive lemma and the integer display path in the same module presuppose it. It sits upstream of the rational construction (ratio-orbit quotients) only indirectly, by stabilizing the integer layer the rationals build on. It does not itself touch the forcing chain T0–T8, the J-cost, or the mass ladder; it is pure carrier infrastructure for the PRC number system.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.