lt
plain-language theorem explainer
Internal strict order on signed orbits: a is less than b when the difference is nonnegative and nonzero. Integer-order development cites it for translation invariance of < and for the comparison selector. Defined directly as the weak order conjoined with unbalanced (nonzero difference).
Claim. For signed orbits $a,b$ (each a pair of distinction-nats read as $\mathrm{pos}-\mathrm{neg}$), declare $a<b$ if and only if $a\le b$ and $a$ is not balanced with $b$: the difference is nonnegative and nonzero.
background
A signed orbit is a pair of distinction-nats intended as $\mathrm{pos}-\mathrm{neg}$. The module builds integer arithmetic and order from these pairs without relying on a verifier integer display.
The weak order $\mathrm{le}$ on signed orbits is the nonnegative-difference relation (parallel to $\mathrm{le}$ on $\mathrm{LogicNat}$, which is existence of a summand). Balance means the two sides cancel: zero difference. Upstream ledger balance is the same idea at the event-list level; here it is specialized to a pair of orbits.
Strict order is then the standard cut of weak order by equality-as-balance: nonnegative and not balanced.
proof idea
Definitional, not a proof. The predicate is the conjunction of the existing weak order with negation of balance. No lemmas are applied; downstream theorems unfold this definition and rewrite with the corresponding facts about $\mathrm{le}$ and $\mathrm{balanced}$.
why it matters
This is the internal $<$ that IntegerOrder uses everywhere: left/right translation of strict inequality, the comparison selector $\mathrm{cmp}$ (eq when balanced, else branch on the nonnegative flag of the difference), and congruence of $\mathrm{cmp}$ under addition. It mirrors the LogicNat strict order in ArithmeticFromLogic, keeping the foundation's order story uniform from pure logic-nats up through signed orbits.
In the Recognition stack this sits under Primitive Recognition Calculus: integers as signed orbit differences, ordered before any real embedding or J-cost analysis. It does not itself force $\phi$, eight-tick structure, or $D=3$; it supplies the discrete order those later layers assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.