cmp_sub_self_right
plain-language theorem explainer
Comparing any signed orbit $b$ against a self-difference $a-a$ yields the same ordering result as comparing $b$ against zero. Anyone building the internal PRC integer order (trichotomy, nonneg flags, certificate closure) cites this reduction. The proof is a two-line congruence: $b$ balances itself and $a-a$ balances zero, so comparison is invariant.
Claim. For signed orbits $a,b$, the internal comparison $\mathrm{cmp}(b,\,a-a)$ equals $\mathrm{cmp}(b,\,0)$.
background
In the Primitive Recognition Calculus, integers are carried as signed orbits: pairs of nonnegative orbit lengths (pos, neg) rather than a bare $\mathbb{Z}$ display. Two orbits are balanced when $a.pos+b.neg=b.pos+a.neg$; that is the internal equivalence, and it agrees with equality of the verifier integer map (balanced_iff_toInt_eq).
Internal comparison cmp is defined from that balance relation and the nonneg flag of a difference: equal when balanced, otherwise ordered by whether $b-a$ is nonnegative. It deliberately does not consult the external integer display.
Upstream, sub_self_balanced_zero already records that $a-a$ is balanced with the zero orbit, and cmp_congr_of_balanced says comparison is unchanged when either argument is replaced by a balanced partner.
proof idea
Reflexivity of balance on $b$ is obtained by rewriting with balanced_iff_toInt_eq (same toInt implies balanced). Combined with sub_self_balanced_zero a (so $a-a$ balances zero), a single application of cmp_congr_of_balanced rewrites $\mathrm{cmp}(b,a-a)$ into $\mathrm{cmp}(b,0)$. No case split on the ordering constructor is needed.
why it matters
This is a small but necessary identity on the signed-orbit order surface: self-subtraction must act as the zero of the order, not merely of the additive structure. It is consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed," packaging display lemmas for truncated subtraction, $\le$, absolute difference, and nonneg flags.
In the Recognition foundation stack this sits under the ledger/forcing layer that eventually feeds the T0–T8 chain; here the work is purely the discrete order calculus that makes integer comparisons choice-free and display-independent before continuum or $\phi$-ladder structure appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.