lt_of_sub_left_input_iff_of_balanced
plain-language theorem explainer
If two signed orbits represent the same integer, subtracting a common right operand preserves strict order against any fixed left operand: c < a−b iff c < a′−b whenever a ~ a′. Builders of the PRC integer-order surface cite this left-input congruence. The proof is a one-line composition of right-order congruence with left-subtraction balance preservation.
Claim. Let $c,a,a',b$ be signed orbits. If $a$ is balanced with $a'$ (same integer: $a_{\mathrm{pos}}+a'_{\mathrm{neg}}=a'_{\mathrm{pos}}+a_{\mathrm{neg}}$), then $c < a-b$ if and only if $c < a'-b$, where $<$ is the internal strict order (nonnegative difference and not balanced).
background
In Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit positions (pos, neg) recording excess on each side of a δ-ledger. Two signed orbits are balanced when $a.pos + b.neg = b.pos + a.neg$; that is the internal integer equality, defined only on orbit lengths (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 not balanced. Subtraction is the corresponding group operation on these pairs. The surrounding IntegerOrder module builds the ordered-group surface from these primitives, without classical $\mathbb{Z}$.
Upstream, sub_congr_of_balanced_left shows that if $a \sim a'$ then $a-b \sim a'-b$. Separately, lt_congr_right_of_balanced says strict order is invariant when the right operand is replaced by a balanced twin (via the toInt characterization).
proof idea
One-line term proof. First apply left-subtraction congruence: balanced $a \sim a'$ yields balanced $(a-b) \sim (a'-b)$. Feed that witness into right-order congruence, which rewrites $c < \cdot$ across any balanced pair on the right. No case split or toInt expansion appears at this layer; both steps are already proved.
why it matters
This is a structural congruence for the ordered group of signed orbits: left inputs to subtraction may be replaced by integer-equivalent twins without changing comparisons from a fixed left operand. 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 (nonneg flags, abs-diff, truncated sub) that seal the PRC integer-order API used higher in the foundation stack.
In the Recognition forcing chain this sits below arithmetic-from-logic and ledger forcing: once order respects the balance relation under subtraction, the φ-ladder and mass formulas can treat integer ranks as well-defined rather than representative-dependent. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.