le_sub_zero_left_iff
plain-language theorem explainer
Subtracting the signed-orbit zero on the left does not change the internal order: a−0 ≤ b if and only if a ≤ b. Anyone building the integer-order surface from signed orbits cites this cancellation identity. The proof is a one-line term application of left-congruence of ≤ under balanced equivalence, using that a−0 is balanced with a.
Claim. For signed orbits $a,b$ (pairs of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$), writing $\le$ for the internal order "$b-a$ is nonnegative" and $0$ for the zero signed orbit, one has $a-0\le b$ if and only if $a\le b$.
background
Signed orbits are the K4.6 integer carriers in Primitive Recognition Calculus: a structure with fields pos and neg of distinction-natural type, intended as the formal difference $\mathrm{pos}-\mathrm{neg}$. Their internal non-strict order is defined by nonnegativity of the difference: $a\le b$ means $\mathrm{nonneg}(b-a)$.
Balanced equivalence identifies signed orbits that represent the same integer (equivalently, equal toInt values). Order is insensitive to that identification on the left: if $a$ is balanced with $a'$, then $a\le b$ iff $a'\le b$. Separately, subtracting zero is a balanced no-op: $a-0$ is balanced with $a$, proved by reducing toInt and a trivial integer identity.
The ambient module assembles the order laws (reflexivity, transitivity, totality, trichotomy, sign-flag characterizations) needed to certify that the signed-orbit order surface is closed.
proof idea
One-line term proof. Apply left-congruence of $\le$ under balanced equivalence to the pair $(a-0,,a)$, discharging the balanced hypothesis with the lemma that $a-0$ is balanced with $a$. No case split and no unfolding of le itself is required.
why it matters
Feeds the integer-order certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags; left-cancellation of zero is part of making $\le$ behave like ordinary integer order on the balanced quotient.
In the Recognition foundation stack this sits under Arithmetic-from-Logic and the primitive recognition calculus: integers arise as signed distinction orbits before rationals and the forcing chain. It does not itself touch T5–T8 or the J-cost, but it is infrastructure those later layers assume when they treat integer comparisons as already settled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.