Reference · Signed rationals

rainbow.math.rational.signed.convex-combination

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

Two-point convex combination of signed rationals stays within [min, max] -- the signed lift of nnrat/convex-at-most-max / convex-at-least-min, and a foundation brick for convex optimization over signed rationals (connects to the KKT / Lagrangian lane). signed/convex-at-most-max : (w0 + w1 ~ 1) -> (from-nnrat w0)*v0 + (from-nnrat w1)*v1 <= max v0 v1 signed/convex-at-least-min : (w0 + w1 ~ 1) -> min v0 v1 <= (from-nnrat w0)*v0 + (from-nnrat w1)*v1 Weights are nonnegative (nnrat, injected by from-nnrat). Each w_i*v_i is bounded by w_i*max (multiply-left-monotone, weight >= 0, v_i <= max), the two sum, and the weight sum collapses (w0+w1)*max ~ 1*max ~ max via distributivity + from-nnrat-add + (w0+w1~1). Does NOT route through the magnitude/reciprocal modulus, so it is free of that reduction wall. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.minmaxmath.rational.signed.multiply-monotonemath.rational.signed.order-monotonemath.rational.signed.distributivemath.linear.matrix.affine-general-rate-certificatemath.rational.signed.geometric-bridgemath.rational.signed.multiply-ringmath.rational.signed.unit-lawsmath.rational.signed.multiply-ordermath.rational.signed.order-respectsmath.rational.nnrat.farkas-elim-list

signed/convex-at-most-max :
  (w0 w1 : ℚ≥0) (v0 v1 : ℚ)
  (hw : w0 + w1 = 1)
  → signed/from-nnrat w0 · v0 + signed/from-nnrat w1 · v1 ≤ signed/max v0 v1

signed/convex-at-least-min :
  (w0 w1 : ℚ≥0) (v0 v1 : ℚ)
  (hw : w0 + w1 = 1)
  → signed/min v0 v1 ≤ signed/from-nnrat w0 · v0 + signed/from-nnrat w1 · v1