instNeg
plain-language theorem explainer
Equips PRC integers with additive inversion by packaging signed-orbit negation (swap of positive and negative orbit legs) as the standard Neg instance. Anyone building the PRC integer group or ring structure cites this. The body is a one-line instance wiring of the existing pointwise negate map on representatives.
Claim. The type of PRC integers (quotient of signed orbits by the balanced-length relation) carries a negation operation $-\,\cdot\,$, induced on representatives by swapping the positive and negative orbit components.
background
In the Primitive Recognition Calculus, integers are not postulated as $\mathbb{Z}$. They arise as quotient classes of signed orbits: each representative is a pair of ordinary orbits (positive leg, negative leg), and two pairs are identified when their balanced lengths match. The type PRCInt is that quotient; a later verifier map into classical $\mathbb{Z}$ is a downstream theorem, not part of the definition.
Pointwise negation on signed orbits is already defined: swap the two legs. That map is named separately from the typeclass field to avoid a name clash. The present declaration simply installs that map as the canonical additive inverse on the quotient type, so ordinary notation and the Neg API become available in the PRC integer layer.
The surrounding module also builds rationals as ratio-orbit quotients and the usual arithmetic scaffolding (order, absolute difference, truncation). Negation is the first step toward a full additive group structure on the integer quotient.
proof idea
One-line instance: the Neg structure on PRC integers is inhabited by the already-defined pointwise negate map on signed-orbit representatives. No separate well-definedness proof appears in this declaration; the instance assumes (or inherits from the surrounding development) that swapping legs respects the balanced-length setoid, so it descends to the quotient.
why it matters
Recognition Science rebuilds number systems from recognition orbits before classical $\mathbb{Z}$ is available as a primitive. Installing negation on PRC integers is infrastructure for the integer and rational layers (K4.8) that later feed real completeness and continuity results in the same foundation stack.
No downstream theorem currently lists this instance as a direct edge, but every use of unary minus, additive inverse laws, or ring axioms on PRC integers depends on it. It does not itself touch the forcing chain (T5–T8), the Recognition Composition Law, or physical constants; it is pure algebraic scaffolding under those later claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.