lt_sub_self_right_iff
plain-language theorem explainer
For signed orbits, the right-hand side of a strict comparison may be replaced by zero when it is a self-difference: b < a−a holds exactly when b < 0. Authors of the integer-order certificate cite this when normalizing self-subtraction in the signed-orbit order surface. The proof is a one-line term application of right-congruence of strict order under the balanced relation, using that a−a is balanced with zero.
Claim. For any signed orbits $a$ and $b$, $b < (a - a)$ if and only if $b < 0$, where $<$ is the internal strict order on signed orbits (nonnegative difference that is not balanced) and $0$ denotes the zero signed orbit.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction-nats intended as a difference pos − neg. Two signed orbits are balanced when they represent the same integer (equivalently, when their toInt images agree). The internal strict order is defined by $a < b$ iff $a \le b$ and $a$ is not balanced with $b$.
Self-subtraction is already known to be balanced with zero: sub_self_balanced_zero states that $a - a$ is balanced with the zero signed orbit. Separately, lt_congr_right_of_balanced records that strict order is invariant on the right under balanced replacement: if $b$ is balanced with $b'$, then $a < b$ iff $a < b'$. Both facts live in the same IntegerOrder module that builds a total order on these signed differences from the underlying LogicNat order.
The local setting is the closed order surface on signed orbits: reflexivity, transitivity, antisymmetry up to balance, totality, trichotomy, and the various sign-flag characterizations of nonnegativity and negativity.
proof idea
One-line term proof. Apply right-congruence of strict order under balance (lt_congr_right_of_balanced) to the instance sub_self_balanced_zero a, which supplies the hypothesis that $a - a$ is balanced with zero. The biconditional $b < (a - a) \leftrightarrow b < 0$ is then immediate; no further case analysis or unfolding of lt is required.
why it matters
This lemma is a normalization step inside the signed-orbit order toolkit. 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 for truncated subtraction, absolute difference, and nonnegativity flags, sealing the integer-order layer of the Primitive Recognition Calculus.
In the broader Recognition Science stack, integers and their order are reconstructed from distinction structure before rationals (PRCRat) and Cauchy reals. Clean identities such as $a - a \sim 0$ under the order relation keep later arithmetic and cost comparisons free of residual self-difference noise. The result does not itself touch the forcing chain (T5–T8) or the Recognition Composition Law, but it is part of the arithmetic substrate those layers sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.