lt_iff_toRat_lt
plain-language theorem explainer
Internal strict order on PRC rationals agrees with ordinary rational order under the verifier display map toRat. Anyone moving Cauchy, boundedness, or J-cost estimates between the ledger and Mathlib ℚ cites this bridge. Proof unfolds order as positivity of a difference, rewrites by the positivity and subtraction transport lemmas, and closes both directions by linear arithmetic.
Claim. For PRC rationals $a,b$, the internal strict order holds if and only if the ordinary rational displays satisfy $\mathrm{toRat}(a)<\mathrm{toRat}(b)$ in $\mathbb{Q}$.
background
PRC rationals are the K4.8 quotient of ratio-orbit displays (nonzero-denominator pairs of signed orbits, identified by cross-multiplication). The verifier map toRat sends each class to an ordinary Mathlib rational by integer numerator over natural denominator; it is a pure transport wrapper whose internal characterization is cross-multiplication.
Strict order on the ledger is defined by positivity of a difference: $a<b$ means the difference $b-a$ is positive in the internal sense. Upstream, positivity itself is already known to match ordinary positivity after display (positive_iff_toRat_pos), and subtraction is known to commute with display (toRat_sub: $(a-b)^{\mathrm{to}}=a^{\mathrm{to}}-b^{\mathrm{to}}$).
This module sits in the Primitive Recognition Calculus real-construction layer: rationals are already built from logic-level arithmetic, and Cauchy ledgers / J-cost distances are about to be ordered and completed. The local job is to make the internal order interchangeable with Mathlib's order on ℚ.
proof idea
Term/tactic hybrid, short. Unfold the internal lt (positivity of a difference). Rewrite the positivity claim by positive_iff_toRat_pos, then replace the internal difference by ordinary subtraction via sub_eq and toRat_sub. The goal is then the elementary equivalence $0 < b^{\mathrm{to}}-a^{\mathrm{to}} \leftrightarrow a^{\mathrm{to}} < b^{\mathrm{to}}$. Split into both directions and finish each with linarith. No induction and no quotient induction: pure transport plus arithmetic.
why it matters
This is the order-transport hinge for the entire PRC real layer. Downstream it is applied to prove that a positive ledger element is strictly above zero (zero_lt_of_positive), that unit fractions eventually fall below any positive epsilon (PRCUnitFraction_eventually_lt), that small J-cost distance forces squared display increments below one (PRCJCostDistance_sq_diff_lt_one_of_lt_boundedness_delta and the order-congruence variant), and that Cauchy ledgers are eventually bounded in a symmetric rational interval. The triangle-modulus target for J-cost distance is likewise closed by display transport that routes through this comparison.
In the Recognition stack this is foundation plumbing, not a physics landmark: it lets later forcing-chain and cost-geometry arguments reason in Mathlib ℚ while staying honest to the internal ledger. Without it, every Cauchy, completeness, and continuity lemma would have to re-prove order compatibility by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.