Reference · Non-negative rationals

rainbow.math.rational.nnrat.order-nontrivial

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

Constructive impossibility of 1 <= 0 and of k+1 <= k+0 in nnrat order. These give reusable negative certificates for infeasible constant LP rows. The first proof extracts a natural slack from cross-product order and derives successor(extra)=0. The second cancels the arbitrary common summand k. No classical principle or new axiom is used.

Depends onmath.rational.nnrat.add-monotonemath.rational.nnrat.add-cancellation

nnrat/one-not-at-most-zero :
  (h₁ : 1 ≤ 0)
  → proposition/falsity

nnrat/common-add-unit-gap-impossible :
  (k : ℚ≥0)
  (h₁ : k + 1 ≤ k + 0)
  → proposition/falsity