cmp_sub_inputs_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced-equivalent, their differences compare the same way against any third orbit. Order theorists working on the PRC integer surface cite this when transporting comparisons across balanced representatives. The proof is a short congruence chain: difference preserves balance, then comparison is invariant under balanced pairs.
Claim. Let $a,a',b,b',c$ be signed orbits. If $a$ is balanced with $a'$ and $b$ is balanced with $b'$, then $\mathrm{cmp}(a-b,\,c)=\mathrm{cmp}(a'-b',\,c)$, where $\mathrm{cmp}$ is the internal signed-orbit comparison (equality on balance, otherwise ordered by the nonnegativity flag of the difference).
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative $\delta$-orbit lengths (pos, neg). Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That internal relation is the PRC integer equality; by balanced_iff_toInt_eq it agrees with equality of the verifier display toInt.
Comparison cmp is defined without consulting toInt: if the two arguments are balanced it returns equality; otherwise it inspects the nonnegativity flag of their difference. Subtraction is built from addition and negation on signed orbits. The local module develops the order surface on these internal objects so that later certificates can close the integer-order API without classical choice.
Upstream, sub_congr_of_balanced says balanced pairs yield balanced differences, and cmp_congr_of_balanced says cmp is invariant when both arguments are replaced by balanced equivalents.
proof idea
First obtain reflexivity of balance on the third argument $c$ by rewriting with balanced_iff_toInt_eq (so $c$ is balanced with itself). Then apply cmp_congr_of_balanced to the pair of differences and to $c$, feeding sub_congr_of_balanced ha hb as the left-hand balance hypothesis. The whole argument is two lines of congruence composition; no case split on Ordering is needed here.
why it matters
This lemma is a transport rule for comparisons of differences: once representatives are fixed only up to balance, cmp of a difference against a fixed third orbit is well-defined. It feeds the closed integer-order surface packaged by integer_order_certificate ("The internal signed-orbit order surface is closed."), which bundles display bridges for truncated subtraction, $\le$, absolute difference, and nonnegativity flags.
In the Recognition foundation stack, the PRC integer layer sits under ledger forcing and the later forcing chain (T0–T8). Keeping comparison congruence internal (on $\delta$-orbit positions rather than on a classical $\mathbb{Z}$ quotient) preserves the choice-free character of the order API. Without this fact, difference-based order statements would depend on representative choice and the certificate could not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.