Reference · Signed rationals

rainbow.math.rational.signed.minmax-algebra

Signed rationalssrc/rainbow/math/rational/signed/minmax_algebra.clj0 definitions, 8 theorems

Algebraic and monotonicity laws for signed extrema. Signed rationals are quotient-like Grothendieck pairs, so algebraic laws are stated with signed/equivalent rather than structural equality. The lattice bounds from rainbow.math.rational.signed.minmax and order transitivity prove: min/max commutativity, idempotence, monotonicity, and associativity. Each equivalence is obtained by antisymmetry after proving the two order directions. No arithmetic representation is unfolded here: this is exactly the reusable structural layer that robust aggregation, dynamic programming, and finite extrema can depend on. Native and axiom-free on D63.

Depends onmath.rational.signed.limit-uniquenessmath.rational.signed.minmax

signed/min-commutative :
  (left right : ℚ)
  → signed/min left right = signed/min right left

signed/max-commutative :
  (left right : ℚ)
  → signed/max left right = signed/max right left

signed/min-idempotent :
  (value : ℚ)
  → signed/min value value = value

signed/max-idempotent :
  (value : ℚ)
  → signed/max value value = value

signed/min-monotone :
  (left right left-prime right-prime : ℚ)
  (left-order : left ≤ left-prime)
  (right-order : right ≤ right-prime)
  → signed/min left right ≤ signed/min left-prime right-prime

signed/max-monotone :
  (left right left-prime right-prime : ℚ)
  (left-order : left ≤ left-prime)
  (right-order : right ≤ right-prime)
  → signed/max left right ≤ signed/max left-prime right-prime

signed/min-associative :
  (a b c : ℚ)
  → signed/min (signed/min a b) c = signed/min a (signed/min b c)

signed/max-associative :
  (a b c : ℚ)
  → signed/max (signed/max a b) c = signed/max a (signed/max b c)