le_total
plain-language theorem explainer
Any two signed-orbit differences are comparable under the internal nonnegative-difference order. Foundation proofs that case-split on order (arc covers, bad-sequence bounds, monotone d'Alembert) cite this totality. The argument rewrites both sides through the integer embedding and finishes by omega on ℤ.
Claim. For all signed orbit differences $a,b$ (pairs of distinction naturals read as $a=\mathrm{pos}-\mathrm{neg}$), either $a\le b$ or $b\le a$, where $a\le b$ means $b-a$ is nonnegative.
background
Signed orbits are the internal integer model in the primitive recognition calculus: a structure with two distinction-natural components, intended as $\mathrm{pos}-\mathrm{neg}$. Their order is defined by nonnegativity of the difference: $a\le b$ iff $\mathrm{sub},b,a$ is nonnegative.
That order is tied to ordinary integer comparison by a bridge lemma: $a\le b$ if and only if the integer image $a.\mathrm{toInt}$ is $\le$ $b.\mathrm{toInt}$. Upstream, non-strict order on logic naturals is the usual "exists a summand" relation; here the signed case inherits totality from $\mathbb{Z}$ once the embedding is in place.
The IntegerOrder module packages reflexivity, transitivity, antisymmetry, totality, and trichotomy for this surface so later certificates can treat signed orbits as a total order without reopening the embedding.
proof idea
Rewrite both disjuncts with the characterization that signed-orbit $\le$ is equivalent to $\le$ of the integer images. The goal becomes $a.\mathrm{toInt}\le b.\mathrm{toInt}$ or the reverse, which omega discharges on $\mathbb{Z}$. No separate case analysis on signs is written by hand.
why it matters
Totality is the missing order axiom that closes the signed-orbit order surface: it is listed among the fields assembled by the integer-order certificate. Downstream, arc-complement work uses it to split index comparisons in bad-sequence bounds and to cover the circle by the two semicircle ranges (comparing $0$ to an ambient coordinate). The monotone d'Alembert theorem that forces the cosh cost form (Recognition J-cost landmark, T5) relies on order case splits that need totality. Native-cost uniqueness and cut-pin lemmas in the PRC ledger likewise case on comparable traces. Without this fact, the internal integers would only be a preorder, blocking the Archimedean monotone path to $\cosh$ and the geometric covering arguments in high-dimensional linking.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.