Reference · Signed rationals

rainbow.math.rational.signed.clamp

Signed rationalssrc/rainbow/math/rational/signed/clamp.clj1 definitions, 7 theorems

Projection of a signed rational into a closed interval. clamp lower upper value = min (max lower value) upper For every ordered interval lower <= upper, the result lies in the interval. Values already in the interval are preserved up to signed equivalence; values below or above it saturate at the corresponding endpoint. Clamp is monotone in its value argument without any interval hypothesis, and respects signed equivalence in all three inputs. These are structural lattice proofs over signed min/max. They do not unfold rational arithmetic and introduce no axiom, making the operator reusable by projected optimization, box constraints, trust regions, and bounded monitors. Native and axiom-free on D63.

Depends onmath.rational.signed.minmax-algebra

signed/clamp :
  (x₁ x₂ x₃ : ℚ)
  → ℚ

signed/clamp-lower :
  (lower upper value : ℚ)
  (ordered : lower ≤ upper)
  → lower ≤ signed/clamp lower upper value

signed/clamp-upper :
  (lower upper value : ℚ)
  → signed/clamp lower upper value ≤ upper

signed/clamp-in-band :
  (lower upper value : ℚ)
  (above-lower : lower ≤ value)
  (below-upper : value ≤ upper)
  → signed/clamp lower upper value = value

signed/clamp-monotone :
  (lower upper left right : ℚ)
  (ordered : left ≤ right)
  → signed/clamp lower upper left ≤ signed/clamp lower upper right

signed/clamp-respects-equivalence :
  (lower lower-prime upper upper-prime value value-prime : ℚ)
  (lower-same : lower = lower-prime)
  (upper-same : upper = upper-prime)
  (value-same : value = value-prime)
  → signed/clamp lower upper value = signed/clamp lower-prime upper-prime value-prime

signed/clamp-below :
  (lower upper value : ℚ)
  (ordered : lower ≤ upper)
  (below : value ≤ lower)
  → signed/clamp lower upper value = lower

signed/clamp-above :
  (lower upper value : ℚ)
  (ordered : lower ≤ upper)
  (above : upper ≤ value)
  → signed/clamp lower upper value = upper