le_zero_sub_left_iff
plain-language theorem explainer
For signed orbits, left-hand order against b is unchanged when 0−a is replaced by −a. Anyone assembling the integer order from recognition orbits cites this when rewriting zero-minus as negation. The proof is a one-line left-congruence from the balanced identity 0−a ∼ −a.
Claim. For signed orbits $a,b$, one has $(0-a)\le b$ if and only if $(-a)\le b$, where $\le$ is the internal signed-orbit order ($b-a$ nonnegative) and $-a$ is pointwise swap of the positive and negative legs.
background
Signed orbits are the K4.6 integer carriers in the primitive recognition calculus: pairs (pos, neg) of distinction naturals, read as the formal difference pos − neg. Pointwise negation swaps the two legs. Subtraction and zero are the induced group operations on that carrier.
Internal order is defined by nonnegativity of the difference: a ≤ b means b − a is nonnegative. Two orbits are balanced when they represent the same integer (equal toInt). The module builds a total order on this carrier from those primitives, without importing classical ℤ as a black box.
Upstream, zero_sub_balanced_negate records that 0 − a is balanced with −a (via toInt arithmetic: 0 − toInt a = − toInt a). Left order-congruence for balanced pairs then lets any left operand be rewritten under ≤.
proof idea
One-line term proof. Apply left order-congruence for balanced orbits to the pair (0 − a, −a), feeding the already-proved balanced identity zero_sub_balanced_negate a. That identity is itself a short toInt calculation (sub_toInt, zero_toInt, negate_toInt). No case split on signs is needed here.
why it matters
This is a small rewrite lemma in the integer-order surface of the primitive recognition calculus. It lets later proofs treat zero-minus and negation as interchangeable on the left of ≤, which is the natural form of additive inversion for signed orbits.
Downstream it is consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas (truncated sub, leq flags, abs-diff, signed nonneg) so the order layer can be cited as a finished foundation block rather than an open stub pile.
In the broader Recognition stack this sits under Foundation arithmetic-from-logic work that precedes the forcing chain (T5 J-uniqueness through T8 dimension). It does not itself force φ or the eight-tick octave; it only stabilizes the signed integer order those later steps assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.