neg_eq
plain-language theorem explainer
Unary minus on PRC integers is definitionally the signed-orbit swap that exchanges positive and negative components. Anyone normalizing arithmetic on the K4.8 integer quotient will cite this simp rule. The proof is pure reflexivity: the Neg instance is wired to that swap.
Claim. For every PRC integer $a$ (a balanced-length quotient class of signed orbits), the notation $-a$ equals the pointwise negation of $a$, i.e. the class obtained by swapping the positive and negative orbit components.
background
In the Primitive Recognition Calculus, integers are not postulated as a primitive type. PRCInt is the quotient of signed orbits by the internal balanced-length relation (K4.8). A signed orbit carries a positive orbit display and a negative orbit display; the integer class is what remains after identifying balanced presentations.
Pointwise negation on a signed orbit is the swap of those two components. It is named negate at the orbit level to avoid clashing with structure fields, then lifted to the quotient. The standard unary-minus notation on PRCInt is installed so that it coincides with that lift.
This module sits in the foundation layer that builds integers and rationals from orbit arithmetic before any completeness or continuity results about reals.
proof idea
One-line definitional equality: rfl. The Neg instance on PRCInt is defined to be the quotient lift of orbit-level negate, so -a and negate a reduce to the same term. The @[simp] attribute exposes that identity to the simplifier.
why it matters
K4.8 constructs PRC integers as signed-orbit quotient classes; this lemma closes the notational gap between the structure-level swap and ordinary minus. Without it, every arithmetic identity that uses -a would have to mention the internal name explicitly. It is pure infrastructure for later integer and rational arithmetic in the same module (zero, absolute difference, order, and the display into ordinary $\mathbb{Z}$). No downstream consumers are recorded yet; the lemma is a local simp bridge rather than a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.