le_sub_zero_right_iff
plain-language theorem explainer
For signed orbits, right-hand subtraction of zero does not change the order: $b \le a-0$ if and only if $b \le a$. Anyone building the internal integer order on signed orbits cites this when normalizing differences. The proof is a one-line term application of right-congruence of $\le$ under balanced equality, using that $a-0$ is balanced with $a$.
Claim. For signed orbits $a,b$ (each a pair of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$), one has $b \le (a-0)$ if and only if $b \le a$, where $\le$ means the difference of the right operand minus the left is nonnegative.
background
Signed orbits are the internal integer carriers in the primitive recognition calculus: a structure with nonnegative distinction-natural components pos and neg, intended as the difference $\mathrm{pos}-\mathrm{neg}$. Their internal non-strict order is defined by nonnegativity of the difference: $a \le b$ means $\mathrm{sub},b,a$ is nonnegative.
Two signed orbits are balanced when they represent the same integer (equal toInt). Order is insensitive to balanced replacement on either side; the relevant upstream fact is right-congruence: if $b$ is balanced with $b'$, then $a \le b$ iff $a \le b'$. Separately, subtraction of zero is balanced with the original orbit: $\mathrm{sub},a,0$ is balanced with $a$, proved by reducing toInt and a trivial integer identity.
This module assembles the order surface (reflexivity, totality, trichotomy, sign flags) needed before the integer-order certificate can close.
proof idea
One-line term proof. Apply right-order congruence under balanced equality (le_congr_right_of_balanced) to the pair $(\mathrm{sub},a,0,,a)$, feeding the already-proved fact that $a-0$ is balanced with $a$ (sub_zero_balanced). No further case splits or toInt rewrites appear at this site; those live inside the two lemmas.
why it matters
Closes a normalization identity on the signed-orbit order: subtracting zero on the right is invisible to $\le$. Downstream it is consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas (truncated subtraction, nonnegativity flags, absolute difference) so later foundation layers can treat signed-orbit order as a finished integer order rather than an open interface.
In the Recognition stack this sits in the arithmetic-from-logic foundation beneath the forcing chain: before J-cost uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), or $D=3$ (T8) can be stated over integer carriers, the order on signed orbits must be stable under the zero-difference rewrite. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.