cmp_eq_lt_of_lt
plain-language theorem explainer
If signed orbit a is strictly below b in the internal PRC order, the comparison selector returns Ordering.lt. Downstream order lemmas for addition, multiplication, and balanced congruence cite this one-way bridge from lt into cmp. The proof discharges the two branches of cmp via the toInt display bridge and omega on the resulting integer inequalities.
Claim. Let $a,b$ be signed orbits. If $a < b$ in the internal strict order (nonnegative difference and not balanced), then the internal comparison selector satisfies $\mathrm{cmp}(a,b)=\mathrm{lt}$.
background
Signed orbits are the PRC carriers for integers: each has positive and negative orbit lengths. Two orbits are balanced when $a.pos+b.neg=b.pos+a.neg$; that is the internal equality relation on $\delta$-orbit positions (K4.9). The verifier display toInt agrees with balance: balanced iff the displayed integers coincide.
Strict order is defined internally as the weak order plus not-balanced, equivalently a nonnegative nonzero difference. The comparison selector cmp is not taken from the verifier integer; it is defined by cases on balance and the nonnegativity flag of $b-a$: equal when balanced, lt when the difference is nonnegative and unbalanced, otherwise gt.
This lemma sits in the IntegerOrder layer that builds a total order and arithmetic-compatible comparison on those carriers, upstream of add/mul monotonicity.
proof idea
From $a<b$, rewrite via lt_iff_toInt_lt and balanced_iff_toInt_eq and apply omega to get $\neg$ balanced. Separately, rewrite the nonnegativity flag of $b-a$ through nonnegFlag_eq_true_iff and sub_toInt, again using the toInt form of lt, and omega to obtain the flag true. Unfold cmp and simp with those two facts to hit Ordering.lt.
why it matters
This is the forward half of the bridge between internal strict order and the Ordering-valued selector. It is consumed by cmp_eq_lt_iff (the full equivalence), by cmp_congr_of_balanced (comparison stable under balance), and by the left/right additivity lemmas cmp_add_left and cmp_add_right, which case-split on cmp and recover lt via this direction. Multiplication monotonicity under positive and negative flags (cmp_mul_left_of_nonnegFlag_..., cmp_mul_left_of_negativeFlag, and the right-sided twins) likewise pattern-match on cmp and re-enter through lt. In the Recognition foundation stack this keeps integer order native to signed-orbit data rather than smuggling classical $\mathbb{Z}$ comparison into the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.