le_sub_self_left_iff
plain-language theorem explainer
On signed orbits, self-subtraction on the left of ≤ is interchangeable with zero: a−a ≤ b holds exactly when 0 ≤ b. Order-theory work in the primitive recognition calculus cites this to clear trivial left differences. The proof is a one-line term applying left-congruence of ≤ under the balanced relation, using that a−a is balanced to zero.
Claim. For signed orbits $a$ and $b$, $a-a \le b$ if and only if $0 \le b$, where $\le$ means the difference of the right operand minus the left is nonnegative.
background
Signed orbits are the internal integer model in the primitive recognition calculus: pairs (pos, neg) of distinction naturals, read as pos − neg. Their order is defined by nonnegativity of the difference: a ≤ b means nonneg(b − a). Two orbits are balanced when they represent the same integer (equal toInt).
The ambient module builds the order surface on that representation: reflexivity, totality, trichotomy, and sign-flag characterizations sit as siblings. Upstream, le on logic naturals is the usual existential-sum order; the signed version lifts it through the orbit difference.
The key prior facts are that self-subtraction is balanced to zero (sub_self_balanced_zero), and that ≤ is invariant on the left under balanced pairs (le_congr_left_of_balanced). Together they turn any occurrence of a − a on the left of ≤ into a pure zero comparison.
proof idea
Term-mode one-liner. Apply le_congr_left_of_balanced at the pair (a − a, 0), discharging the balanced hypothesis with sub_self_balanced_zero a. That lemma rewrites both sides of ≤ through toInt and uses balanced-iff-equal-toInt, so the self-difference is replaced by zero and the biconditional falls out immediately. No case split on signs or flags.
why it matters
Feeds the closed order certificate integer_order_certificate, whose doc states the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, absolute difference, nonnegativity, and flag characterizations; this iff is one of the algebraic reductions that keep left-hand differences canonical.
In the Recognition foundation stack, integers arise from distinction orbits before rationals and the J-cost calculus. Cleaning a − a to zero on the order side keeps the arithmetic layer free of representation noise, so later forcing steps (T5 J-uniqueness onward) can treat integer comparisons as genuine, not orbit-dependent. No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.