leQ_total

In the primitive recognition calculus, a rational orbit is a pair of a signed orbit (numerator) and a nonzero distinction-nat (denominator). The module equips these with the classical cross-multiplication order: $p \le q$ means the signed product of $p$'s numerator with $q$'s denominator (cast via SignedOrbit.ofOrbit) is $\le$ the swapped product, using the choice-free signed-orbit order.

That underlying order already has a totality theorem: for any two signed orbits $a,b$, either $a \le b$ or $b \le a$, proved by reducing to a comparison of natural images and a finite omega case split. The present result lifts that fact from signed orbits to rational orbits by definition of the cross-product comparison.

Local setting is the grow layer that builds ordered structure on ratio orbits without classical choice, feeding later trichotomy and field axioms.

One-line wrapper. Unfold the definition of the rational order (cross-multiplication of numerators and cast denominators). The goal becomes totality of signed-orbit order on those two products, which is exactly the upstream choice-free totality lemma applied to the two cross-products.

Totality is the missing half of a preorder that becomes a total order once reflexivity and the rest of the order axioms are in place. Downstream, the strict-order trichotomy theorem cases on this result: from $p \le q$ or $q \le p$ it splits on cross-equality to obtain $p < q$, equality of cross-products, or $q < p$. That trichotomy is the ordered backbone for comparing phi-ladder rungs and mass ratios once rationals are embedded in the recognition calculus. In the forcing chain this sits in the foundation layer beneath cost uniqueness and the J-functional, not yet at T5–T8, but it is the arithmetic substrate those steps assume when they compare dimensionless ratios.