IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLtTrichotomy
Defines the strict cross-multiplication order on ratio orbits and proves it is irreflexive and trichotomous against cross-equality. Anyone arguing density, positivity, or ordered arithmetic on the rational orbit lattice cites the trichotomy lemma. The development reduces strict comparison to signed integer-orbit order and reuses the weak order's reflexivity and totality.
claimOn ratio orbits $p,q$, write $p <_{\mathbb{Q}} q$ when the signed cross product $p_{\mathrm{num}}\cdot q_{\mathrm{den}}$ is strictly less than $q_{\mathrm{num}}\cdot p_{\mathrm{den}}$ in the integer-orbit order. The relation is irreflexive. Cross-equality of those products is decidable, and for every pair exactly one of $p <_{\mathbb{Q}} q$, cross-equality, or $q <_{\mathbb{Q}} p$ holds.
background
This module sits in the Primitive Recognition Calculus grow layer, where positive distinctions are packaged as orbits and rational comparisons are realized without classical $\mathbb{Q}$ as a primitive. The weak order from the imported ratio-orbit module says $p \le_{\mathbb{Q}} q$ iff the signed orbit $p.num * q.den$ is $\le$ the signed orbit $q.num * p.den$, dens cast in via SignedOrbit.ofOrbit.
Integer order and integer-rational scaffolding supply the underlying strict and non-strict comparisons on those signed cross products. The present module introduces the strict companion relation and the equality case of the cross products, so ordered arguments can case-split cleanly.
Notation: ratio orbits carry numerator and denominator orbits; cross-multiplication is the comparison engine throughout the grow stack.
proof idea
Definition module plus elementary order lemmas, not a deep derivation. The strict relation is the lift of integer-orbit $<$ on the two cross products. Irreflexivity is immediate from irreflexivity of that integer order. Decidability of cross-equality is inherited from the integer layer. Trichotomy packages the three mutually exclusive outcomes (strict less, cross-equal, strict greater) by combining integer trichotomy with the already-proved reflexivity and totality of the weak cross-multiplication order.
why it matters in Recognition Science
Strict order and trichotomy are the case-split engine for later grow lemmas. Downstream importers are the dense-mediant module (inserting mediants between unequal ratios), multiplicative positivity on ratio orbits, and the base fact that zero is strictly below one in this order. Without a proved trichotomy, density and positivity arguments cannot discharge the unequal case. In the broader Recognition foundation this is bookkeeping on the rational skeleton that later supports self-similar scaling and forcing-chain comparisons, not a physics claim by itself.
scope and limits
- Does not construct classical $\mathbb{Q}$ or prove isomorphism to Mathlib rationals.
- Does not prove density, mediant insertion, or multiplicative monotonicity; those are downstream.
- Does not address real completion, Archimedeanness, or continuum limits.
- Does not relate $<_{\mathbb{Q}}$ to J-cost, $\varphi$-ladder rungs, or physical constants.
- Does not claim decidability of arbitrary orbit equality beyond cross-product equality.