negate_respects_balanced
plain-language theorem explainer
Negation of signed orbits preserves the balanced equivalence relation: if two signed orbits represent the same integer difference, so do their pointwise swaps of positive and negative legs. Anyone constructing PRC integers as a quotient of signed orbits needs this to lift negation through the quotient. The proof rewrites balance as equality of integer displays and applies the fact that negation flips the sign of that display.
Claim. If $a_1, a_2$ are signed orbits (pairs of distinction-orbit lengths interpreted as $\mathrm{pos}-\mathrm{neg}$) and $a_1$ is balanced with $a_2$ (i.e. $a_1.\mathrm{pos}+a_2.\mathrm{neg}=a_2.\mathrm{pos}+a_1.\mathrm{neg}$), then the pointwise negations $\mathrm{swap}(a_1)$ and $\mathrm{swap}(a_2)$ are likewise balanced.
background
In the Primitive Recognition Calculus, integers are built from signed orbits: a structure SignedOrbit holding two distinction-orbit lengths pos and neg, with intended meaning $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are related by the internal equivalence balanced when their orbit lengths cross-sum equal: $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That relation is the kernel of the quotient that yields PRC integers.
Pointwise negation on a signed orbit swaps the two legs. The bridge lemma balanced_iff_toInt_eq identifies balance with equality of the conservative integer display toInt (the difference of the two natural lengths as elements of $\mathbb{Z}$). A companion computation negate_toInt records that swapping legs sends that display to its additive inverse.
The local module constructs PRC integers and rationals from these orbit-level primitives, staying inside the forcing chain that begins from primitive distinction rather than assuming classical $\mathbb{Z}$ as given.
proof idea
Short rewrite proof. First replace every occurrence of balanced by equality of toInt via balanced_iff_toInt_eq. The goal becomes $(\mathrm{negate},a_1).\mathrm{toInt}=(\mathrm{negate},a_2).\mathrm{toInt}$. Apply negate_toInt on each side to obtain $-a_1.\mathrm{toInt}=-a_2.\mathrm{toInt}$, then finish by the rewritten hypothesis $a_1.\mathrm{toInt}=a_2.\mathrm{toInt}$. No case splits or induction.
why it matters
This private lemma is the well-definedness obligation for lifting signed-orbit negation to the quotient type of PRC integers. Immediately below it, PRCInt.negate is defined by Quot.lift of the pointwise swap, and the soundness argument is exactly negate_respects_balanced. Without it, additive inverse on PRC integers would not descend from the orbit representatives.
In the Recognition framework this sits in the foundation layer that rebuilds integer arithmetic from distinction orbits (K4.6–K4.9), upstream of the forcing chain landmarks T5–T8. It is pure structural bookkeeping: once balance is the integer kernel and negation flips the display, the quotient inverse is forced. Downstream consumers of PRC integer arithmetic inherit a choice-free negation that matches the classical $-n$ on the verifier display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.