lt
plain-language theorem explainer
Defines the strict order on PRC rationals by declaring a < b exactly when the difference b − a is positive in the ratio-orbit sense. Anyone building ordered-field or Cauchy-real structure on the PRC stack cites this. The body is a one-line abbreviation of RationalField.positive on the gap.
Claim. For PRC rationals $a,b$ (ratio-orbit quotient classes), write $a < b$ if and only if $b-a$ is positive: its signed numerator is nonnegative and not balanced with zero.
background
PRC rationals are the quotient of ratio orbits by cross-multiplication equivalence (nonzero-denominator displays). They sit above signed orbits and LogicNat in the Primitive Recognition Calculus stack, which rebuilds arithmetic from recognition primitives rather than classical ZF naturals.
Positivity on a ratio orbit means the signed numerator is nonnegative and not balanced with zero. That predicate lives in RationalField and is the only ingredient here. Upstream, strict order on LogicNat is existential successor-gap, and on signed orbits it is nonnegative nonzero difference; this definition lifts the same idea to the rational quotient.
The ambient module RealCauchy develops Cauchy sequences and completeness over these rationals, so a native $<$ is required before gaps, square gaps, and J-cost distances can be stated.
proof idea
Pure definition: no proof obligations. The predicate is identified with positive (b - a), using field subtraction on PRCRat and the RationalField positivity test on the resulting ratio orbit.
why it matters
This is the order atom for the PRC rational field inside the real-construction path. Downstream order lemmas (additivity of $<$, comparison selectors, antisymmetry patterns in ArithmeticFromLogic and IntegerOrder) and the many RealCauchy siblings (square gap, J-cost distance, Cauchy sequences, null equivalence) all route through it.
In the Recognition forcing chain the calculus must eventually support the J-cost $J(x)=(x+x^{-1})/2-1$ and the phi-ladder; a native strict order on the rational substrate is the first step toward ordered completeness and continuous structure. Without it, defect distances and Cauchy limits cannot be phrased inside the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.