ltQ_trichotomy
plain-language theorem explainer
Any two ratio orbits are comparable under the strict order: either the first is strictly below the second, they agree by cross-multiplication, or the second is strictly below the first. Anyone building ordered arithmetic on PRC rationals cites this. The proof splits on totality of the weak order, then cases on whether the two orbits are cross-equal.
Claim. For any two ratio orbits $p,q$ (integer numerator over nonzero orbit denominator), either $p<q$, or $p$ and $q$ are equivalent under cross-multiplication balance of scaled numerators, or $q<p$. Here $p<q$ means $p\le q$ and the two orbits are not cross-equal.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed orbit numerator over a nonzero distinction-nat denominator. Equality of two such displays is not raw structural equality; it is the internal relation crossEq (K4.10): the scaled products of numerator and opposite denominator balance as signed orbits. That is the PRC stand-in for ordinary rational equality.
The weak order leQ on ratio orbits is defined via comparison of those same cross-products. Totality of leQ is already proved: for any $p,q$, either $p\le q$ or $q\le p$, by totality of the underlying comparison on cross-products. The strict order is the usual cut: $p<q$ means $p\le q$ and not cross-equal.
This module sits in the Grow layer that equips ratio orbits with a reflexive, total, and (here) trichotomous order, all stated entirely on $\delta$-orbit positions rather than on classical $\mathbb{Q}$.
proof idea
Apply totality of the weak order to obtain either $p\le q$ or $q\le p$.
In the first branch, case on whether $p$ and $q$ are cross-equal. If yes, land in the middle disjunct. If no, the pair $(p\le q,,\neg\mathrm{crossEq})$ is exactly the definition of $p<q$, so the left disjunct.
In the second branch, case on whether $q$ and $p$ are cross-equal. If yes, symmetrize cross-equality to get $p$ cross-equal $q$, again the middle disjunct. If no, the pair $(q\le p,,\neg\mathrm{crossEq},q,p)$ is $q<p$, the right disjunct.
No further arithmetic is needed; the argument is pure case analysis on totality plus the definition of the strict order.
why it matters
Trichotomy is the missing order axiom once reflexivity, totality of $\le$, and the strict cut are in place. It lets later PRC development treat ratio orbits as a linearly ordered field of displays without smuggling classical $\mathbb{Q}$ comparison.
No downstream consumers are wired in the graph yet (used_by is empty), so the lemma is presently a leaf in the Grow order stack. Its natural parents are any uniqueness, density, or monotonicity results for costs and ladders that quantify over ordered rationals (native cost uniqueness, rung comparisons, mass-ladder inequalities).
Within the broader Recognition chain this is pure foundation: it does not touch J-uniqueness, $\varphi$, the eight-tick octave, or $D=3$, but it supplies the ordered arithmetic those later forcing steps assume when they speak of rational displays and cross-product balance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.