lt_of_sub_inputs_iff_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (same integer values), strict comparison of a fixed orbit against their differences is invariant under that replacement. Anyone assembling the PRC integer-order surface cites this congruence. The proof is a one-line composition of right-congruence for strict order with balance-congruence of subtraction.
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.pos+b'.neg=a'.pos+a.neg$ and likewise for $b,b'$), then $c < a-b$ if and only if $c < a'-b'$.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit positions (pos, neg). Two signed orbits are balanced when $a.pos + b.neg = b.pos + a.neg$; that is the internal integer equality, defined only on $\delta$-orbit data (K4.9).
Strict order on signed orbits is the internal relation "nonnegative difference and not balanced": $a < b$ means $a \le b$ and $\neg$ balanced$(a,b)$. Subtraction is defined via addition of the negation, so balance of differences follows from balance of summands and of negations.
The local module builds the order surface on these orbits: reflexivity, totality, trichotomy, and flag characterizations of sign. Upstream, right-congruence already says $a < b \leftrightarrow a < b'$ whenever $b$ is balanced with $b'$; separately, subtraction preserves balance of both arguments.
proof idea
One-line term proof. First apply balance-congruence of subtraction: from $a$ balanced $a'$ and $b$ balanced $b'$, conclude that $a-b$ is balanced with $a'-b'$. Then feed that witness into right-congruence of strict order, which rewrites $c < (a-b)$ into $c < (a'-b')$. No case split or unfolding of $lt$ is needed at this site.
why it matters
This lemma is a small but necessary congruence step in closing the internal signed-orbit order surface. It is consumed by the integer-order certificate, whose doc-comment states that surface is closed and packages display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags.
In the Recognition foundation stack, integers and their order are not imported from classical $\mathbb{Z}$; they are forced from orbit arithmetic on the ledger. Congruence of $<$ under balanced replacement of difference inputs is exactly the statement that the order descends to balance-classes, i.e. to genuine integers. That descent is prerequisite for later ladder and mass constructions that treat integer rungs as well-defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.