trichotomy
plain-language theorem explainer
Any two signed orbits are comparable: either the first is strictly less than the second, they balance (same integer value), or the second is strictly less. Order theorists and anyone building positivity or root-selection arguments on the PRC integer layer cite this. The proof rewrites both relations to ordinary integer comparison via the toInt bridge, then closes by omega.
Claim. For any two signed orbits $a$ and $b$, either $a < b$, or $a$ and $b$ are balanced (equivalent integer displays), or $b < a$.
background
In the Primitive Recognition Calculus, integers are carried as signed orbits: pairs of nonnegative orbit lengths (positive and negative legs). Two orbits are balanced when $a.pos + b.neg = b.pos + a.neg$; this is the internal equality relation on the PRC integer layer. The strict order is the nonnegative difference that is not balanced.
Both relations are bridged to the ordinary verifier integers: balanced holds exactly when $a.toInt = b.toInt$, and $a < b$ holds exactly when $a.toInt < b.toInt$. Those characterizations (K4.9 and the companion order lemma) let classical integer facts transfer without leaving the orbit language.
This module develops the order theory on signed orbits (reflexivity, transitivity, antisymmetry under balance, totality, and the sign-flag laws). Trichotomy is the exclusive three-way split that underwrites later positivity and selection arguments.
proof idea
Rewrite the goal with the two bridge lemmas: strict order becomes $a.toInt < b.toInt$, and balance becomes $a.toInt = b.toInt$ (applied on both order directions). The resulting statement is ordinary integer trichotomy on $toInt$, which omega discharges in one step. No case split on orbit constructors is needed.
why it matters
Trichotomy is the comparison engine for the PRC integer layer. Downstream it feeds golden-integer root exclusivity (golden_roots, posPair_not_neg), the real sign bridge (posPair_real_pos), and the maximal-forcing selection stack: positivity selection of the expanding root $\varphi$, the mass-ladder universe certificate, and continuum-weight forcing. In RS terms it supports the T6 fixed-point story (choosing the expanding self-similar root) and the crown trichotomy language (Forced / Independent / Selected) used in MaximalForcing. Without a clean three-way split on signed orbits, positivity cannot lawfully pick $\varphi$ over $\psi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.