cmp_of_sub_right_input_of_balanced
plain-language theorem explainer
If two signed orbits balance, right-subtracting either from a fixed orbit leaves the comparison against any third orbit unchanged. Order-certificate authors cite this when showing the internal comparison selector is well-defined on balanced classes. The proof is a two-line application of comparison congruence after right-subtraction congruence and reflexivity of balance.
Claim. Let $c,a,b,b'$ be signed orbits. If $b$ and $b'$ are balanced (i.e. $b.\mathrm{pos}+b'.\mathrm{neg}=b'.\mathrm{pos}+b.\mathrm{neg}$), then $\mathrm{cmp}(c,\,a-b)=\mathrm{cmp}(c,\,a-b')$.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (pos, neg) rather than a bare $\mathbb{Z}$ display. Two signed orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; this is the internal equivalence (K4.9), and it agrees with equality of the verifier integer display via balanced_iff_toInt_eq.
The internal comparison selector cmp is defined from that balance relation and the nonnegativity flag of a difference: equal when the arguments balance, otherwise ordered by whether $b-a$ is nonnegative. Subtraction of signed orbits is the corresponding orbit-level operation. The local module builds a choice-free order surface on these objects, independent of the external integer view.
Upstream, right-subtraction preserves balance: if $b\sim b'$ then $a-b\sim a-b'$. Comparison itself is congruent under balanced replacements of both arguments.
proof idea
First obtain reflexivity of balance on the left argument $c$ by rewriting through the bridge balanced_iff_toInt_eq (equal integer displays). Then apply comparison congruence under balanced pairs: the left pair is $(c,c)$, the right pair is $(a-b,,a-b')$, the latter supplied by right-subtraction congruence from the hypothesis $b\sim b'$. The result is equality of the two cmp values.
why it matters
This lemma is one of the congruence facts that close the internal signed-orbit order surface. It is consumed by integer_order_certificate, whose doc-comment states that surface is closed: display bridges for truncated subtraction, $\le$, absolute difference, and nonnegativity flags all line up with the internal order.
In the Recognition foundation stack, integer order on $\delta$-orbits is scaffolding for ledger arithmetic and the forcing chain that later pins $J$, $\varphi$, the eight-tick octave, and $D=3$. Without right-input stability of cmp under balance, the order would depend on representative choice and the certificate could not be assembled. The result is fully proved (no sorry); it does not itself force physical constants, but it keeps the PRC integer layer coherent for those later steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.