le_sub_self_right_iff
plain-language theorem explainer
For signed orbits, a non-strict inequality with right-hand side equal to a self-difference is equivalent to the same inequality against zero. Order-certificate and cancellation lemmas cite this when simplifying post-subtraction goals. The proof is a one-line term applying right-congruence of ≤ under balanced equality, using that a−a is balanced with zero.
Claim. For signed orbits $a$ and $b$, $b \le a-a$ if and only if $b \le 0$, where $\le$ is the internal signed-orbit order ($x \le y$ means $y-x$ is nonnegative) and $0$ is the zero signed orbit.
background
Signed orbits are the integer layer of the primitive recognition calculus: pairs (pos, neg) of distinction naturals, read as the difference pos − neg. Internal order is defined by nonnegativity of the difference: $a \le b$ means nonneg(b − a).
Two signed orbits are balanced when they represent the same integer (equal toInt). Order is insensitive to balanced replacement on either side. Upstream, right-congruence states that if $b$ is balanced with $b'$, then $a \le b$ iff $a \le b'$. Separately, self-subtraction is balanced with zero: $a-a$ is balanced with $0$.
The local module assembles the order surface on these signed orbits (reflexivity, totality, sign flags, and cancellation identities) before packaging it into a certificate.
proof idea
One-line term proof. Apply right-congruence of $\le$ under balanced equality to the pair $(a-a,,0)$, feeding the lemma that self-subtraction is balanced with zero. The biconditional is immediate; no case split on signs or nonnegativity flags is needed.
why it matters
Used by the integer-order certificate, which asserts that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, $\le$, abs-diff, and nonnegativity flags). This is foundation bookkeeping that builds integers from recognition distinctions, not a forcing-chain step (T0–T8). It closes a small algebraic identity so order goals after cancelling $a-a$ reduce cleanly to comparisons with zero, supporting the certificate's claim that the order API is complete.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.