negate
plain-language theorem explainer
Pointwise negation on signed orbits swaps the two distinction counts, so a pair meant as pos minus neg becomes its additive inverse. Anyone proving order, absolute value, or ratio comparison facts on PRC integers cites it. The body is a pure field swap, deliberately named to avoid clashing with the structure field.
Claim. Given a signed orbit $a=(p,n)$ of distinction naturals (intended value $p-n$), its negation is the signed orbit $(n,p)$.
background
In the primitive recognition calculus, a SignedOrbit is a pair of distinction naturals (pos, neg) whose intended meaning is the integer difference pos minus neg (K4.6). This is the PRC-native stand-in for integers before quotienting by balanced equivalence.
The same swap pattern already appears upstream in IntegersFromLogic.neg, where negation on logic integers is -(a,b)=(b,a), and in DeltaReal.neg for protocol intervals. Here the operation is kept at the representative level so later lemmas can transport it across balanced equivalence and the toInt display map.
The module builds integer and rational structure from orbit arithmetic; negation is the first signed unary operation needed for order, absolute value, and ratio comparisons.
proof idea
Definitional one-liner: construct a new SignedOrbit whose pos field is the input's neg and whose neg field is the input's pos. No lemmas are applied; the name negate is chosen only to avoid shadowing the structure field neg.
why it matters
This is the primitive that makes signed orbit arithmetic closed under additive inverse. Downstream order theory uses it heavily: abs_negate shows absolute value is invariant under negation; abs_le_iff_between and abs_le_of_between characterize |z| ≤ n as lying between -n and n; balanced_negate_iff and related balanced-zero criteria track equivalence after sign flip. Ratio growth facts such as leQ_neg_neg_iff reverse inequalities under double negation of ratio orbits. Without this swap, the PRC integer order and absolute-value layer cannot state the usual trichotomy and sandwich lemmas that feed later forcing and ladder comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.