Reference · Signed rationals

rainbow.math.rational.signed.minmax

Signed rationalssrc/rainbow/math/rational/signed/minmax.clj2 definitions, 6 theorems

Universal minimum and maximum over signed rationals. The older validation/STL layer computes signed extrema under validation-specific aliases and proves only which operand is selected in one Boolean branch. This module exposes reusable signed/min and signed/max operations and proves their actual order laws for every pair of signed rationals: min a b <= a a <= max a b min a b <= b b <= max a b lo <= x, lo <= y -> lo <= min x y x <= hi, y <= hi -> max x y <= hi Each proof case-splits on signed/decide-at-most. Its true and false soundness theorems supply the only non-reflexive order fact needed in either branch. Native and axiom-free on D63.

Depends onmath.rational.signed.decide-order

signed/min :
  (x₁ x₂ : ℚ)
  → ℚ

signed/max :
  (x₁ x₂ : ℚ)
  → ℚ

signed/min-lower-left :
  (left right : ℚ)
  → signed/min left right ≤ left

signed/min-lower-right :
  (left right : ℚ)
  → signed/min left right ≤ right

signed/max-upper-left :
  (left right : ℚ)
  → left ≤ signed/max left right

signed/max-upper-right :
  (left right : ℚ)
  → right ≤ signed/max left right

signed/at-most-min :
  (lower left right : ℚ)
  (lower-left : lower ≤ left)
  (lower-right : lower ≤ right)
  → lower ≤ signed/min left right

signed/at-most-max :
  (left right upper : ℚ)
  (left-upper : left ≤ upper)
  (right-upper : right ≤ upper)
  → signed/max left right ≤ upper