cmp_eq_gt_of_gt
plain-language theorem explainer
If signed orbit b is strictly less than a in the internal PRC order, the comparison selector returns Ordering.gt on the pair (a,b). Downstream order-congruence and signed-multiplication lemmas cite this direction of the cmp characterization. The proof bridges lt and balanced to the verifier integer display, discharges two flag facts by omega, then simp-unfolds cmp.
Claim. Let $a,b$ be signed orbits. If $b < a$ in the internal strict order (nonnegative nonzero difference), then the internal comparison selector satisfies $\mathrm{cmp}(a,b)=\mathrm{gt}$.
background
Signed orbits are the Primitive Recognition Calculus carriers for integers: each has positive and negative orbit lengths, with an internal equivalence balanced meaning $a.pos+b.neg=b.pos+a.neg$ (K4.9). That relation is proved equivalent to equality of the verifier display toInt.
Strict order lt is defined internally as the weak order plus failure of balance: nonnegative difference and not balanced. The comparison selector cmp is not taken from toInt; it is defined by cases on balance and the nonnegativity flag of sub b a: equal when balanced, lt when the difference is nonnegative and unbalanced, otherwise gt.
This lemma is the one-way implication from reverse strict order into the gt branch of that selector, inside the IntegerOrder development that builds a total order and arithmetic-compatible comparison on signed orbits from δ-orbit data alone.
proof idea
From lt b a, rewrite via lt_iff_toInt_lt and nonnegFlag_eq_false_iff plus sub_toInt to obtain (sub b a).nonnegFlag = false by omega on the integer display. Separately, the same toInt bridge with balanced_iff_toInt_eq yields ¬ balanced a b again by omega. With both side conditions in hand, simp on the definition of cmp selects the final else branch and closes with Ordering.gt.
why it matters
This is the forward half of the characterization later packaged as cmp_eq_gt_iff. It is the case-split fuel for translation-invariance (cmp_add_left, cmp_add_right), balance-congruence of comparison (cmp_congr_of_balanced), and the signed multiplication rules that reverse or preserve order according to the multiplier's sign flag (cmp_mul_left/right_of_negativeFlag and the nonnegative nonzero variants).
In the Recognition foundation stack, integers and their order are forced from recognition calculus rather than assumed as a primitive ℤ. A correct internal cmp that agrees with strict order is required before ledger arithmetic and later forcing steps can treat comparison as a pure function of orbit data. The lemma sits in that scaffolding: no T5–T8 physics claim, but a necessary order-theoretic brick under ArithmeticFromLogic and LedgerForcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.