cmp
plain-language theorem explainer
Internal three-way comparison on signed orbits: equal when lengths balance, otherwise ordered by the nonnegative flag of the difference. Order and arithmetic lemmas on PRC integers cite it as the computable selector. The body is a straight if-then on balanced and nonnegFlag, not a display-integer comparison.
Claim. For signed orbits $a,b$ (each a pair of distinction-nat lengths meaning $\mathrm{pos}-\mathrm{neg}$), define $\mathrm{cmp}(a,b)\in\{\mathrm{eq},\mathrm{lt},\mathrm{gt}\}$ by: $\mathrm{eq}$ if $a$ and $b$ are balanced ($a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$); otherwise $\mathrm{lt}$ if $b-a$ is nonnegative by the structural flag; otherwise $\mathrm{gt}$.
background
In the Primitive Recognition Calculus, integers are not bare $\mathbb{Z}$ values. A signed orbit is a pair of distinction-nat lengths $(\mathrm{pos},\mathrm{neg})$ with intended meaning $\mathrm{pos}-\mathrm{neg}$. Two orbits are balanced when $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$; that is the internal equivalence relation on PRC integers, defined only on $\delta$-orbit positions.
Nonnegativity is a computable Bool flag: $\mathrm{nonnegFlag}(z)$ holds when the negative side is structurally $\le$ the positive side. Strict order is then nonnegative difference with nonzero (unbalanced) difference. The IntegerOrder module builds the ordered arithmetic layer on top of these IntegerRational primitives; this selector is the bridge from those Props/Bools to Lean's Ordering type used by congruence and translation lemmas.
proof idea
Definitional, not a proof. Case on whether $a$ and $b$ are balanced: if yes, return equality. Otherwise subtract $a$ from $b$ and read the structural nonnegative flag of that difference: true yields less-than, false yields greater-than. No external lemmas; only the balanced relation, subtraction, and nonnegFlag on signed orbits.
why it matters
This is the internal comparison API for PRC integers. Downstream order facts are stated in terms of it: equality of cmp iff balanced; cmp equals gt iff the reverse strict order; congruence under balanced replacement; and left/right translation invariance under addition (cmp_add_left, cmp_add_right). Those lemmas case-split on the three Ordering values this def produces.
In the foundation stack it keeps integer order on orbit geometry rather than on a verifier display integer, matching the module's claim that comparison is from signed-orbit order and balanced length. It sits under the arithmetic-from-logic and ledger-forcing layer that eventually feeds the forcing chain, but it is local plumbing: a selector, not a T5–T8 landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.