negate_congr_of_balanced
plain-language theorem explainer
Negation preserves the internal balance relation on signed orbits: if two orbits represent the same integer, so do their pointwise negations. Order and arithmetic lemmas on the PRC integer surface cite this congruence. The proof rewrites balance to equality of integer displays, then applies the identity that negation flips the sign of toInt.
Claim. Let $a,a'$ be signed orbits (pairs of distinction naturals interpreted as $\mathrm{pos}-\mathrm{neg}$). If $a$ and $a'$ are balanced in the sense $a.\mathrm{pos}+a'.\mathrm{neg}=a'.\mathrm{pos}+a.\mathrm{neg}$ (equivalently $a$ and $a'$ have the same integer display), then the pointwise negations (swap pos/neg) of $a$ and of $a'$ are likewise balanced.
background
In the Primitive Recognition Calculus, a signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, read as the formal difference $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; this is the internal PRC integer relation, defined entirely on $\delta$-orbit positions (K4.9).
The bridge to ordinary integers is the display map $\mathrm{toInt}$, and the characterization theorem states that balance holds if and only if the two orbits have equal $\mathrm{toInt}$ values. Pointwise negation swaps the two components; its display identity is $(\mathrm{negate},a).\mathrm{toInt}=-a.\mathrm{toInt}$.
This module builds the order surface on those signed orbits (reflexivity, transitivity, antisymmetry under balance, trichotomy, sign flags). Congruence of the arithmetic operations under balance is needed before the order certificate can close.
proof idea
Short rewrite proof. First replace the balance hypothesis and goal by equality of integer displays via the characterization $\mathrm{balanced}\leftrightarrow\mathrm{toInt}$ equality. Then rewrite both sides with the display law for negation, which sends each orbit to the negation of its $\mathrm{toInt}$. The hypothesis supplies $a.\mathrm{toInt}=a'.\mathrm{toInt}$, so the negated displays agree and balance is restored.
why it matters
This is the negation half of the congruence package for signed-orbit arithmetic. Downstream, subtraction congruence is obtained by unfolding subtraction as addition of a negation and applying addition congruence together with this lemma. Both feed the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed (nonnegativity displays, flag displays, truncated subtraction, absolute difference).
In the broader Recognition stack, signed orbits are the choice-free integer layer under ledger forcing and the primitive recognition calculus. Closing congruence and order here keeps the integer surface internal to $\delta$-orbit data rather than smuggling classical $\mathbb{Z}$ structure into the foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.