IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLtTrichotomy
Defines the strict cross-multiplication order on ratio orbits and proves irreflexivity plus full trichotomy with equality. Anyone assembling ordered arithmetic inside the primitive recognition calculus cites this layer. The argument reduces strict comparison to the existing total preorder by deciding equality of signed cross products.
claimOn ratio orbits $p,q$, set $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}}$. Then $<_{\mathbb{Q}}$ is irreflexive, cross-equality is decidable, and for every pair exactly one of $p <_{\mathbb{Q}} q$, $p=q$, or $q <_{\mathbb{Q}} p$ holds.
background
Ratio orbits are the primitive stand-in for rational values in the recognition calculus: each carries a numerator orbit and a positive denominator orbit. The sibling module on the non-strict order already equips them with $p \le_{\mathbb{Q}} q$ by comparing signed cross products $p_{\mathrm{num}}\cdot q_{\mathrm{den}}$ and $q_{\mathrm{num}}\cdot p_{\mathrm{den}}$ after casting positive distinctions through signed orbits.
Integer order and integer-rational scaffolding supply the underlying comparison and arithmetic on those signed products. This module sits in the Grow layer that builds ordered field structure from those primitives, before density and positivity lemmas.
The strict relation is the natural open companion of that preorder: same cross-multiplication test, strict inequality of signed orbits.
proof idea
The module introduces the strict predicate by flipping the non-strict cross-multiplication comparison to a strict signed-orbit inequality. Irreflexivity is immediate from irreflexivity of the integer strict order on equal cross products.
Decidability of cross-equality (whether the two signed products agree) is recorded so case splits are lawful. Trichotomy then follows the classical pattern: compare the two signed cross products; the integer trichotomy yields less, equal, or greater, which translate to $p<q$, definitional equality of the rational representatives, or $q<p$.
why it matters in Recognition Science
Trichotomy is the hinge that lets later Grow lemmas treat ratio orbits as a totally ordered set rather than a mere preorder. Downstream modules import it for density via mediants, positivity of products of positive ratios, and the base fact $0<1$.
Without a strict, irreflexive, trichotomous order, mediant-density arguments cannot separate distinct orbits, and sign lemmas cannot open strict cones. In the broader Recognition stack this is still pre-physics bookkeeping: it underwrites the discrete rational skeleton on which continuous recognition costs and the forcing chain later sit, but it does not yet mention $J$, $\varphi$, or the eight-tick octave.
scope and limits
- Does not construct addition or multiplication morphisms on ratio orbits.
- Does not prove density, archimedeanness, or completeness of the order.
- Does not identify ratio orbits with classical rationals or prove a field isomorphism.
- Does not address $J$-cost, $\varphi$-ladder rungs, or any physical constant.
- Does not discharge positivity of denominators beyond what the imported orbit casts already assume.