le_iff_toInt_le
plain-language theorem explainer
Internal order on signed orbit differences coincides with ordinary integer comparison under the verifier display map. Anyone assembling the ordered-ring laws on ratio orbits cites this bridge. The proof unfolds difference-nonnegativity, applies the nonnegativity display lemma and the subtraction homomorphism, then closes by omega on ℤ.
Claim. For signed orbit differences $a,b$ (pairs of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$), the internal order holds, $a\le b$, if and only if the integer displays satisfy $a^{\mathrm{toInt}}\le b^{\mathrm{toInt}}$. Internally $a\le b$ means the difference $b-a$ is nonnegative.
background
Signed orbits are the K4.6 integer layer of the primitive recognition calculus: a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, intended as the difference $\mathrm{pos}-\mathrm{neg}$. The verifier map $\mathrm{toInt}$ recovers an ordinary $\mathbb{Z}$ value from that pair (via the LogicInt recovery map upstream).
Internal order is defined without classical choice: $a\le b$ means $\mathrm{nonneg}(b-a)$, i.e. the difference is a nonnegative signed orbit. Nonnegativity itself is witnessed by balance against a pure positive orbit. The companion lemma $\mathrm{nonneg}\leftrightarrow 0\le\mathrm{toInt}$ already equates that internal flag with the integer display; subtraction is a $\mathrm{toInt}$-homomorphism, $(\mathrm{sub},a,b)^{\mathrm{toInt}}=a^{\mathrm{toInt}}-b^{\mathrm{toInt}}$.
The module sits in the foundation stack that builds integers and rationals from recognition orbits before any continuum structure is assumed.
proof idea
Term-mode bridge, four lines. Unfold the internal order to $\mathrm{nonneg}(\mathrm{sub},b,a)$. Rewrite with the upstream nonnegativity display lemma and the subtraction homomorphism $\mathrm{sub_toInt}$, obtaining the pure integer comparison $0\le b^{\mathrm{toInt}}-a^{\mathrm{toInt}}$. Split the biconditional and finish each direction by omega on $\mathbb{Z}$.
why it matters
This is the purified choice-free order bridge from signed orbits to $\mathbb{Z}$. Downstream ratio-orbit order theorems route through it almost exclusively: transitivity and antisymmetry of the cross-multiplication order $\mathrm{leQ}$, the negation-reversal law, the zero-nonnegativity characterization, and right-multiplication monotonicity for nonnegative ratios all rewrite $\mathrm{le}$ via this lemma before cancelling in $\mathrm{Int}$. Integer-order facts such as absolute-value sandwich bounds also depend on it. In the Recognition stack it closes the integer comparison layer needed before the rational ordered-ring laws and, further up, the forcing chain's arithmetic scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.