Reference · Non-negative rationals

rainbow.math.rational.nnrat.archimedean

Non-negative rationalssrc/rainbow/math/rational/nnrat/archimedean.clj0 definitions, 1 theorems

The Archimedean reciprocal limit helper for nonnegative rationals. If x <= y + 1/(k+1) for every natural k, then x <= y. At the cross-product level, choose k = den(y)*den(x). If A = num(x)*den(y), B = num(y)*den(x), K = den(y)*den(x), and M = succ K, the chosen hypothesis normalizes to M*A <= M*B + K. Decidability of A <= B closes the positive branch. In the negative branch, B <= A has a witness B+d=A. The zero case is equality; a successor witness forces M <= K, i.e. succ K <= K, contradicting nat/not-equal-successor-add. Native and axiom-free; chains nnrat-order-equivalence, nat at-most cancellation, and the nat-ring proof-term generator on the D63 checkpoint.

Depends onmath.rational.nnrat.order-equivalence

nnrat/at-most-of-all-plus-reciprocal :
  (x y : ℚ≥0)
  (bounded : ∀ (k : ℕ), x ≤ y + nnrat/make 1 k)
  → x ≤ y