Reference · Non-negative rationals

rainbow.math.rational.nnrat.order-equivalence

Non-negative rationalssrc/rainbow/math/rational/nnrat/order_equivalence.clj0 definitions, 2 theorems

Real-analysis roadmap step 2: the nnrat closure<->base order equivalence. nnrat/at-most is the church-encoded reflexive-transitive closure of the cross-product order nnrat/base-at-most (base-at-most a b = num a * den b <= num b * den a). The forward direction nnrat/at-most-from-cross (base -> closure) is already in d63. Here we prove the two missing pieces: nnrat/base-at-most-transitive : base a x -> base x y -> base a y nnrat/at-most-to-cross : nnrat/at-most a b -> nnrat/base-at-most a b base-at-most transitivity is the payoff of step-1 nat multiplicative cancellation: scale the two cross-products by the opposite denominators (multiply-right-monotone), reorder the degree-3 monomials with the nat-ring tactic, chain, then cancel the shared positive factor den_x = succ(dpre x) with nat/at-most-multiply-right-cancel. The reverse closure->base then instantiates the closure recursor at P := (base a _), with base-reflexivity for the base case and base-transitivity for the step. Together with at-most-from-cross this makes the nnrat order decidable/cancellable at the base level -- the gateway to nnrat additive at-most cancellation (step 3) and signed order transitivity (step 4). Native and axiom-free; chains rainbow.math.nat.at-most-cancellation (-> nat-ring) on d63.

Depends onmath.nat.at-most-cancellation

nnrat/base-at-most-transitive :
  (a x y : ℚ≥0) (ax : nnrat/base-at-most a x) (xy : nnrat/base-at-most x y)
  → nnrat/base-at-most a y

nnrat/at-most-to-cross :
  (a b : ℚ≥0)
  (h : a ≤ b)
  → nnrat/base-at-most a b