le_zero_sub_right_iff
plain-language theorem explainer
For signed orbits, the order relation treats zero-minus-a and the pointwise negation of a as interchangeable on the right-hand side. Anyone assembling the internal integer order from signed-orbit differences would cite this equivalence. The proof is a one-line term application of right-congruence of ≤ under the balanced relation, using that those two right-hand sides are balanced.
Claim. For signed orbits $a$ and $b$, one has $b \le (0 - a)$ if and only if $b \le (-a)$, where $-a$ is pointwise swap of the positive and negative components and $\le$ means the difference is nonnegative.
background
Signed orbits are the K4.6 difference carriers in the primitive recognition calculus: a pair (pos, neg) of distinction naturals, read as pos - neg. Pointwise negation swaps the two components. Internal order is defined by nonnegativity of the difference: $a \le b$ means sub b a is nonnegative.
Two signed orbits are balanced when they represent the same integer (equivalently, equal under the toInt embedding). The module builds the full order surface on these carriers from the LogicNat order ∃ k, n + k = m upward through signed differences.
Upstream, zero_sub_balanced_negate already records that sub zero a is balanced with negate a. Right-congruence le_congr_right_of_balanced then says that if the right endpoints are balanced, the order statements with a fixed left endpoint are equivalent.
proof idea
One-line term proof. Apply le_congr_right_of_balanced at the pair (sub zero a, negate a), feeding the hypothesis zero_sub_balanced_negate a. That lemma rewrites both sides through toInt and uses sub_toInt, zero_toInt, and negate_toInt to obtain integer equality, which is exactly balancedness. Congruence then swaps the right-hand sides of le.
why it matters
This is a small but necessary display identity on 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 signed nonnegativity into one closed bundle.
In the Recognition foundation stack, integers and their order are not imported from Mathlib as primitives; they are reconstructed from distinction counts and signed orbits so that later forcing (T5 J-uniqueness through T8 dimension) sits on a logic-first arithmetic. Closing right-hand-side identities such as zero-sub versus negate keeps the order API coherent before those higher steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.