cmp_sub_right_input_of_balanced
plain-language theorem explainer
If two signed orbits are balanced, right-subtracting either from a fixed orbit yields the same comparison against any third orbit. Order theorists and PRC auditors cite it when showing the internal comparison is invariant under integer-equivalent right inputs. The proof is a short congruence: right-sub preserves balance, then cmp is congruent under balanced pairs.
Claim. Let $a,b,b',c$ 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}(a-b,c)=\mathrm{cmp}(a-b',c)$, 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 (pos, neg) rather than a bare $\mathbb{Z}$ display. Two orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; by K4.9 this is equivalent to equal verifier integers via balanced_iff_toInt_eq.
Subtraction of signed orbits is the internal difference used by the order surface. The comparison selector cmp returns equality when the two arguments are balanced, otherwise reads the nonnegativity flag of the difference. It is defined from signed-orbit order and balanced length, not from the verifier integer display.
Upstream, right-subtraction preserves balance: if $b\sim b'$ then $a-b\sim a-b'$ (sub_congr_of_balanced_right). Separately, cmp is jointly congruent in both slots under balanced replacements (cmp_congr_of_balanced).
proof idea
Reflexivity of balance on $c$ is immediate from the bridge to equal integers: rewrite with balanced_iff_toInt_eq. Right-subtraction congruence then supplies balance of $a-b$ with $a-b'$. Feed those two balanced pairs into cmp_congr_of_balanced to equate the two comparisons. Five-line tactic proof; no case split on Ordering.
why it matters
Feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas (truncated sub, leq, abs-diff, signed nonneg flags) so the order API can be treated as a finished foundation object rather than an open congruence obligation.
In the Recognition stack this sits in the pre-physics integer layer of Primitive Recognition Calculus: before J-cost uniqueness (T5), $\varphi$ forcing (T6), or the eight-tick octave (T7). Closing right-input invariance of cmp under balance is one of the small algebraic facts that keep the internal order independent of which balanced representative is chosen for a difference. Without it, downstream certificates could not treat subtraction as well-defined on the quotient by balance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.