lt_subtractions_iff_of_balanced
plain-language theorem explainer
Strict comparison of differences of signed orbits is invariant under balanced replacement of each operand. Anyone assembling the internal integer order from δ-orbit positions cites this to transport inequalities across equivalent representatives. The argument is a one-line composition: subtraction preserves balance, then order congruence applies to the two differences.
Claim. Let $a,a',b,b',c,c',d,d'$ be signed orbits. If $a$ is balanced with $a'$, $b$ with $b'$, $c$ with $c'$, and $d$ with $d'$ (equal cross-sums of positive and negative orbit lengths), then $a-b < c-d$ if and only if $a'-b' < c'-d'$, where $<$ is the internal strict order: nonnegative difference and not balanced.
background
In the Primitive Recognition Calculus, integers are realized as signed orbits: pairs of δ-orbit positions recording positive and negative length. 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 orbit data.
Strict order on signed orbits is the conjunction of the weak order with failure of balance: $a<b$ means $a\le b$ and the pair is not balanced. Subtraction is defined via addition of the negation, so differences live in the same signed-orbit type.
Upstream, subtraction congruence already shows that if the summands are pairwise balanced then the differences are balanced. Order congruence shows that strict order is insensitive to balanced replacement on either side. The present statement packages those facts for the four-operand comparison of two differences.
proof idea
Term-mode one-liner. Apply subtraction congruence twice: balanced $a\sim a'$ and $b\sim b'$ yield balanced $\mathrm{sub},a,b\sim\mathrm{sub},a',b'$; likewise for $c,d$ and $c',d'$. Feed those two balance witnesses into order congruence, which rewrites $x<y$ under balanced replacement of both arguments. No extra case analysis.
why it matters
The parent consumer is the integer-order certificate, which asserts that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags). Without invariance of $<$ on differences under balanced representatives, that certificate could not treat subtraction as a well-defined operation on the quotient by balance.
This sits in the Foundation layer that builds arithmetic from recognition structure before the forcing chain (T0–T8) and physical constants. It is pure order-well-definedness on the PRC integer model, not a physics claim, but it is required scaffolding for any later mass-ladder or ledger argument that compares integer quantities constructed as orbit differences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.