lt_sub_self_left_iff
plain-language theorem explainer
For signed orbits, a − a is strictly less than b exactly when zero is strictly less than b. Order theorists and anyone assembling the integer-order certificate cite it to erase self-subtraction on the left of <. The proof is a one-line term applying left-congruence of < under balanced equivalence to the fact that a − a is balanced with zero.
Claim. For any signed orbits $a,b$, one has $a-a < b$ if and only if $0 < b$, where $<$ is the internal strict order on signed orbits (nonnegative difference and not balanced).
background
Signed orbits are the PRC integer layer: pairs (pos, neg) of distinction naturals, read as the formal difference pos − neg. Two signed orbits are balanced when they represent the same integer (equivalently, equal under the toInt map). The internal strict order is a < b iff a ≤ b and a is not balanced with b.
Self-subtraction is already known to land on the zero class: sub_self_balanced_zero states that a − a is balanced with SignedOrbit.zero. Separately, lt_congr_left_of_balanced says that if the left arguments are balanced, then strict comparison against a fixed right argument is equivalent. The module builds the ordered-ring surface for these signed orbits from the underlying distinction-nat arithmetic.
proof idea
One-line term proof. Apply lt_congr_left_of_balanced with the balanced witness sub_self_balanced_zero a. That lemma rewrites both sides via lt_iff_toInt_lt and uses balanced_iff_toInt_eq, so replacing the left argument a − a by zero is immediate.
why it matters
Feeds the single downstream consumer integer_order_certificate, whose doc-comment records that "the internal signed-orbit order surface is closed." The certificate packages display lemmas (nonnegativity, flags, truncated subtraction, abs-diff) that the rest of Primitive Recognition Calculus treats as the finished integer-order API.
In the Recognition stack this sits under Foundation arithmetic-from-logic: once signed-orbit order behaves like ordinary integer order under cancellation identities such as a − a = 0, later forcing steps can treat the integer layer as settled rather than re-proving order facts at each use site. It is a small but necessary closure fact on the path from LogicNat strict order up through signed orbits toward the real/Cauchy layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.