Reference · Signed rationals

rainbow.math.rational.signed.rate-order

Signed rationalssrc/rainbow/math/rational/signed/rate_order.clj0 definitions, 2 theorems

Order closure under vanishing signed-rational error bounds. The Archimedean theorem turns `x <= y + 1/(k+1)` for every natural k into `x <= y`. Its rate-null corollary accepts any nonnegative signed error sequence with an explicit modulus. These are reusable limit/order lemmas; they do not assume completeness or construct limits. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-signed-value-iteration-general-convergesmath.rational.signed.limit-uniquenessmath.rational.signed.additive-distancemath.rational.nnrat.ring

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

analysis/signed-at-most-of-rate-null-upper-bounds :
  (error : ℕ → ℚ) (modulus : ℕ → ℕ) (x y : ℚ)
  (null : analysis/signed-rate-null error modulus)
  (bounded : ∀ (steps : ℕ), x ≤ y + error steps)
  → x ≤ y