cmp_of_sub_inputs_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced, comparing a fixed orbit against either difference yields the same Ordering. Order-surface and certificate authors cite it to show subtraction is well-defined on balanced classes before the integer-order certificate closes. The proof is a short tactic: reflexivity of balance on the fixed orbit, then congruence of cmp under balanced subtraction.
Claim. Let $c,a,a',b,b'$ be signed orbits. If $a$ is balanced with $a'$ and $b$ is balanced with $b'$, 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). Two orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; that is the internal equivalence, not a display-side $\mathbb{Z}$ equality. The bridge lemma states this matches the verifier integer display: balanced iff the two toInt values agree.
Subtraction of signed orbits is defined via addition after negation. The comparison selector cmp returns eq when the two arguments are balanced, otherwise inspects the nonnegativity flag of the difference. Congruence lemmas already show that balance is preserved by subtraction and that cmp itself is invariant when both arguments are replaced by balanced partners.
This module builds the internal order surface on those primitives so that later certificates can treat order as closed without appealing to classical integer comparison.
proof idea
Instantiate balance of the fixed orbit with itself: rewrite via the characterization that balance is equivalent to equal toInt, which is immediate for identical arguments. Feed that reflexivity hypothesis together with the already-proved fact that subtraction preserves balance of both summands into the general congruence of cmp under balanced replacement of both arguments. The goal is then exactly the desired equality of orderings.
why it matters
The integer-order certificate packages the closed internal signed-orbit order surface (truncated subtraction display, leq display, abs-diff, signed nonnegativity). This lemma supplies the missing well-definedness of comparing a fixed orbit against a difference when the minuend and subtrahend move inside their balanced classes, so the certificate can treat subtraction as an operation on equivalence classes rather than on raw orbit representatives.
In the Recognition foundation stack this sits under ledger forcing and the primitive recognition calculus: balance is the internal integer relation before any continuum or J-cost structure appears. It does not itself invoke the forcing chain T5–T8, but it keeps the discrete order layer choice-free and display-independent, which those later layers assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.