lt_of_sub_right_input_iff_of_balanced
plain-language theorem explainer
Right-input replacement under signed-orbit balance preserves strict order after subtraction: if b ~ b', then c < a−b iff c < a−b'. Order and arithmetic developers on the PRC integer surface cite it when rewriting differences. The proof is a two-lemma term composition: balance of the subtracted pair, then right-congruence of lt.
Claim. Let $c,a,b,b'$ be signed orbits. If $b$ is balanced with $b'$ (i.e. $b.\mathrm{pos}+b'.\mathrm{neg}=b'.\mathrm{pos}+b.\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 recording positive and negative legs. Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that relation 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 not balanced. Subtraction is the corresponding signed-orbit difference. The module builds the order surface needed so that later certificates can treat these internal integers as an ordered ring fragment without leaving the recognition calculus.
Upstream, right-congruence of strict order under balance already holds: if $b \sim b'$ then $a < b \leftrightarrow a < b'$. Separately, subtracting a fixed left operand preserves balance on the right: if $b \sim b'$ then $a-b \sim a-b'$.
proof idea
Term-mode composition of two prior facts. First apply right-subtraction balance congruence to the hypothesis $b \sim b'$, obtaining $a-b \sim a-b'$. Feed that balanced pair into right-congruence of strict order, which rewrites the right operand of $<$ and yields $c < a-b \leftrightarrow c < a-b'$. No case split or integer embedding is opened in this proof.
why it matters
Closes a small but necessary rewrite law on the signed-orbit order surface: differences may replace a balanced right input without changing comparisons from a fixed left witness. Downstream it is consumed by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed; the certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags.
In the broader Recognition foundation this sits under arithmetic-from-logic and ledger forcing: order must be invariant under the internal equality (balance) so that later forcing steps can treat integers as well-defined before the T0–T8 chain reaches $J$-uniqueness, $\varphi$, the eight-tick octave, and $D=3$. It does not itself force physical constants; it keeps the integer order API coherent for those later layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.