leQ
plain-language theorem explainer
Cross-multiplication order on rational orbits: p is at most q when the signed product of p's numerator with q's denominator is ≤ the swapped product. Anyone assembling an ordered field of rationals from δ-orbits cites this relation. It is a pure definition lifting the classical cross-product test through the choice-free signed-orbit order.
Claim. For rational orbits $p=(n_p,d_p)$ and $q=(n_q,d_q)$ (signed-orbit numerator over nonzero distinction denominator), set $p\le_Q q$ iff $n_p\cdot\iota(d_q)\le n_q\cdot\iota(d_p)$ in the signed-orbit order, where $\iota$ embeds a positive distinction as the nonnegative signed orbit $\langle d,0\rangle$.
background
A rational orbit is an integer-over-nonzero-orbit display: numerator a signed orbit, denominator a nonzero distinction natural. Signed orbits are differences $\mathrm{pos}-\mathrm{neg}$ of distinction naturals; their internal order declares $a\le b$ when $b-a$ is nonnegative.
Positive denominators enter the comparison via the embedding that builds a nonnegative signed orbit $\langle n,0\rangle$ from a distinction position. The signed-orbit order itself is choice-free and ultimately rests on the LogicNat order (existence of a witness summand).
This definition lives in the Primitive Recognition Calculus grow layer, which builds ordered rational structure from orbit data without classical choice or an ambient $\mathbb{Q}$.
proof idea
Pure definition with no proof obligations. The body is the classical cross-multiplication test: compare the signed-orbit product of $p$'s numerator with the embedded denominator of $q$ against the swapped product, using the existing signed-orbit non-strict order. No lemmas are applied at the definition site; downstream theorems unfold this and invoke choice-free reflexivity, totality, and the toInt bridge.
why it matters
This is the order relation on which the entire rational-orbit order theory hangs. Immediate parents include reflexivity (via choice-free signed-orbit reflexivity at identical cross-products), totality (via choice-free signed-orbit totality on the two cross-products), transitivity (multiply through by outer positive denominators and cancel), and antisymmetry up to cross-product equivalence. The strict order, negation compatibility, positivity criteria, and mediant/density comparisons all unfold this definition.
In the Recognition foundation it is the bridge from signed-orbit arithmetic to a total preorder on rational displays, feeding ordered arithmetic built from recognition primitives rather than from set-theoretic $\mathbb{Q}$. It sits upstream of the denseness and ladder constructions that later connect to the phi-ladder mass and cost calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.