le_sub_inputs_iff_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced-equivalent, the order relation of their difference against a third orbit is independent of representatives. Anyone assembling the internal PRC integer order cites this congruence. The proof is a one-line composition of left-order congruence with subtraction congruence under balance.
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_{\mathrm{pos}}+a'_{\mathrm{neg}}=a'_{\mathrm{pos}}+a_{\mathrm{neg}}$ and likewise for $b,b'$), then $a-b\le c$ if and only if $a'-b'\le c$, where $\le$ means the difference is nonnegative.
background
In the Primitive Recognition Calculus, integers are realized as signed orbits: pairs of $\delta$-orbit lengths carrying a positive and a negative part. Two signed orbits $a,b$ are balanced when $a.pos+b.neg=b.pos+a.neg$; this is the internal integer equality relation, defined entirely on orbit positions (K4.9).
The internal order is defined by $a\le b$ iff the signed difference $b-a$ is nonnegative. Subtraction is built from addition and negation on signed orbits. The surrounding module develops the order theory of these objects (reflexivity, transitivity, totality, trichotomy, sign-flag characterizations) before packaging a closure certificate.
Upstream, sub_congr_of_balanced shows that balanced pairs remain balanced after subtraction, and le_congr_left_of_balanced shows that the order is invariant under replacing the left argument by a balanced twin (via the bridge to integer comparison).
proof idea
One-line term proof. First apply subtraction congruence under balance to obtain that $a-b$ is balanced with $a'-b'$. Then feed that balanced pair into left-order congruence, which rewrites $a-b\le c$ into $a'-b'\le c$. No further case analysis or unfolding is required.
why it matters
This lemma is a representative-independence fact for differences under the internal order. It is consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display equalities for truncated subtraction, nonnegativity, and absolute difference, sealing the order layer of the PRC integer construction.
In the broader Recognition foundation, integers and their order sit beneath the arithmetic-from-logic ladder that eventually feeds the forcing chain. Closing congruence of $\le$ under balanced subtraction is bookkeeping needed before one can treat signed-orbit integers as well-defined ordered objects rather than raw orbit pairs. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.