cmp_eq_eq_of_balanced
plain-language theorem explainer
If two signed orbits balance (equal net length under the internal δ-orbit relation), their internal comparison returns equality. Order and arithmetic lemmas on signed orbits cite this to discharge the equality branch of the comparison selector. The proof is a one-line simplification against the definition of the selector.
Claim. Let $a$ and $b$ be signed orbits (pairs of distinction naturals, read as $a=\mathrm{pos}-\mathrm{neg}$). If $a$ and $b$ are balanced, i.e. $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$, then the internal comparison of $a$ and $b$ equals $\mathrm{Ordering.eq}$.
background
In the Primitive Recognition Calculus, integers are not taken as primitives. A signed orbit is a pair of distinction naturals (pos, neg) with intended meaning pos - neg. Two signed orbits are balanced when their orbit lengths match under the internal relation a.pos + b.neg = b.pos + a.neg (K4.9). That relation is the PRC stand-in for integer equality, defined entirely on δ-orbit positions rather than on a verifier display.
The internal comparison selector cmp is defined from signed-orbit order and balanced length: it returns equality exactly when the two orbits balance, otherwise it branches on the nonnegativity flag of the difference b - a. This lemma is the direct reading of that first branch. The surrounding module builds a total order and arithmetic compatibility for these orbits without appealing to classical Int comparison.
proof idea
One-line wrapper. Unfold the definition of the comparison selector and simplify with the balanced hypothesis: the first if branch fires and yields Ordering.eq. No auxiliary lemmas are required beyond definitional reduction.
why it matters
This is the equality-introduction rule for the internal comparison. Downstream it feeds the biconditional cmp = eq ↔ balanced, congruence of comparison under balanced replacements, left/right translation invariance of cmp under addition, and the sign-sensitive multiplication rules (negative vs nonnegative multiplier, excluding the balanced-zero case). Those results assemble the ordered-ring skeleton of signed orbits inside PRC IntegerOrder.
In the Recognition foundation this keeps integer order internal to δ-orbit data, consistent with ledger balance as the primitive equivalence, rather than importing classical integer comparison. It is scaffolding for later forcing and ledger arguments that need a well-behaved ordered arithmetic on recognition integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.