lt_zero_sub_right_iff
plain-language theorem explainer
For signed orbits, b is strictly less than zero minus a if and only if b is strictly less than the pointwise negation of a. Order-theory and integer-construction work in the Primitive Recognition Calculus cites this to treat 0−a and −a interchangeably on the right of <. The proof is a one-line application of right-congruence of < under balanced equivalence, using that 0−a is balanced with −a.
Claim. For signed orbits $a,b$ (pairs of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$), $b < (0 - a)$ if and only if $b < (-a)$, where $<$ is the internal strict order (nonnegative difference and not balanced) and $-a$ is pointwise swap of the positive and negative components.
background
Signed orbits are the integer layer of the Primitive Recognition Calculus: a structure with components pos and neg (distinction naturals), intended as the difference pos − neg. Pointwise negation swaps those components. The internal strict order on signed orbits is the conjunction of the weak order with failure of balanced equivalence (same integer value).
Balanced equivalence identifies presentations of the same integer. Upstream, zero_sub_balanced_negate records that subtracting $a$ from zero yields a representative balanced with the pointwise negation of $a$. The companion congruence lt_congr_right_of_balanced states that if two right-hand sides are balanced, then strict comparison from a fixed left-hand side is equivalent for both.
This module builds the order surface on those signed orbits so later certificates can treat the internal integer order as closed and displayable.
proof idea
One-line term proof. Apply right-congruence of strict order under balanced equivalence (lt_congr_right_of_balanced) to the pair $(0-a)$ and $(-a)$, feeding the balanced witness zero_sub_balanced_negate a. No further case analysis: once the two right-hand sides are known balanced, $b < (0-a)$ rewrites to $b < (-a)$.
why it matters
Feeds the integer-order certificate (integer_order_certificate), whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, weak order, absolute difference, and nonnegativity flags; interchangeable use of $0-a$ and $-a$ on the right of $<$ is part of making subtraction and negation coherent on the order surface.
In the broader Recognition foundation, signed orbits sit under the arithmetic-from-logic stack that eventually supports the forcing chain and continuum constructions. This lemma is local plumbing, not a T0–T8 landmark, but it removes a presentation mismatch that would otherwise block order certificates and downstream integer reasoning.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.