ltQ
plain-language theorem explainer
Strict order on ratio orbits: p is strictly below q when the cross-multiplication weak order holds and the two orbits are not cross-equivalent. Cited by anyone proving trichotomy, irreflexivity, mediant density, or positivity of products on the PRC rational display. One-line definition combining the weak order with negated cross-equality.
Claim. For ratio orbits $p$ and $q$, declare $p < q$ if and only if $p \le q$ under the cross-multiplication order and $p$ is not cross-equivalent to $q$ (i.e., the signed products $p_{\mathrm{num}}\cdot q_{\mathrm{den}}$ and $q_{\mathrm{num}}\cdot p_{\mathrm{den}}$ are not balanced).
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator: the internal display of a rational before any real embedding. Cross-equivalence equates two ratio orbits when the signed products of numerator with the other's denominator balance; this is the PRC-native stand-in for rational equality.
The weak order leQ compares those same cross-products via the signed-orbit order: $p \le q$ means the signed orbit $p_{\mathrm{num}}\cdot q_{\mathrm{den}}$ is at most $q_{\mathrm{num}}\cdot p_{\mathrm{den}}$. The present definition turns that weak order into a strict order by excluding the equality case.
The surrounding Grow modules develop order, density, and multiplicative positivity for these displays, all without leaving the orbit language.
proof idea
Pure definitional abbreviation: strict order is the conjunction of the already-defined cross-multiplication weak order with the negation of cross-equivalence. No tactic steps and no lemmas are applied at the definition site; downstream theorems unfold this conjunction and discharge each conjunct separately.
why it matters
This is the strict order primitive for the entire Grow development on ratio orbits. Immediate consumers include irreflexivity and trichotomy in the same module, the mediant-density pair (strict inequalities sandwich the mediant), and the multiplicative-positivity facts (product of two positive ratio orbits is positive; zero-strictly-below characterized by numerator sign). Those results feed the denseness and ordered-field scaffolding that later connect PRC rationals to the recognition cost calculus. No forcing-chain landmark (T5–T8) is touched directly; the declaration is pure ordered-arithmetic infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.