Reference · Non-negative rationals

rainbow.math.rational.nnrat.positive

Non-negative rationalssrc/rainbow/math/rational/nnrat/positive.clj1 definitions, 10 theorems

Constructive strict positivity for exact nonnegative rationals. A nonnegative rational is positive exactly when its numerator is a positive natural. This representation-facing definition is executable and avoids quotient reasoning. Positivity is invariant under exact-rational equivalence, and addition, multiplication, division, and minimum preserve it. These are the algebraic prerequisites for full-support Hastings reachability. Native, kernel-checked, and axiom-free on D63.

nnrat/positive :
  (x₁ : ℚ≥0)
  → Prop

nnrat/one-positive :
  → nnrat/positive 1

nnrat/multiply-positive :
  (left right : ℚ≥0) (left-positive : nnrat/positive left)
  (right-positive : nnrat/positive right)
  → nnrat/positive (left · right)

nnrat/positive-respects-equivalence :
  (left right : ℚ≥0)
  (same : left = right)
  (left-positive : nnrat/positive left)
  → nnrat/positive right

nat/add-positive-left :
  (left right : ℕ) (left-positive : nat/strict-below 0 left)
  → nat/strict-below 0 (algebra/nat-add left right)

nnrat/denominator-positive :
  (value : ℚ≥0)
  → nat/strict-below 0 (nnrat/denominator value)

nnrat/add-positive-left :
  (left right : ℚ≥0) (left-positive : nnrat/positive left)
  → nnrat/positive (left + right)

nnrat/add-positive-right :
  (left right : ℚ≥0) (right-positive : nnrat/positive right)
  → nnrat/positive (left + right)

nnrat/min-positive :
  (left right : ℚ≥0) (left-positive : nnrat/positive left)
  (right-positive : nnrat/positive right)
  → nnrat/positive (minmax/min left right)

nnrat/reciprocal-positive :
  (value : ℚ≥0)
  → nnrat/positive (nnrat/reciprocal value)

nnrat/divide-positive-left :
  (left right : ℚ≥0) (left-positive : nnrat/positive left)
  → nnrat/positive (nnrat/divide left right)