Reference · Signed rationals

rainbow.math.rational.signed.scale-reflection

Signed rationalssrc/rainbow/math/rational/signed/scale_reflection.clj0 definitions, 2 theorems

Positive rational scaling reflects signed order. Together with explicit endpoint equivalences this transports a checked scaled bound to its original values. It does not assert that a host-language transformation produces those equivalences. Positivity is structural: make (succ ap) adp, never zero.

Depends onmath.rational.signed.scale-ordermath.rational.nnrat.order-scalemath.rational.signed.order-respects

signed/scale-positive-reflects-order :
  (ap adp : ℕ) (left right : ℚ)
  (ordered : signed/scale (nnrat/make (data/succ ap) adp) left ≤ signed/scale (nnrat/make (data/succ ap) adp) right)
  → left ≤ right

signed/scaled-bound-to-original :
  (ap adp : ℕ) (left right checked-left checked-right : ℚ)
  (left-same : checked-left = signed/scale (nnrat/make (data/succ ap) adp) left)
  (right-same : checked-right = signed/scale (nnrat/make (data/succ ap) adp) right)
  (checked-bound : checked-left ≤ checked-right)
  → left ≤ right