sub_balanced_zero_iff_of_balanced_right
plain-language theorem explainer
If two signed orbits are balanced (equivalent under the PRC integer relation), then subtracting either from a fixed orbit yields zero under balance if and only if the other does. Order and certificate authors cite this to show that vanishing of a difference is well-defined on equivalence classes of the right operand. The proof is a one-line specialization of the general right-input balance transport lemma at the zero orbit.
Claim. Let $a,b,b'$ be signed orbits (pairs of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$). If $b$ and $b'$ are balanced, i.e. $b.\mathrm{pos}+b'.\mathrm{neg}=b'.\mathrm{pos}+b.\mathrm{neg}$, then $\mathrm{sub}(a,b)$ is balanced with the zero orbit if and only if $\mathrm{sub}(a,b')$ is balanced with the zero orbit.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, intended as the difference $\mathrm{pos}-\mathrm{neg}$. Two signed orbits $a,b$ are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; the module doc for this relation calls it the internal PRC integer equivalence, defined entirely on $\delta$-orbit positions.
Subtraction of signed orbits is the natural difference operation on those pairs. Balance with the zero orbit is the internal notion of vanishing: $\mathrm{sub}(a,b)$ balanced with zero means $a$ and $b$ represent the same integer class.
The local module builds the order surface on these signed orbits (reflexivity, transitivity, antisymmetry under balance, trichotomy, sign flags). Upstream, the general transport lemma states that if $b$ and $b'$ are balanced, then for any third orbit $c$, $\mathrm{sub}(a,b)$ is balanced with $c$ iff $\mathrm{sub}(a,b')$ is balanced with $c$, proved by rewriting through the integer interpretation of balance and subtraction.
proof idea
One-line term wrapper. Instantiate the general right-input transport theorem balanced_sub_right_input_iff_of_balanced at $c$ equal to the zero signed orbit, feeding the given balance hypothesis on $b$ and $b'$. No extra rewriting is needed; the zero case is pure specialization.
why it matters
Vanishing of differences must be independent of which balanced representative is chosen on the right. This lemma records that invariance for the zero target and is the positive half of the well-definedness package used by the order surface.
It is applied directly by the negated companion (sub_not_balanced_zero_iff_of_balanced_right), which rewrites through this biconditional, and sits in the dependency cone of integer_order_certificate, whose doc states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, $\leq$, absolute difference, and nonnegativity flags on signed orbits.
In the broader Recognition foundation, signed-orbit integers are the discrete carrier beneath ledger forcing and the forcing chain; a stable zero test under balance is a prerequisite for any later comparison or rung arithmetic that treats orbits up to the K4.9 relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.