Reference · Non-negative rationals

rainbow.math.rational.nnrat.order-scale

Non-negative rationalssrc/rainbow/math/rational/nnrat/order_scale.clj0 definitions, 5 theorems

Positive scaling and coefficient normalization for the nnrat order. Positivity is represented structurally: a positive coefficient has the form `nnrat/make (data/succ ap) adp`. The central cancellation proof descends from `nnrat/at-most` to its natural-number cross product, normalizes the product, and cancels the positive numerator and denominator factors. Division then turns upper and lower coefficient constraints into ordinary bound predicates. The proper-fraction rate-null law closes the family: a value at most a proper multiple of itself is equivalent to zero. Native and axiom-free on the d63 checkpoint.

Depends onmath.rational.nnrat.order-equivalencemath.rational.nnrat.multiply-monotonemath.rational.nnrat.multiply-commutemath.rational.nnrat.product-reassociationmath.rational.nnrat.identities

nnrat/at-most-multiply-left-cancel :
  (ap adp : ℕ) (v w : ℚ≥0)
  (ordered : nnrat/make (data/succ ap) adp · v ≤ nnrat/make (data/succ ap) adp · w)
  → v ≤ w

nnrat/multiply-divide-cancel :
  (ap adp : ℕ) (b : ℚ≥0)
  → nnrat/make (data/succ ap) adp · nnrat/divide b (nnrat/make (data/succ ap) adp) = b

nnrat/at-most-multiply-left-normalize-upper :
  (ap adp : ℕ) (v b : ℚ≥0)
  → proposition/conjunction (nnrat/make (data/succ ap) adp · v ≤ b → v ≤ divide) (v ≤ divide → nnrat/make (data/succ ap) adp · v ≤ b)
  where divide := nnrat/divide b (nnrat/make (data/succ ap) adp)

nnrat/at-most-multiply-left-normalize-lower :
  (ap adp : ℕ) (b v : ℚ≥0)
  → proposition/conjunction (b ≤ nnrat/make (data/succ ap) adp · v → divide ≤ v) (divide ≤ v → b ≤ nnrat/make (data/succ ap) adp · v)
  where divide := nnrat/divide b (nnrat/make (data/succ ap) adp)

nnrat/zero-of-proper-contraction :
  (np dp : ℕ) (x : ℚ≥0)
  (proper : np ≤ dp)
  (bounded : x ≤ nnrat/make np dp · x)
  → x = 0