cmp_eq_gt_iff
plain-language theorem explainer
The internal signed-orbit comparator returns greater-than exactly when the second argument is strictly less than the first. Anyone building order-preserving arithmetic (addition, multiplication by sign flags, congruence under balance) cites this biconditional. The reverse direction is the existing one-way lemma; the forward direction cases on balance and the nonnegativity flag, then finishes by integer comparison and omega.
Claim. For signed orbits $a,b$, the internal comparison $\mathrm{cmp}(a,b)$ equals $\mathrm{gt}$ if and only if $b < a$ in the strict signed-orbit order.
background
In Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (positive and negative legs) rather than a bare verifier integer. Two orbits are balanced when $a_{+} + b_{-} = b_{+} + a_{-}$; balance is the internal equality relation (K4.9), defined only on $\delta$-orbit positions.
The strict order $b < a$ is the PRC order on those orbits. The internal comparator $\mathrm{cmp}$ is defined without consulting the integer display: it returns equality on balanced pairs, otherwise inspects the nonnegativity flag of $b - a$, and otherwise returns greater-than. This theorem ties that selector back to the order predicate.
Upstream, the one-direction fact already shows that $b < a$ forces $\mathrm{cmp}(a,b) = \mathrm{gt}$. Related flag lemmas equate a false nonnegativity flag with a negative integer image of the difference, and $\mathrm{lt}$ is characterized by the integer images under $\mathrm{toInt}$.
proof idea
Iff introduction. Reverse direction is a one-line appeal to $\mathrm{cmp_eq_gt_of_gt}$.
Forward: assume $\mathrm{cmp}(a,b) = \mathrm{gt}$. Unfold the definition of $\mathrm{cmp}$. If $a$ and $b$ are balanced, simplification contradicts the $\mathrm{gt}$ hypothesis. Otherwise case on whether $(b-a)$ has nonnegativity flag true: the true branch again contradicts by simplification. In the false branch, rewrite via the $\mathrm{toInt}$ characterization of strict order; force the flag to false by exhaustive cases on the Bool; transport through the flag-false-iff and subtraction-toInt identities; close the resulting integer inequality with omega.
why it matters
This biconditional is the workhorse that lets later order lemmas case-split on $\mathrm{cmp}$ and recover a strict inequality (or the reverse). Downstream it feeds left and right translation invariance of $\mathrm{cmp}$ under addition, congruence of $\mathrm{cmp}$ under balanced replacements, sign-sensitive multiplication rules (negative flag reverses order; nonnegative nonzero flag preserves it), and the negation-swap identity for $\mathrm{cmp}$.
In the Recognition stack this sits in the foundation layer that reconstructs integer order from primitive recognition data, before the forcing chain (T5 J-uniqueness through T8 dimension) and the Recognition Composition Law are applied to physics. Closing the $\mathrm{cmp}\leftrightarrow\mathrm{lt}$ dictionary keeps arithmetic lemmas from leaking verifier integers into the internal PRC order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.