lt_sub_zero_right_iff
plain-language theorem explainer
Strict order on signed orbits is invariant under right-hand subtraction of zero: b < a−0 iff b < a. Anyone discharging order goals after canceling zero, or assembling the integer-order certificate, cites this. The proof is a one-line term applying right-congruence of strict order under the balanced relation, using that a−0 is balanced with a.
Claim. For signed orbits $a$ and $b$, $b < (a - 0)$ if and only if $b < a$, where $<$ is the internal strict order (nonnegative difference that is not balanced) and $0$ is the zero signed orbit.
background
In the Primitive Recognition Calculus, integers are carried by SignedOrbit: a pair of distinction-nats (pos, neg) with intended meaning pos − neg. Two signed orbits are balanced when they represent the same integer (equal toInt). The internal strict order is defined as nonnegative difference together with failure of balance: $a < b$ means $a \le b$ and not balanced$(a,b)$.
Subtraction of the zero orbit is not definitionally the identity on the pair representation, but it is balanced-equivalent to the original orbit. The sibling lemma sub_zero_balanced records exactly that: sub a zero is balanced with $a$, proved by reducing both sides through toInt and a trivial integer identity.
Right-congruence of strict order under balance is already available: if $b$ is balanced with $b'$, then $a < b$ iff $a < b'$. That is the only nontrivial order fact needed here.
proof idea
One-line term proof. Instantiate right-congruence of strict order under balance (lt_congr_right_of_balanced) at the pair $(b,,\mathrm{sub},a,0,,a)$, feeding the hypothesis that $\mathrm{sub},a,0$ is balanced with $a$ (sub_zero_balanced a). The biconditional falls out immediately; no case split or toInt rewriting is done at this site.
why it matters
This is a small cancellation law in the signed-orbit order surface. It feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed: the certificate packages display lemmas for truncated subtraction, nonnegative flags, and related order facts so downstream arithmetic can treat signed orbits as an ordered integer type without reopening representation details.
In the broader Recognition foundation stack, ordered integers sit under the path from logic-nats through signed orbits toward PRC rationals and Cauchy reals. The lemma does not itself touch the forcing chain (T0–T8), J-cost, or phi; it is pure order hygiene needed so those later layers can assume $a-0=a$ in order goals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.