cmp_eq_lt_iff
plain-language theorem explainer
On signed orbits, the internal comparison selector returns less-than exactly when the strict order holds. Anyone proving translation or sign-sensitive multiplication rules for that selector cites this biconditional. One direction is the existing one-way lemma; the other unfolds the selector, cases on balance and the nonnegativity flag, then finishes by the integer-display bridge and omega.
Claim. For signed orbits $a$ and $b$, the internal comparison selector satisfies $\mathrm{cmp}(a,b)=\mathrm{lt}$ if and only if $a<b$ in the signed-orbit strict order.
background
In the Primitive Recognition Calculus integer layer, a signed orbit carries positive and negative $\delta$-orbit lengths. Two orbits are balanced when $a.pos+b.neg=b.pos+a.neg$; that internal relation is equivalent to equality of the verifier integer display $a.toInt=b.toInt$.
Strict order on signed orbits is the order induced through that display (and ultimately from the LogicNat order $n<m:\Leftrightarrow\exists k.,n+\mathrm{succ},k=m$). The comparison selector is defined without consulting the display first: it returns equality on balanced pairs, otherwise less-than precisely when the difference $b-a$ has nonnegativity flag true, else greater-than.
The one-way implication from strict order to selector less-than is already available; the present result closes the converse and packages both directions as an iff.
proof idea
Split the biconditional. Forward: assume the selector equals less-than, unfold its definition, and case on whether $a$ and $b$ are balanced. The balanced branch contradicts the selector value by simplification. In the unbalanced branch, case on the nonnegativity flag of $b-a$. When the flag is true, rewrite via the characterizations of strict order, nonnegativity, subtraction, and balance in terms of $toInt$, then finish with omega on the integers. When the flag is false, simplification again contradicts the selector. Reverse: apply the existing one-way lemma that strict order forces the selector to less-than.
why it matters
This iff is the workhorse that lets later lemmas treat the selector as interchangeable with the strict order. Downstream, addition-invariance of the selector (left and right), congruence of the selector under balanced replacements, and the sign-sensitive multiplication rules (nonnegative and negative left/right factors) all case on the selector and immediately recover a strict-order hypothesis via this equivalence. Negation-swap for the selector uses it the same way. In the foundation stack it keeps the PRC integer order aligned with the internal comparison used by arithmetic lemmas, without smuggling classical choice through the integer display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.