cmp_zero_sub_right
plain-language theorem explainer
Comparing any signed orbit b against zero-minus-a equals comparing b against the negation of a. Order-surface authors cite this when rewriting right-hand sides of cmp through the internal subtraction/negation bridge. The proof is a two-line congruence: reflexivity of balanced on b plus the zero-sub/negate balance lemma.
Claim. For signed orbits $a$ and $b$, the internal comparison $\mathrm{cmp}(b,\, 0-a)$ equals $\mathrm{cmp}(b,\, -a)$.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative $\delta$-orbit lengths (positive and negative sides). Two orbits are balanced when $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$, equivalently when their verifier displays toInt agree. That relation is the internal integer equality used throughout the order surface.
The comparison selector cmp is defined from the signed-orbit order and balanced length, not from the external $\mathbb{Z}$ display: equal when balanced, otherwise ordered by the nonnegativity flag of the difference. Negation and subtraction are orbit-level operations; a prior lemma records that $0-a$ is balanced with $-a$, so they represent the same integer.
This module builds the internal order laws (reflexivity, totality, trichotomy, sign-flag bridges) needed before any certificate that the order surface is closed.
proof idea
Reflexivity of balance on the left argument is immediate from balanced_iff_toInt_eq (same toInt). The right arguments $0-a$ and $-a$ are already known balanced by zero_sub_balanced_negate. Feed both witnesses into cmp_congr_of_balanced, which states that cmp is invariant when each side is replaced by a balanced partner. No case split on Ordering is required here.
why it matters
The rewrite lets every right-hand occurrence of zero-minus-$a$ in a comparison be replaced by negation without leaving the internal PRC vocabulary. Downstream it is consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display bridges (truncated sub, leq, abs-diff, signed nonneg flags) so later forcing and ledger layers can treat orbit order as a finished integer order. Within the Recognition foundation this is bookkeeping on the integer carrier that underpins the forcing chain, not a physics step itself; it keeps subtraction and negation interchangeable before mass-ladder or eight-tick constructions ever see the order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.