lt_sub_inputs_iff_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced-equivalent, their differences stand in the same strict order to any third orbit. Order and arithmetic developers in the Primitive Recognition Calculus cite it when transporting inequalities across integer representatives. The proof is a one-line term: subtraction preserves balance, then left-congruence of strict order finishes.
Claim. Let $a,a',b,b',c$ be signed orbits. If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ (i.e. $a_{+} + a'_{-} = a'_{+} + a_{-}$ and likewise for $b,b'$), then $a-b < c$ if and only if $a'-b' < c$, where $<$ is the internal strict order (nonnegative difference and not balanced).
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of orbit positions recording positive and negative legs. Two signed orbits are balanced when $a_{+} + b_{-} = b_{+} + a_{-}$; that is the internal integer equality, defined only on $\delta$-orbit data (K4.9).
Strict order on signed orbits is the conjunction of the weak order with failure of balance: $a < b$ means $a \le b$ and $\neg,\mathrm{balanced}(a,b)$. Subtraction is defined via addition of the negation, so congruence facts for add and negate lift to sub.
The local module builds the full order surface on these representatives. Upstream, lt_congr_left_of_balanced says balanced pairs may be swapped on the left of $<$, and sub_congr_of_balanced says balanced inputs yield balanced differences.
proof idea
One-line term proof. First apply sub_congr_of_balanced to the two balance hypotheses; that yields balance of the two differences $a-b$ and $a'-b'$. Feed that witness into lt_congr_left_of_balanced with right operand $c$. The latter rewrites both sides through the integer embedding and uses that balanced orbits share the same integer value, so the strict comparisons coincide.
why it matters
This is a transport lemma for the signed-orbit order calculus: inequalities involving differences are independent of which balanced representative is chosen on each input. It is consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display and flag lemmas (nonnegativity, truncated sub, abs-diff) into a single closure object for the integer layer of the foundation stack.
In the broader Recognition Science forcing chain, the integer and order layer sits under the arithmetic-from-logic construction that eventually supports the continuum and the T0–T8 forcing (J-uniqueness, $\varphi$, eight-tick octave, $D=3$). Closing representative-independence for $<$ on differences is routine bookkeeping, but without it the certificate cannot honestly claim a well-defined order surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.