Reference · Signed rationals

rainbow.math.rational.signed.order-transitivity

Signed rationalssrc/rainbow/math/rational/signed/order_transitivity.clj0 definitions, 1 theorems

Real-analysis roadmap step 4: transitivity of the signed-rational order. signed/at-most a b is the additive comparison pos(a) + neg(b) <= pos(b) + neg(a) (nnrat order, no primitive subtraction). Transitivity is the classic argument, now fully mechanizable because every ingredient exists: a<=b : Pa+Nb <= Pb+Na b<=c : Pb+Nc <= Pc+Nb add them (nnrat/add-monotone) : (Pa+Nb)+(Pb+Nc) <= (Pb+Na)+(Pc+Nb) reorder both sides so the shared (Pb+Nb) is isolated (nnrat/add-four-reorder + add-commutative, transported by add-/at-most-respects-equivalence) : (Pa+Nc)+(Pb+Nb) <= (Pc+Na)+(Pb+Nb) cancel the shared summand (step-3 nnrat/at-most-add-right-cancel) : Pa+Nc <= Pc+Na == a<=c. This is the gate to signed min/max/abs and the epsilon-N convergence predicate. Native and axiom-free; chains nnrat-add-monotone, nnrat-add-cancellation, and nnrat-additive-reassociation on d63.

Depends onmath.rational.nnrat.add-monotonemath.rational.nnrat.add-cancellationmath.rational.nnrat.additive-reassociation

signed/at-most-transitive :
  (a b c : ℚ)
  (h1 : a ≤ b)
  (h2 : b ≤ c)
  → a ≤ c