cmp_of_sub_left_input_of_balanced
plain-language theorem explainer
If two signed orbits are balanced (internally equivalent), replacing the left input of a difference leaves comparison against any fixed third orbit unchanged. Anyone building or transporting the PRC integer order surface cites this when moving comparisons across equivalent minuends. The proof is a short congruence: reflexivity of balance on the fixed orbit, left-subtraction congruence, then two-argument comparison congruence.
Claim. Let $a,a',b,c$ be signed orbits. If $a$ and $a'$ are balanced, meaning $a_{\mathrm{pos}}+a'_{\mathrm{neg}}=a'_{\mathrm{pos}}+a_{\mathrm{neg}}$, then $\mathrm{cmp}(c,\,a-b)=\mathrm{cmp}(c,\,a'-b)$, where $\mathrm{cmp}$ is the internal signed-orbit comparison selector.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (positive and negative legs) rather than bare verifier displays. Two signed orbits are balanced when their cross-sums agree, $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$. That relation is the internal PRC integer equivalence; it matches equality of the conservative $\mathbb{Z}$ display via the bridge balanced iff toInt equal.
Internal comparison cmp is defined from that balance relation and the nonnegativity flag of a difference: equal when the two orbits balance, otherwise ordered by whether $b-a$ is nonnegative. Subtraction of signed orbits is the corresponding difference operation on those legs. The IntegerOrder module builds a closed order surface on this internal data, deliberately independent of the verifier integer display except through the balance bridge.
Upstream, left-subtraction already preserves balance: if $a\sim a'$ then $a-b\sim a'-b$. Separately, comparison is a congruence for balance in both slots.
proof idea
Three-line tactic proof. First obtain reflexivity of balance on the fixed left argument $c$ by rewriting with the bridge that balance is equivalent to equal integer displays (so $c$ balances itself). Then apply the two-slot comparison congruence, feeding that reflexivity in the first slot and the already-proved left-subtraction balance congruence (from the hypothesis that $a$ balances $a'$) in the second slot. No case split on the Ordering value is needed here; the work is entirely in the named congruences.
why it matters
This lemma is one of the transport facts that let the internal signed-orbit order treat balanced orbits as interchangeable under differences and comparisons. It is consumed by the integer-order certificate, whose doc-comment states that "the internal signed-orbit order surface is closed": that certificate packages display bridges (truncated subtraction, $\le$, absolute difference, signed nonnegativity and its flag) into a single closed interface.
In the Recognition foundation stack this sits inside the Primitive Recognition Calculus integer layer, below ledger forcing and the later forcing chain (T0–T8). Closing order congruence under subtraction is bookkeeping required before mass-ladder and cost-functional arguments can treat PRC integers as a stable ordered group-like surface. No open scaffold remains on this declaration; it is fully proved and only supports the certificate assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.