Reference · Signed rationals

rainbow.math.rational.signed.multiply-monotone

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

Scaling a signed inequality by a nonnegative signed scalar. signed/multiply-left-monotone : 0 <= c -> a <= b -> c*a <= c*b signed/multiply-right-monotone : 0 <= c -> a <= b -> a*c <= b*c This is the keystone the signed layer was missing: the additive toolkit could add an inequality to something, and the sign rules could decide the sign of a product, but nothing could SCALE an inequality -- which is what every weighted bound, gradient step, discounted backup and convexity argument does. The proof is `nnrat/rearrangement-two-point`, instantiated with the ORDER SUMS themselves rather than the components. Signed order `a <= b` is the nnrat comparison `q0 <= m0` where q0 = Pa + Nb and m0 = Pb + Na, and `0 <= c` is `Nc <= Pc`. Feeding (n,p,q,m) := (q0, m0, Nc, Pc) to rearrangement gives m0*Nc + q0*Pc <= m0*Pc + q0*Nc and each side is the corresponding side of the unfolded goal rearranged: the same four monomials, distributed and commuted. Both of those rearrangements are now single `rainbow.math.rational.nnrat.ring` calls -- they were about a hundred lines of hand-chained four-reorders and per-product commutations before the tactic existed. Native and axiom-free; chains the nnrat rearrangement toolkit, the nnrat-ring tactic and the signed sign rules on D63.

Depends onmath.rational.nnrat.ringmath.rational.nnrat.order-differencemath.rational.signed.multiply-order

signed/multiply-left-monotone :
  (c a b : ℚ)
  (hc : 0 ≤ c)
  (hab : a ≤ b)
  → c · a ≤ c · b

signed/multiply-right-monotone :
  (c a b : ℚ)
  (hc : 0 ≤ c)
  (hab : a ≤ b)
  → a · c ≤ b · c